:: deftheorem Def9 defines addemb RING_EMB:def 9 :
for A being AbGroup
for X being non empty set
for f being Function of A,X
for b₄ being BinOp of X holds
( b₄ = addemb f iff for a, b being Element of X holds b₄ . (a,b) = addemb (f,a,b) );