let A, B be 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)
let x1, x2 be Element of A; ( A is Subring of B implies (In (x1,B)) * (In (x2,B)) = In ((x1 * x2),B) )
assume A0:
A is Subring of B
; (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)
; verum