theorem Th10: :: HILB10_8:10
for n being Nat
for a being non trivial Nat st n <= a holds
ex T being _Theta st Py (a,(n + 1)) = ((2 * a) |^ n) * (1 + (T * (n / a)))