let n be Nat; :: thesis: 2 |^ (n + 12),2 |^ n are_congruent_mod 65
2 |^ n,2 |^ n are_congruent_mod 65 by INT_1:11;
then (2 |^ n) * (2 |^ 12),(2 |^ n) * 1 are_congruent_mod 65 by Lm1107, Lm1118, INT_1:18;
hence 2 |^ (n + 12),2 |^ n are_congruent_mod 65 by NEWTON:8; :: thesis: verum