theorem Th32: :: HILB10_1:29

for x, y being Integer
for a being non trivial Nat holds (sgn (x + y)) * (Py (a,|.(x + y).|)),(sgn (x - y)) * (Py (a,|.(x - y).|)) are_congruent_mod Px (a,|.x.|)