:: deftheorem Def1 defines addemb RING_EMB:def 1 :
for A being Ring
for X being non empty set
for f being Function of A,X
for a, b being Element of X st f is bijective holds
addemb (f,a,b) = f . ( the addF of A . (((f ") . a),((f ") . b)));