let a, b, m be Nat; :: thesis: a + b divides (a |^ (2 * m)) - (b |^ (2 * m))
A1: a + b divides (a |^ 2) - (b |^ 2) by Lm44;
(a |^ 2) - (b |^ 2) divides (a |^ (2 * m)) - (b |^ (2 * m)) by Th33;
hence a + b divides (a |^ (2 * m)) - (b |^ (2 * m)) by A1, INT_2:9; :: thesis: verum