theorem Th20: :: HILB10_8:20

for A being non trivial Nat
for C being Nat
for B, L being positive Nat holds
( C = Py (A,B) iff ex i, j being positive 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) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * (j - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 ) )