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)
defpred S₁[ Nat] means (a \ b) |^ $1 = (a |^ $1) \ (b |^ $1);
(a \ b) |^ 0 = 0. X by Def1
.= (0. X) ` by BCIALG_1:def 5
.= (a |^ 0 ) \ (0. X) by Def1 ;
then A1: S₁[ 0 ] by Def1;

A3: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume B1: S₁[n] ; :: thesis: S₁[n + 1]
B2: ( (b |^ n) ` in AtomSet X & a |^ (n + 1) in AtomSet X ) by Th12, BCIALG_1:34;
(a \ b) |^ (n + 1) = (a \ b) \ (((a |^ n) \ (b |^ n)) ` ) by B1, Th1
.= (a \ (((a |^ n) \ (b |^ n)) ` )) \ b by BCIALG_1:7
.= (a \ (((a |^ n) ` ) \ ((b |^ n) ` ))) \ b by BCIALG_1:9
.= (((b |^ n) ` ) \ (((a |^ n) ` ) \ a)) \ b by B2, Th0
.= (((b |^ n) ` ) \ b) \ (((a |^ n) ` ) \ a) by BCIALG_1:7
.= ((b |^ (n + 1)) ` ) \ (((a |^ n) ` ) \ a) by Th13
.= ((b |^ (n + 1)) ` ) \ ((a |^ (n + 1)) ` ) by Th13
.= ((b |^ (n + 1)) \ (a |^ (n + 1))) ` by BCIALG_1:9
.= (a |^ (n + 1)) \ (b |^ (n + 1)) by B2, BCIALG_1:30 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
hence (a \ b) |^ n = (a |^ n) \ (b |^ n) ; :: thesis: verum