let a, b, n be Nat; :: thesis: a - b divides (a |^ n) - (b |^ n)
defpred S₁[ Nat] means a - b divides (a |^ $1) - (b |^ $1);
A1: S₁[ 0 ] by Lm18b;
A2: for x being Nat st S₁[x] holds
S₁[x + 1]

proof

let x be Nat; :: thesis: ( S₁[x] implies S₁[x + 1] )
( x = 0 or x > 0 ) ;
hence ( S₁[x] implies S₁[x + 1] ) by Lm18f; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A2);
hence a - b divides (a |^ n) - (b |^ n) ; :: thesis: verum