theorem :: NUMBER17:77

for s being positive Nat holds (2 |^ (2 |^ ((4 * s) + 1))) + 7 is composite