:: deftheorem Def24 defines multnat BINOP_2:def 24 :
for b₁ being BinOp of NAT holds
( b₁ = multnat iff for n1, n2 being Nat holds b₁ . (n1,n2) = n1 * n2 );