for y, z, a being Nat holds
( ( y = Py (a,z) & a > 1 ) iff ex x, x1, y1, A, x2, y2 being Nat st
( a > 1 & [x,y] is Pell's_solution of (a ^2) -' 1 & [x1,y1] is Pell's_solution of (a ^2) -' 1 & y1 >= y & A > y & y >= z & [x2,y2] is Pell's_solution of (A ^2) -' 1 & y2,y are_congruent_mod x1 & A,a are_congruent_mod x1 & y2,z are_congruent_mod 2 * y & A,1 are_congruent_mod 2 * y & y1, 0 are_congruent_mod y ^2 ) )