theorem Th18: :: HILB10_8:18

for A being non trivial Nat
for C, B, e being Nat st 0 < B holds
for i, j being Nat
for 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 holds
C = Py (A,B)