:: deftheorem defmult defines multemb FIELD_2:def 6 :
for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T
for b₄ being BinOp of (carr f) holds
( b₄ = multemb f iff for a, b being Element of carr f holds b₄ . (a,b) = multemb (f,a,b) );