let k be Nat; :: thesis: 17 divides (((34 * k) + 30) |^ (2 |^ 1)) + 1
17 divides (((17 * (2 * k)) + 30) |^ (2 |^ 1)) + 1 by Th34, Lm43;
hence 17 divides (((34 * k) + 30) |^ (2 |^ 1)) + 1 ; :: thesis: verum