let a, n be Nat; :: thesis: 7 divides (a |^ ((6 * n) + 1)) - a
6 + 1 divides (a |^ ((6 * n) + 1)) - a by NAT_4:26, Th73;
hence 7 divides (a |^ ((6 * n) + 1)) - a ; :: thesis: verum