16 |^ 2 = 16 * 16 by WSIERP_1:1;
hence (16 |^ 2) - 1 = (3 * 5) * 17 ; :: thesis: verum