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

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 A1: 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 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 Element of 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 Element of NAT holds S₁[n] from NAT_1:sch 1(A6, A5);
hence (x,(0. X)) to_power (n + 1) = x ; :: thesis: verum