metamath/valid/mathd-algebra-67.mm

$(
  @{
    mathd-algebra-67.0 @e |- F = ( x e. RR |-> ( ( 5 x. X ) + 3 ) ) $@
    mathd-algebra-67.1 @e |- G = ( x e. RR |-> ( ( X ^ 2 ) - 2 ) ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-67 @p |- ( ph -> ( G ` ( F ` -u 1 ) ) = 2 ) @=
      ? @.
  @}
$)