theorem Th10: :: RING_EMB:10

for A being AbGroup
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
f . ( the addF of A . (((f ") . a),((f ") . b))) is Element of X