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

now

(((0. X),x to_power 0 ) ` ) ` = ((0. X) ` ) ` by Th1
.= (0. X) ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 5 ;
hence (((0. X),x to_power 0 ) ` ) ` = (0. X),x to_power 0 by Th1; :: thesis: verum

end;

then A1: S₁[ 0 ] ;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

now

let k be Element of NAT ; :: thesis: ( ( for m being Element of NAT st m = k & m <= n holds
(((0. X),x to_power m) ` ) ` = (0. X),x to_power m ) implies for m being Element of NAT st m = k + 1 & m <= n holds
(((0. X),x to_power (k + 1)) ` ) ` = (0. X),x to_power (k + 1) )
assume A3: for m being Element of NAT st m = k & m <= n holds
(((0. X),x to_power m) ` ) ` = (0. X),x to_power m ; :: thesis: for m being Element of 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 Element of 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 A4: 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 A3, A4
.= (((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;

hence for k being Element of NAT st S₁[k] holds
S₁[k + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence (((0. X),x to_power n) ` ) ` = (0. X),x to_power n ; :: thesis: verum