let X be BCI-algebra; :: thesis: for x being Element of X
for n being Element of NAT holds x,(0. X) to_power (n + 1) = x
let x be Element of X; :: thesis: for n being Element of NAT holds x,(0. X) to_power (n + 1) = x
let n be Element of NAT ; :: thesis: x,(0. X) to_power (n + 1) = x
defpred S₁[ set ] means for m being Element of NAT st m = $1 & m <= n holds
x,(0. X) to_power (m + 1) = x;

now

x,(0. X) to_power (0 + 1) = x \ (0. X) by Th2;
hence x,(0. X) to_power (0 + 1) = x by BCIALG_1:2; :: thesis: verum

end;

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