let X be BCI-algebra; :: thesis: for x, y being Element of X
for n being Nat st x \ y = x holds
(x,y) to_power n = x
let x, y be Element of X; :: thesis: for n being Nat st x \ y = x holds
(x,y) to_power n = x
let n be Nat; :: thesis: ( x \ y = x implies (x,y) to_power n = x )
defpred S₁[ set ] means for m being Nat st m = $1 & m <= n holds
(x,y) to_power m = x;
assume A1: x \ y = x ; :: thesis: (x,y) to_power n = x

now :: thesis: for k being Nat st ( for m being Nat st m = k & m <= n holds
(x,y) to_power m = x ) holds
for m being Nat st m = k + 1 & m <= n holds
(x,y) to_power (k + 1) = x

let k be Nat; :: thesis: ( ( for m being Nat st m = k & m <= n holds
(x,y) to_power m = x ) implies for m being Nat st m = k + 1 & m <= n holds
(x,y) to_power (k + 1) = x )
assume A2: for m being Nat st m = k & m <= n holds
(x,y) to_power m = x ; :: thesis: for m being Nat st m = k + 1 & m <= n holds
(x,y) to_power (k + 1) = x
let m be Nat; :: thesis: ( m = k + 1 & m <= n implies (x,y) to_power (k + 1) = x )
A3: (x,y) to_power (k + 1) = ((x,y) to_power k) \ y by Th4;
assume ( m = k + 1 & m <= n ) ; :: thesis: (x,y) to_power (k + 1) = x
then k <= n by NAT_1:13;
hence (x,y) to_power (k + 1) = x by A1, A2, A3; :: thesis: verum

end;

then A4: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A5: S₁[ 0 ] by Th1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A4);
hence (x,y) to_power n = x ; :: thesis: verum