5 divides (2 |^ ((4 * n) + 2)) + 1 by Th40;
hence (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is natural ; :: thesis: verum