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);

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
A2: (b |^ n) ` in AtomSet X by BCIALG_1:34;
A3: a |^ (n + 1) in AtomSet X by Th13;
assume S<sub>1</sub>[n] ; :: thesis: S<sub>1</sub>[n + 1]
then (a \ b) |^ (n + 1) = (a \ b) \ (((a |^ n) \ (b |^ n)) `) by Th2
.= (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 A2, Th1
.= (((b |^ n) `) \ b) \ (((a |^ n) `) \ a) by BCIALG_1:7
.= ((b |^ (n + 1)) `) \ (((a |^ n) `) \ a) by Th14
.= ((b |^ (n + 1)) `) \ ((a |^ (n + 1)) `) by Th14
.= ((b |^ (n + 1)) \ (a |^ (n + 1))) ` by BCIALG_1:9
.= (a |^ (n + 1)) \ (b |^ (n + 1)) by A3, BCIALG_1:30 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(a \ b) |^ 0 = 0. X by Def1
.= (0. X) ` by BCIALG_1:def 5
.= (a |^ 0) \ (0. X) by Def1 ;
then A4: S₁[ 0 ] by Def1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A1);
hence (a \ b) |^ n = (a |^ n) \ (b |^ n) ; :: thesis: verum