let a, n be Nat; :: thesis: 2 divides (a |^ (n + 1)) - a
1 + 1 divides (a |^ ((n * 1) + 1)) - a by INT_2:28, Th73;
hence 2 divides (a |^ (n + 1)) - a ; :: thesis: verum