:: deftheorem defines emb_Ring RING_EMB:def 5 :
for A being Ring
for X being non empty set
for f being Function of A,X holds emb_Ring f = doubleLoopStr(# X,(addemb f),(multemb f),(f . (1. A)),(f . (0. A)) #);