theorem Th15: :: HILB10_1:12

for n, k being Nat
for a being non trivial Nat st Py (a,k) = Py (a,n) holds
k = n