$(
  @{
    mathd-algebra-15.0 @e |- S = ( a e. NN , b e. NN |-> ( ( a ^ b ) + ( b ^ a ) ) ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-15 @p |- ( ph -> ( 2 S 6 ) = ; ; 1 0 0 ) @=
      ? @.
  @}
$)