let X be BCI-algebra; :: thesis: for a, b being Element of AtomSet X
for n being Nat holds (a \ b) |^ (- n) = (a |^ (- n)) \ (b |^ (- n))
let a, b be Element of AtomSet X; :: thesis: for n being Nat holds (a \ b) |^ (- n) = (a |^ (- n)) \ (b |^ (- n))
let n be Nat; :: thesis: (a \ b) |^ (- n) = (a |^ (- n)) \ (b |^ (- n))
set c = a ` ;
set d = b ` ;
reconsider c = a ` , d = b ` as Element of AtomSet X by BCIALG_1:34;
A1: ( c |^ n = a |^ (- n) & d |^ n = b |^ (- n) ) by Th10;
(a \ b) |^ (- n) = ((a \ b) `) |^ n by Th10
.= ((a `) \ (b `)) |^ n by BCIALG_1:9 ;
hence (a \ b) |^ (- n) = (a |^ (- n)) \ (b |^ (- n)) by A1, Th15; :: thesis: verum