let n be Nat; :: thesis: 7 divides (2 |^ (6 * n)) - 1
(9 * 7) + 1,1 are_congruent_mod 7 ;
then (2 |^ 6) |^ n,1 |^ n are_congruent_mod 7 by Lm5, GR_CY_3:34;
hence 7 divides (2 |^ (6 * n)) - 1 by NEWTON:9; :: thesis: verum