theorem Th12: :: RING_EMB:12

for A being AbGroup
for X being non empty set
for f being Function of A,X st f is bijective holds
emb_AbGr f is AbGroup