let X be BCI-algebra; :: thesis: for x, y being Element of X
for n being Nat holds (x,y) to_power (n + 1) = ((x,y) to_power n) \ y
let x, y be Element of X; :: thesis: for n being Nat holds (x,y) to_power (n + 1) = ((x,y) to_power n) \ y
let n be Nat; :: thesis: (x,y) to_power (n + 1) = ((x,y) to_power n) \ y
A1: n < n + 1 by NAT_1:3, XREAL_1:29;
consider g being sequence of the carrier of X such that
A2: (x,y) to_power n = g . n and
A3: g . 0 = x and
A4: for j being Nat st j < n holds
g . (j + 1) = (g . j) \ y by Def1;
consider f being sequence of the carrier of X such that
A5: (x,y) to_power (n + 1) = f . (n + 1) and
A6: f . 0 = x and
A7: for j being Nat st j < n + 1 holds
f . (j + 1) = (f . j) \ y by Def1;
defpred S₁[ set ] means for m being Nat st m = $1 & m <= n holds
f . m = g . m;

now :: thesis: for k being Nat st ( for m being Nat st m = k & m <= n holds
f . m = g . m ) holds
for m being Nat st m = k + 1 & m <= n holds
f . m = g . m

let k be Nat; :: thesis: ( ( for m being Nat st m = k & m <= n holds
f . m = g . m ) implies for m being Nat st m = k + 1 & m <= n holds
f . m = g . m )
assume A8: for m being Nat st m = k & m <= n holds
f . m = g . m ; :: thesis: for m being Nat st m = k + 1 & m <= n holds
f . m = g . m
let m be Nat; :: thesis: ( m = k + 1 & m <= n implies f . m = g . m )
assume that
A9: m = k + 1 and
A10: m <= n ; :: thesis: f . m = g . m
k + 1 <= n + 1 by A9, A10, NAT_1:13;
then k < n + 1 by NAT_1:13;
then A11: f . (k + 1) = (f . k) \ y by A7;
A12: k < n by A9, A10, NAT_1:13;
then g . (k + 1) = (g . k) \ y by A4;
hence f . m = g . m by A8, A9, A12, A11; :: thesis: verum

end;

then A13: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A14: S₁[ 0 ] by A6, A3;
for n being Nat holds S₁[n] from NAT_1:sch 2(A14, A13);
then f . n = g . n ;
hence (x,y) to_power (n + 1) = ((x,y) to_power n) \ y by A5, A7, A2, A1; :: thesis: verum