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