let X be BCI-algebra; :: thesis: for a being Element of AtomSet X
for i, j being Integer st i > 0 & j > 0 holds
(a |^ i) \ (a |^ j) = a |^ (i - j)
let a be Element of AtomSet X; :: thesis: for i, j being Integer st i > 0 & j > 0 holds
(a |^ i) \ (a |^ j) = a |^ (i - j)
let i, j be Integer; :: thesis: ( i > 0 & j > 0 implies (a |^ i) \ (a |^ j) = a |^ (i - j) )
assume that
A1: i > 0 and
A2: j > 0 ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)

per cases ( i = j or i > j or i < j ) by XXREAL_0:1;

suppose A3: i = j ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)

then (a |^ i) \ (a |^ j) = 0. X by BCIALG_1:def 5;
then (a |^ i) \ (a |^ j) = a |^ 0 by Def1;
hence (a |^ i) \ (a |^ j) = a |^ (i - j) by A3; :: thesis: verum

end;

suppose A4: i > j ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)

set m = i - j;
i - j > 0 by A4, XREAL_1:50;
then reconsider j = j, m = i - j as Element of NAT by A2, INT_1:3;
a |^ i = a |^ ((i - j) + j)
.= (a |^ j) \ ((a |^ m) `) by Lm1 ;
then A5: (a |^ i) \ (a |^ j) = ((a |^ j) \ (a |^ j)) \ ((a |^ m) `) by BCIALG_1:7;
a |^ m in AtomSet X by Th13;
then ((a |^ m) `) ` = a |^ m by BCIALG_1:29;
hence (a |^ i) \ (a |^ j) = a |^ (i - j) by A5, BCIALG_1:def 5; :: thesis: verum

end;

suppose A6: i < j ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)

set m = j - i;
j - i > 0 by A6, XREAL_1:50;
then reconsider i = i, m = j - i as Element of NAT by A1, INT_1:3;
A7: 0. X in AtomSet X ;
a |^ j = a |^ (i + (j - i))
.= (a |^ i) \ ((a |^ m) `) by Lm1 ;
then (a |^ i) \ (a |^ j) = (a |^ m) ` by A7, BCIALG_1:32;
then (a |^ i) \ (a |^ j) = (a `) |^ m by Th17;
then (a |^ i) \ (a |^ j) = a |^ (- m) by Th10;
hence (a |^ i) \ (a |^ j) = a |^ (i - j) ; :: thesis: verum

end;

end;