$(
  @{
    amc12a-2009-p9.0 @e |- ( ph -> F : RR --> RR ) $@
    amc12a-2009-p9.1 @e |- ( ph -> X e. RR ) $@
    amc12a-2009-p9.2 @e |- ( ph -> A e. RR ) $@
    amc12a-2009-p9.3 @e |- ( ph -> B e. RR ) $@
    amc12a-2009-p9.4 @e |- ( ph -> C e. RR ) $@
    amc12a-2009-p9.5 @e |- ( ph -> ( F ` ( X + 3 ) ) = ( ( 3 x. ( X ^ 2 ) ) + ( ( 7 x. X ) + 4 ) ) ) $@
    amc12a-2009-p9.6 @e |- ( ph -> ( F ` X ) = ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) ) $@
    @( (Contributed by Kunhao Zheng, 9-Aug-2021.) @)
    amc12a-2009-p9 @p |- ( ph -> ( ( A + B ) + C ) = 2 ) @=
      ? @.
  @}
$)