for n, n1, n2 being Nat
for x, y being Integer
for a being non trivial Nat st n1 < n2 & n2 <= n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) holds
x = y