theorem Th13: :: ALGNUM_1:9
for A, B being Ring
for x1, x2 being Element of A st A is Subring of B holds
(In (x1,B)) * (In (x2,B)) = In ((x1 * x2),B)