let m be Nat; :: thesis: for t, z being Integer holds t - z divides (t |^ m) - (z |^ m)
let t, z be Integer; :: thesis: t - z divides (t |^ m) - (z |^ m)
for n being Nat holds
( t - z divides ((t - z) + z) |^ n iff t - z divides z |^ n ) by Th11;
hence t - z divides (t |^ m) - (z |^ m) by Th10; :: thesis: verum