let X be BCI-algebra; for x, y, z being Element of X
for n being Nat holds ((x,y) to_power n) \ z = ((x \ z),y) to_power n
let x, y, z be Element of X; for n being Nat holds ((x,y) to_power n) \ z = ((x \ z),y) to_power n
let n be Nat; ((x,y) to_power n) \ z = ((x \ z),y) to_power n
defpred S1[ set ] means for m being Nat st m = $1 & m <= n holds
((x,y) to_power m) \ z = ((x \ z),y) to_power m;
now for k being Nat st ( for m being Nat st m = k & m <= n holds
((x,y) to_power m) \ z = ((x \ z),y) to_power m ) holds
for m being Nat st m = k + 1 & m <= n holds
((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1)let k be
Nat;
( ( for m being Nat st m = k & m <= n holds
((x,y) to_power m) \ z = ((x \ z),y) to_power m ) implies for m being Nat st m = k + 1 & m <= n holds
((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1) )assume A1:
for
m being
Nat st
m = k &
m <= n holds
((x,y) to_power m) \ z = (
(x \ z),
y)
to_power m
;
for m being Nat st m = k + 1 & m <= n holds
((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1)let m be
Nat;
( m = k + 1 & m <= n implies ((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1) )assume that A2:
m = k + 1
and A3:
m <= n
;
((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1)
((x,y) to_power m) \ z = (((x,y) to_power k) \ y) \ z
by A2, Th4;
then A4:
((x,y) to_power m) \ z = (((x,y) to_power k) \ z) \ y
by BCIALG_1:7;
k <= n
by A2, A3, NAT_1:13;
then
((x,y) to_power m) \ z = (((x \ z),y) to_power k) \ y
by A1, A4;
hence
((x,y) to_power m) \ z = (
(x \ z),
y)
to_power (k + 1)
by Th4;
verum end;
then A5:
for k being Nat st S1[k] holds
S1[k + 1]
;
((x,y) to_power 0) \ z = x \ z
by Th1;
then A6:
S1[ 0 ]
by Th1;
for n being Nat holds S1[n]
from NAT_1:sch 2(A6, A5);
hence
((x,y) to_power n) \ z = ((x \ z),y) to_power n
; verum