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) )
A2: (((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 ;
assume ( m = k + 1 & m <= n ) ; :: thesis: (((0. X),x) to_power (k + 1)) ` = ((0. X),(x `)) to_power (k + 1)
then k <= n by NAT_1:13;
hence (((0. X),x) to_power (k + 1)) ` = (((0. X),(x `)) to_power k) \ (x `) by A1, A2
.= ((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;
then (((0. X),x) to_power 0) ` = 0. X by BCIALG_1:2;
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