theorem Th11: :: HILB10_8:11

for a being non trivial Nat
for y, n being Nat st y > 0 & n > 0 & (((a ^2) - 1) * (y ^2)) + 1 is square & y,n are_congruent_mod a - 1 & y <= Py (a,(a - 1)) & n <= a - 1 holds
y = Py (a,n)