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

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

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

end;

then A5: for k being Nat st S₁[k] holds
S₁[k + 1] ;
(x,(0. X)) to_power (0 + 1) = x \ (0. X) by Th2;
then A6: S₁[ 0 ] by BCIALG_1:2;
for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A5);
hence (x,(0. X)) to_power (n + 1) = x ; :: thesis: verum