theorem Th28: :: HILB10_6:28

for a being non trivial Nat
for y, n being Nat st 1 <= n holds
( y = Py (a,n) iff ex c, d, r, u, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y ) )