theorem Th8: :: ALGNUM_1:5
for A, B being Ring
for x, y being Element of B
for x1, y1 being Element of A st A is Subring of B & x = x1 & y = y1 holds
x + y = x1 + y1