:: deftheorem Def17 defines multrat BINOP_2:def 17 :
for b₁ being BinOp of RAT holds
( b₁ = multrat iff for w1, w2 being Rational holds b₁ . (w1,w2) = w1 * w2 );