4095 = 13 * 315 ;
then 2 |^ 12,1 are_congruent_mod 13 by Lm12;
then (2 |^ 12) |^ 92,1 |^ 92 are_congruent_mod 13 by GR_CY_3:34;
then (2 |^ 1104) * (2 |^ 1),1 * 2 are_congruent_mod 13 by Lm1132, INT_4:11;
hence 13 divides (2 |^ 1105) - 2 by Lm1128; :: thesis: verum