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 j >= 0 ; :: thesis: (a |^ i) |^ j = a |^ (i * j)

then reconsider i = i, j = j as Element of NAT by A1, INT_1:3;
(a |^ i) |^ j = a |^ (i * j) by Lm2;
hence (a |^ i) |^ j = a |^ (i * j) ; :: thesis: verum

end;

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

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

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

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

then reconsider p = - (i * j) as Element of NAT by INT_1:3;
reconsider b = a ` as Element of AtomSet X by BCIALG_1:34;
reconsider d = a |^ i as Element of AtomSet X by Th13;
a |^ (i * j) = (BCI-power X) . ((a `),|.(i * j).|) by A3, Def2
.= (a `) |^ p by A3, ABSVALUE:def 1
.= (a `) |^ (i * (- j))
.= (b |^ i) |^ m by Lm2
.= ((a |^ i) `) |^ m by Th17
.= d |^ (- m) by Th10
.= (a |^ i) |^ (- (- j)) ;
hence (a |^ i) |^ j = a |^ (i * j) ; :: thesis: verum

end;

suppose A4: 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) `),|.j.|) by A2, Def2
.= ((0. X) `) |^ m by A2, ABSVALUE:def 1
.= (d |^ m) ` by Th17
.= (0. X) ` by Th7
.= 0. X by BCIALG_1:2
.= a |^ (i * j) by A4, Th3 ;
hence (a |^ i) |^ j = a |^ (i * j) by A2, A4, XCMPLX_1:6; :: thesis: verum

end;

end;

end;

end;

end;

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

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

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

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

then reconsider j = j as Element of NAT by INT_1:3;
reconsider b = a ` as Element of AtomSet X by BCIALG_1:34;
reconsider p = - (i * j) as Element of NAT by A5, INT_1:3;
A7: i * j < 0 * j by A5, A6;
then a |^ (i * j) = (BCI-power X) . ((a `),|.(i * j).|) by Def2
.= (a `) |^ p by A7, ABSVALUE:def 1
.= (a `) |^ ((- i) * j)
.= (b |^ m) |^ j by Lm2
.= (a |^ (- m)) |^ j by Th10 ;
hence (a |^ i) |^ j = a |^ (i * j) ; :: thesis: verum

end;

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

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

end;

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

then reconsider n = - j as Element of NAT by INT_1:3;
reconsider d = a |^ m as Element of AtomSet X by Th13;
reconsider e = d ` as Element of AtomSet X by BCIALG_1:34;
a |^ i = (BCI-power X) . ((a `),|.i.|) by A5, Def2
.= (a `) |^ m by A5, ABSVALUE:def 1 ;
then (a |^ i) |^ j = e |^ (- n) by Th17
.= (e `) |^ n by Th10
.= d |^ n by BCIALG_1:29
.= a |^ ((- i) * (- j)) by Lm2 ;
hence (a |^ i) |^ j = a |^ (i * j) ; :: thesis: verum

end;

end;

end;

end;