theorem Th17: :: HILB10_6:17

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