let n be Nat; :: thesis: card (divisors ((3 |^ ((2 * n) + 1)),4,3)) = n + 1
divisors ((3 |^ ((2 * n) + 1)),4,3) = { (3 |^ m) where m is Nat : ( m is odd & m <= (2 * n) + 1 ) } by Th26;
hence card (divisors ((3 |^ ((2 * n) + 1)),4,3)) = n + 1 by Th28; :: thesis: verum