theorem Th9: :: ALGNUM_1:6

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