4 |^ 2 = 4 * 4 by WSIERP_1:1;
hence 17 divides (4 |^ (2 |^ 1)) + 1 ; :: thesis: verum