let R be Ring; :: thesis: for I being Ideal of R
for x being Element of (R / I)
for a being Element of R st x = Class ((EqRel (R,I)),a) holds
for n being Nat holds x |^ n = Class ((EqRel (R,I)),(a |^ n))
let I be Ideal of R; :: thesis: for x being Element of (R / I)
for a being Element of R st x = Class ((EqRel (R,I)),a) holds
for n being Nat holds x |^ n = Class ((EqRel (R,I)),(a |^ n))
let x be Element of (R / I); :: thesis: for a being Element of R st x = Class ((EqRel (R,I)),a) holds
for n being Nat holds x |^ n = Class ((EqRel (R,I)),(a |^ n))
let a be Element of R; :: thesis: ( x = Class ((EqRel (R,I)),a) implies for n being Nat holds x |^ n = Class ((EqRel (R,I)),(a |^ n)) )
assume A1: x = Class ((EqRel (R,I)),a) ; :: thesis: for n being Nat holds x |^ n = Class ((EqRel (R,I)),(a |^ n))
let n be Nat; :: thesis: x |^ n = Class ((EqRel (R,I)),(a |^ n))
defpred S₁[ Nat] means x |^ $1 = Class ((EqRel (R,I)),(a |^ $1));
x |^ 0 = 1_ (R / I) by BINOM:8
.= Class ((EqRel (R,I)),(1_ R)) by RING_1:def 6
.= Class ((EqRel (R,I)),(a |^ 0)) by BINOM:8 ;
then A2: S₁[ 0 ] ;

A3: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
Class ((EqRel (R,I)),(a |^ (i + 1))) = Class ((EqRel (R,I)),((a |^ i) * (a |^ 1))) by BINOM:10
.= Class ((EqRel (R,I)),((a |^ i) * a)) by BINOM:8
.= (x |^ i) * x by A1, A4, RING_1:14
.= (x |^ i) * (x |^ 1) by BINOM:8
.= x |^ (i + 1) by BINOM:10 ;
hence S₁[i + 1] ; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence x |^ n = Class ((EqRel (R,I)),(a |^ n)) ; :: thesis: verum