:: deftheorem Def7 defines multR FIELD_3:def 8 :
for R being non almost_trivial Ring
for x being non trivial Element of R
for o being object
for b₄ being BinOp of (carr (x,o)) holds
( b₄ = multR (x,o) iff for a, b being Element of carr (x,o) holds b₄ . (a,b) = multR (a,b) );