theorem Th31: :: NUMBER15:31
for n being Nat holds card (divisors ((3 |^ ((2 * n) + 1)),4,1)) = card (divisors ((3 |^ ((2 * n) + 1)),4,3))