theorem :: HILB10_8:19

for A being non trivial Nat
for C, B, e being Nat st 0 < B holds
( C = Py (A,B) iff ex i, j being Nat ex D, E, F, G, H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * D) * (e + 1)) * (C ^2) & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 ) )