let A, B be Ring; :: thesis: for x1, x2 being Element of A st A is Subring of B holds
(In (x1,B)) * (In (x2,B)) = In ((x1 * x2),B)
let x1, x2 be Element of A; :: thesis: ( A is Subring of B implies (In (x1,B)) * (In (x2,B)) = In ((x1 * x2),B) )
assume A0: A is Subring of B ; :: thesis: (In (x1,B)) * (In (x2,B)) = In ((x1 * x2),B)
then x1 is Element of B by Lm6;
then A2: In (x1,B) = x1 by SUBSET_1:def 8;
x2 is Element of B by A0, Lm6;
then A4: In (x2,B) = x2 by SUBSET_1:def 8;
x1 * x2 is Element of B by A0, Lm6;
then In ((x1 * x2),B) = x1 * x2 by SUBSET_1:def 8
.= (In (x1,B)) * (In (x2,B)) by A0, A2, A4, Th9 ;
hence (In (x1,B)) * (In (x2,B)) = In ((x1 * x2),B) ; :: thesis: verum