let n be Nat; :: thesis: card (divisors ((3 |^ ((2 * n) + 1)),4,1)) = card (divisors ((3 |^ ((2 * n) + 1)),4,3))
deffunc H₁( Nat) -> Subset of NAT = divisors ((3 |^ ((2 * n) + 1)),4,1);
deffunc H₂( Nat) -> Subset of NAT = divisors ((3 |^ ((2 * n) + 1)),4,3);
deffunc H₃( Nat) -> set = { (3 |^ m) where m is Nat : ( m is even & m <= (2 * $1) + 1 ) } ;
deffunc H₄( Nat) -> set = { (3 |^ m) where m is Nat : ( m is odd & m <= (2 * $1) + 1 ) } ;
A1: H₁(n) = H₃(n) by Th25;
A2: H₂(n) = H₄(n) by Th26;
card H₃(n) = n + 1 by Th27;
hence card (divisors ((3 |^ ((2 * n) + 1)),4,1)) = card (divisors ((3 |^ ((2 * n) + 1)),4,3)) by A1, A2, Th28; :: thesis: verum