:: deftheorem Def11 defines multreal BINOP_2:def 11 :
for b₁ being BinOp of REAL holds
( b₁ = multreal iff for r1, r2 being Real holds b₁ . (r1,r2) = r1 * r2 );