:: deftheorem defines emb_AbGr RING_EMB:def 10 :
for A being AbGroup
for X being non empty set
for f being Function of A,X holds emb_AbGr f = addLoopStr(# X,(addemb f),(f . (0. A)) #);