theorem Th18: :: HILB10_6:18

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