metamath/valid/mathd-algebra-35.mm

$(
  @{
    mathd-algebra-35.0 @e |- P = ( x e. RR |-> ( 2 - ( x ^ 2 ) ) ) $@
    mathd-algebra-35.1 @e |- Q = ( x e. RR* |-> ( 6 / x ) ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-35 @p |- ( ph -> ( P ` ( Q ` 2 ) ) = -u 7 ) @=
      ? @.
  @}
$)