A1: 20 |^ (2 |^ 3) = (20 |^ 2) |^ 4 by Lm3, NEWTON:9;
A2: 20 |^ 2 = 20 * 20 by WSIERP_1:1;
A3: 9 |^ 4 = ((9 * 9) * 9) * 9 by POLYEQ_5:3;
17 + 3,3 are_congruent_mod 17 ;
then 20 * 20,3 * 3 are_congruent_mod 17 by INT_1:18;
then (20 |^ 2) |^ 4,9 |^ 4 are_congruent_mod 17 by A2, GR_CY_3:34;
then A4: ((20 |^ 2) |^ 4) + 1,(9 |^ 4) + 1 are_congruent_mod 17 ;
17 * 386,17 are_congruent_mod 17 by Th33;
hence 17 divides (20 |^ (2 |^ 3)) + 1 by A1, A3, A4, Th32, INT_1:15; :: thesis: verum