let n be Element of NAT ; :: thesis: for A, B being Ring
for z being Element of A st A is Subring of B holds
(power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B)
let A, B be Ring; :: thesis: for z being Element of A st A is Subring of B holds
(power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B)
let z be Element of A; :: thesis: ( A is Subring of B implies (power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B) )
assume A0: A is Subring of B ; :: thesis: (power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B)
then z is Element of B by Lm6;
then A2: In (z,B) = z by SUBSET_1:def 8;
A3: 1_ A = 1_ B by A0, C0SP1:def 3;
reconsider x = z as Element of B by A0, Lm6;
(power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B)

proof

defpred S₁[ Nat] means (power B) . ((In (z,B)),$1) = In (((power A) . (z,$1)),B);
A5: S₁[ 0 ]

proof

A6: In ((1. A),B) = 1. B by A0, Lm5;
In (((power A) . (z,0)),B) = 1. B by A3, GROUP_1:def 7, A6;
hence S₁[ 0 ] by A3, GROUP_1:def 7; :: thesis: verum

end;

A7: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A9: S₁[m] ; :: thesis: S₁[m + 1]
A10: (power A) . (z,m) is Element of B by A0, Lm6;
A11: In (((power A) . (z,m)),B) = (power A) . (z,m) by A10, SUBSET_1:def 8;
A12: (power A) . (z,(m + 1)) is Element of B by A0, Lm6;
(power B) . ((In (z,B)),(m + 1)) = ((power B) . ((In (z,B)),m)) * (In (z,B)) by GROUP_1:def 7
.= ((power A) . (z,m)) * z by A0, A11, A2, Th9, A9
.= (power A) . (z,(m + 1)) by GROUP_1:def 7
.= In (((power A) . (z,(m + 1))),B) by A12, SUBSET_1:def 8 ;
hence S₁[m + 1] ; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A5, A7);
hence (power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B) ; :: thesis: verum

end;

hence (power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B) ; :: thesis: verum