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

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

suppose j > 0 ; :: thesis: a |^ (i + j) = (a |^ i) \ ((a |^ j) `)

then reconsider j = j as Element of NAT by INT_1:3;
(a |^ i) \ ((a |^ j) `) = (a |^ i) \ ((a `) |^ j) by Th17
.= (a |^ i) \ (a |^ (- j)) by Th10
.= a |^ (i - (- j)) by Th22 ;
hence a |^ (i + j) = (a |^ i) \ ((a |^ j) `) ; :: thesis: verum

end;

suppose A1: j = 0 ; :: thesis: a |^ (i + j) = (a |^ i) \ ((a |^ j) `)

then a |^ (i + j) = (a |^ i) \ (0. X) by BCIALG_1:2
.= (a |^ i) \ ((0. X) `) by BCIALG_1:2
.= (a |^ i) \ ((a |^ j) `) by A1, Th3 ;
hence a |^ (i + j) = (a |^ i) \ ((a |^ j) `) ; :: thesis: verum

end;

suppose j < 0 ; :: thesis: a |^ (i + j) = (a |^ i) \ ((a |^ j) `)

then reconsider n = - j as Element of NAT by INT_1:3;
reconsider b = a ` as Element of AtomSet X by BCIALG_1:34;
(a |^ i) \ ((a |^ j) `) = (a |^ i) \ ((a |^ (- (- j))) `)
.= (a |^ i) \ (((a `) |^ n) `) by Th10
.= (a |^ i) \ ((b `) |^ n) by Th17
.= (a |^ i) \ (a |^ n) by BCIALG_1:29
.= a |^ (i - n) by Th22 ;
hence a |^ (i + j) = (a |^ i) \ ((a |^ j) `) ; :: thesis: verum

end;

end;