let X be BCI-algebra; :: thesis: for x, y being Element of X
for n being Element of 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 Element of NAT holds x,y to_power (n + 1) = (x,y to_power n) \ y
let n be Element of NAT ; :: thesis: x,y to_power (n + 1) = (x,y to_power n) \ y
consider f being Function of NAT ,the carrier of X such that
A1: ( x,y to_power (n + 1) = f . (n + 1) & f . 0 = x & ( for j being Element of NAT st j < n + 1 holds
f . (j + 1) = (f . j) \ y ) ) by Def1;
consider g being Function of NAT ,the carrier of X such that
A2: ( x,y to_power n = g . n & g . 0 = x & ( for j being Element of NAT st j < n holds
g . (j + 1) = (g . j) \ y ) ) by Def1;
defpred S₁[ set ] means for m being Element of NAT st m = $1 & m <= n holds
f . m = g . m;
A3: S₁[ 0 ] by A1, A2;
A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

now

let k be Element of NAT ; :: thesis: ( ( for m being Element of NAT st m = k & m <= n holds
f . m = g . m ) implies for m being Element of NAT st m = k + 1 & m <= n holds
f . m = g . m )
assume A5: for m being Element of NAT st m = k & m <= n holds
f . m = g . m ; :: thesis: for m being Element of NAT st m = k + 1 & m <= n holds
f . m = g . m
let m be Element of NAT ; :: thesis: ( m = k + 1 & m <= n implies f . m = g . m )
assume A6: ( m = k + 1 & m <= n ) ; :: thesis: f . m = g . m
A7: ( k < n + 1 & k < n & k <= n )

proof

k + 1 <= n + 1 by A6, NAT_1:13;
hence k < n + 1 by NAT_1:13; :: thesis: ( k < n & k <= n )
thus ( k < n & k <= n ) by A6, NAT_1:13; :: thesis: verum

end;

then ( f . (k + 1) = (f . k) \ y & g . (k + 1) = (g . k) \ y ) by A1, A2;
hence f . m = g . m by A5, A6, A7; :: thesis: verum

end;

hence for k being Element of NAT st S₁[k] holds
S₁[k + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4);
then A8: f . n = g . n ;
n < n + 1 by NAT_1:3, XREAL_1:31;
hence x,y to_power (n + 1) = (x,y to_power n) \ y by A1, A2, A8; :: thesis: verum