let X be BCI-algebra; :: thesis: for a being Element of AtomSet X
for i, j being Integer holds (a |^ i) |^ j = a |^ (i * j)
let a be Element of AtomSet X; :: thesis: for i, j being Integer holds (a |^ i) |^ j = a |^ (i * j)
let i, j be Integer; :: thesis: (a |^ i) |^ j = a |^ (i * j)

per cases ( i >= 0 or i < 0 ) ;

suppose A1: i >= 0 ; :: thesis: (a |^ i) |^ j = a |^ (i * j)

per cases ( j >= 0 or j < 0 ) ;

suppose B1: j >= 0 ; :: thesis: (a |^ i) |^ j = a |^ (i * j)

reconsider i = i, j = j as Element of NAT by A1, B1, INT_1:16;
(a |^ i) |^ j = a |^ (i * j) by Th15;
hence (a |^ i) |^ j = a |^ (i * j) ; :: thesis: verum

end;

suppose B3: j < 0 ; :: thesis: (a |^ i) |^ j = a |^ (i * j)

then reconsider m = - j as Element of NAT by INT_1:16;
reconsider i = i as Element of NAT by A1, INT_1:16;

per cases ( i * j < 0 or i * j = 0 ) by B3;

suppose D1: i * j < 0 ; :: thesis: (a |^ i) |^ j = a |^ (i * j)

then reconsider p = - (i * j) as Element of NAT by INT_1:16;
reconsider b = a ` as Element of AtomSet X by BCIALG_1:34;
reconsider d = a |^ i as Element of AtomSet X by Th12;
a |^ (i * j) = (BCI-power X) . (a ` ),(abs (i * j)) by Def2, D1
.= (a ` ) |^ p by D1, ABSVALUE:def 1
.= (a ` ) |^ (i * (- j))
.= (b |^ i) |^ m by Th15
.= ((a |^ i) ` ) |^ m by Th17
.= d |^ (- m) by Th9
.= (a |^ i) |^ (- (- j)) ;
hence (a |^ i) |^ j = a |^ (i * j) ; :: thesis: verum

end;

suppose D3: i * j = 0 ; :: thesis: (a |^ i) |^ j = a |^ (i * j)

reconsider d = 0. X as Element of AtomSet X by BCIALG_1:23;
(a |^ 0 ) |^ j = (0. X) |^ j by Def1
.= (BCI-power X) . ((0. X) ` ),(abs j) by Def2, B3
.= ((0. X) ` ) |^ m by B3, ABSVALUE:def 1
.= (d |^ m) ` by Th17
.= (0. X) ` by Th6
.= 0. X by BCIALG_1:2
.= a |^ (i * j) by D3, Th2 ;
hence (a |^ i) |^ j = a |^ (i * j) by B3, D3, XCMPLX_1:6; :: thesis: verum

end;

end;

end;

end;

end;

suppose A3: i < 0 ; :: thesis: (a |^ i) |^ j = a |^ (i * j)

then reconsider m = - i as Element of NAT by INT_1:16;

per cases ( j > 0 or j = 0 or j < 0 ) ;

suppose C1: j > 0 ; :: thesis: (a |^ i) |^ j = a |^ (i * j)

then reconsider j = j as Element of NAT by INT_1:16;
reconsider p = - (i * j) as Element of NAT by A3, INT_1:16;
reconsider b = a ` as Element of AtomSet X by BCIALG_1:34;
D1: i * j < 0 * j by A3, C1, XREAL_1:70;
then a |^ (i * j) = (BCI-power X) . (a ` ),(abs (i * j)) by Def2
.= (a ` ) |^ p by D1, ABSVALUE:def 1
.= (a ` ) |^ ((- i) * j)
.= (b |^ m) |^ j by Th15
.= (a |^ (- m)) |^ j by Th9 ;
hence (a |^ i) |^ j = a |^ (i * j) ; :: thesis: verum

end;

suppose C3: j = 0 ; :: thesis: (a |^ i) |^ j = a |^ (i * j)

reconsider b = a |^ i as Element of AtomSet X by Th12;
(a |^ i) |^ j = b |^ 0 by C3
.= 0. X by Def1
.= a |^ (i * 0 ) by Th2 ;
hence (a |^ i) |^ j = a |^ (i * j) by C3; :: thesis: verum

end;

suppose C5: j < 0 ; :: thesis: (a |^ i) |^ j = a |^ (i * j)

then reconsider n = - j as Element of NAT by INT_1:16;
reconsider p = i * j as Element of NAT by A3, C5, INT_1:16;
reconsider b = a ` as Element of AtomSet X by BCIALG_1:34;
reconsider d = a |^ m as Element of AtomSet X by Th12;
reconsider e = d ` as Element of AtomSet X by BCIALG_1:34;
a |^ i = (BCI-power X) . (a ` ),(abs i) by Def2, A3
.= (a ` ) |^ m by A3, ABSVALUE:def 1 ;
then (a |^ i) |^ j = e |^ (- n) by Th17
.= (e ` ) |^ n by Th9
.= d |^ n by BCIALG_1:29
.= a |^ ((- i) * (- j)) by Th15 ;
hence (a |^ i) |^ j = a |^ (i * j) ; :: thesis: verum

end;

end;

end;

end;