theorem Th23: :: HILB10_6:23

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