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

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

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

end;

then A3: for k being Nat st S₁[k] holds
S₁[k + 1] ;
((((0. X),x) to_power 0) `) ` = ((0. X) `) ` by Th1
.= (0. X) ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 5 ;
then A4: S<sub>1</sub>[ 0 ] by Th1;
for n being Nat holds S<sub>1</sub>[n] from NAT_1:sch 2(A4, A3);
hence ((((0. X),x) to_power n) `) ` = ((0. X),x) to_power n ; :: thesis: verum