let a, b, m be Nat; :: thesis: (a |^ 2) - (b |^ 2) divides (a |^ (2 * m)) - (b |^ (2 * m))
( a |^ (2 * m) = (a |^ 2) |^ m & b |^ (2 * m) = (b |^ 2) |^ m ) by NEWTON:9;
hence (a |^ 2) - (b |^ 2) divides (a |^ (2 * m)) - (b |^ (2 * m)) by Th32; :: thesis: verum