let S be Ring; :: thesis: for R being Subring of S
for x being Element of S
for x1 being Element of R
for n being Element of NAT st x = x1 holds
x |^ n = x1 |^ n
let R be Subring of S; :: thesis: for x being Element of S
for x1 being Element of R
for n being Element of NAT st x = x1 holds
x |^ n = x1 |^ n
let x be Element of S; :: thesis: for x1 being Element of R
for n being Element of NAT st x = x1 holds
x |^ n = x1 |^ n
let x1 be Element of R; :: thesis: for n being Element of NAT st x = x1 holds
x |^ n = x1 |^ n
let n be Element of NAT ; :: thesis: ( x = x1 implies x |^ n = x1 |^ n )
assume AS: x = x1 ; :: thesis: x |^ n = x1 |^ n
defpred S₁[ Nat] means for x being Element of S
for x1 being Element of R st x = x1 holds
x |^ $1 = x1 |^ $1;

now :: thesis: for x being Element of S
for x1 being Element of R st x = x1 holds
x |^ 0 = x1 |^ 0

let x be Element of S; :: thesis: for x1 being Element of R st x = x1 holds
x |^ 0 = x1 |^ 0
let x1 be Element of R; :: thesis: ( x = x1 implies x |^ 0 = x1 |^ 0 )
assume x = x1 ; :: thesis: x |^ 0 = x1 |^ 0
thus x |^ 0 = 1_ S by BINOM:8
.= 1_ R by C0SP1:def 3
.= x1 |^ 0 by BINOM:8 ; :: thesis: verum

end;

then IA: S₁[ 0 ] ;
A: the multF of R = the multF of S || the carrier of R by C0SP1:def 3;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for x being Element of S
for x1 being Element of R st x = x1 holds
x |^ (k + 1) = x1 |^ (k + 1)

let x be Element of S; :: thesis: for x1 being Element of R st x = x1 holds
x |^ (k + 1) = x1 |^ (k + 1)
let x1 be Element of R; :: thesis: ( x = x1 implies x |^ (k + 1) = x1 |^ (k + 1) )
assume AS: x = x1 ; :: thesis: x |^ (k + 1) = x1 |^ (k + 1)
then C: x |^ k = x1 |^ k by IV;
B: [(x1 |^ k),x1] in [: the carrier of R, the carrier of R:] by ZFMISC_1:def 2;
thus x |^ (k + 1) = (x |^ k) * (x |^ 1) by BINOM:10
.= (x |^ k) * x by BINOM:8
.= (x1 |^ k) * x1 by AS, A, B, C, FUNCT_1:49
.= (x1 |^ k) * (x1 |^ 1) by BINOM:8
.= x1 |^ (k + 1) by BINOM:10 ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence x |^ n = x1 |^ n by AS; :: thesis: verum