A1: 32 |^ 4 = ((32 * 32) * 32) * 32 by POLYEQ_5:3;
1048577 = 17 * 61681 ;
hence 17 divides (32 |^ (2 |^ 2)) + 1 by A1, Lm2; :: thesis: verum