:: deftheorem defadd defines addemb FIELD_2:def 4 :
for R being Ring
for S being b₁ -monomorphic Ring
for f being Monomorphism of R,S
for b₄ being BinOp of (carr f) holds
( b₄ = addemb f iff for a, b being Element of carr f holds b₄ . (a,b) = addemb (f,a,b) );