theorem Th5: :: RING_EMB:5

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