theorem Th3: :: RING_EMB:3

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