A1: 2 |^ (7 + 7) = (2 |^ 7) * (2 |^ 7) by NEWTON:8;
(128 * 128) - 1 = 43 * 381 ;
then 2 |^ 14,1 are_congruent_mod 43 by A1, Lm7;
then (2 |^ 14) |^ 46,1 |^ 46 are_congruent_mod 43 by GR_CY_3:34;
then (2 |^ 644) * (2 |^ 1),1 * 2 are_congruent_mod 43 by Lm1127, INT_4:11;
hence 43 divides (2 |^ 645) - 2 by Lm1126; :: thesis: verum