theorem Th23: :: HILB10_1:20
for x being Integer
for a being non trivial Nat st x >= 0 holds
(sgn x) * (Py (a,|.x.|)) = Py (a,|.x.|)