let X be BCI-algebra; :: thesis: for x, y being Element of X
for n being Element of NAT st x \ y = x holds
x,y to_power n = x
let x, y be Element of X; :: thesis: for n being Element of NAT st x \ y = x holds
x,y to_power n = x
let n be Element of NAT ; :: thesis: ( x \ y = x implies x,y to_power n = x )
assume A1: x \ y = x ; :: thesis: x,y to_power n = x
defpred S₁[ set ] means for m being Element of NAT st m = $1 & m <= n holds
x,y to_power m = x;
A2: S₁[ 0 ] by Th1;
A3: 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
x,y to_power m = x ) implies for m being Element of NAT st m = k + 1 & m <= n holds
x,y to_power (k + 1) = x )
assume A4: for m being Element of NAT st m = k & m <= n holds
x,y to_power m = x ; :: thesis: for m being Element of NAT st m = k + 1 & m <= n holds
x,y to_power (k + 1) = x
let m be Element of NAT ; :: thesis: ( m = k + 1 & m <= n implies x,y to_power (k + 1) = x )
assume A5: ( m = k + 1 & m <= n ) ; :: thesis: x,y to_power (k + 1) = x
A6: x,y to_power (k + 1) = (x,y to_power k) \ y by Th4;
k <= n by A5, NAT_1:13;
hence x,y to_power (k + 1) = x by A1, A4, A6; :: 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(A2, A3);
hence x,y to_power n = x ; :: thesis: verum