metamath/valid/mathd-algebra-214.mm

$(
  @{
    mathd-algebra-214.0 @e |- ( ph -> A e. RR ) $@
    mathd-algebra-214.1 @e |- F = ( x e. RR |-> ( ( A x. ( ( x - 2 ) ^ 2 ) ) + 3 ) ) $@
    mathd-algebra-214.2 @e |- ( ph -> ( F ` 4 ) = 4 ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-214 @p |- ( ph -> ( F ` 6 ) = 7 ) @=
      ? @.
  @}
$)