let X be BCI-algebra; 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; for n being Nat holds (((0. X),x) to_power n) ` = ((0. X),(x `)) to_power n
let n be Nat; (((0. X),x) to_power n) ` = ((0. X),(x `)) to_power n
defpred S1[ 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 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;
( ( 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
;
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;
( 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 )
;
(((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
;
verum end;
then A3:
for k being Nat st S1[k] holds
S1[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:
S1[ 0 ]
by Th1;
for n being Nat holds S1[n]
from NAT_1:sch 2(A4, A3);
hence
(((0. X),x) to_power n) ` = ((0. X),(x `)) to_power n
; verum