let a be non trivial Nat; :: thesis: for y, n being Nat st 1 <= n holds
( y = Py (a,n) iff ex c, d, r, u, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y ) )
let y, n be Nat; :: thesis: ( 1 <= n implies ( y = Py (a,n) iff ex c, d, r, u, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y ) ) )
assume A1: 1 <= n ; :: thesis: ( y = Py (a,n) iff ex c, d, r, u, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y ) )
thus ( y = Py (a,n) implies ex c, d, r, u, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y ) ) :: thesis: ( ex c, d, r, u, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y ) implies y = Py (a,n) )

proof

assume y = Py (a,n) ; :: thesis: ex c, d, r, u, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y )
then consider b, c, d, r, s, t, u, v, x being Nat such that
A2: [x,y] is Pell's_solution of (a ^2) -' 1 and
A3: [u,v] is Pell's_solution of (a ^2) -' 1 and
A4: [s,t] is Pell's_solution of (b ^2) -' 1 and
A5: v = (4 * r) * (y ^2) and
A6: b = a + ((u ^2) * ((u ^2) - a)) and
A7: s = x + (c * u) and
A8: t = n + ((4 * d) * y) and
A9: n <= y by Th27, A1;
A10: ( not b is trivial & u ^2 > a ) by Th26, A1, A2, A3, A4, A5, A6, A7, A8, A9;
A11: ( a ^2 = a * a & b ^2 = b * b & r ^2 = r * r & v ^2 = v * v ) by SQUARE_1:def 1;
then ( a ^2 >= 1 + 0 & b ^2 >= 1 + 0 ) by A10, NAT_1:13;
then A12: ( (a ^2) -' 1 = (a ^2) - 1 & (b ^2) -' 1 = (b ^2) - 1 ) by XREAL_1:233;
take c ; :: thesis: ex d, r, u, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y )
take d ; :: thesis: ex r, u, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y )
take r ; :: thesis: ex u, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y )
take u ; :: thesis: ex x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y )
take x ; :: thesis: ( [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y )
thus [x,y] is Pell's_solution of (a ^2) -' 1 by A2; :: thesis: ( u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y )
(u ^2) - (((a ^2) -' 1) * (v ^2)) = 1 by A3, Lm1;
then u ^2 = (((a ^2) -' 1) * (v ^2)) + 1 ;
hence u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 by A11, A12, A5; :: thesis: ( (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y )
(s ^2) - (((b ^2) - 1) * (t ^2)) = 1 by A12, A4, Lm1;
then s ^2 = (((b ^2) - 1) * (t ^2)) + 1 ;
hence ( (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y ) by A9, A6, A7, A8; :: thesis: verum

end;

given c, d, r, u, x being Nat such that A13: [x,y] is Pell's_solution of (a ^2) -' 1 and
A14: u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 and
A15: (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 and
A16: n <= y ; :: thesis: y = Py (a,n)
consider k being Nat such that
A17: ( x = Px (a,k) & y = Py (a,k) ) by A13, HILB10_1:4;
A18: ( Px (a,0) = 1 & Py (a,0) = 0 ) by HILB10_1:3;
then A19: Px (a,(0 + 1)) = (1 * a) + (0 * ((a ^2) -' 1)) by HILB10_1:6;
A20: y >= 1 by A16, A1, XXREAL_0:2;
k > 0 by A18, A17, A16, A1;
then k >= 1 + 0 by NAT_1:13;
then ( x >= a & a > 1 ) by A17, A19, HILB10_1:10, NEWTON03:def 1;
then A21: x > 1 by XXREAL_0:2;
set v = (4 * r) * (y ^2);
set b = a + ((u ^2) * ((u ^2) - a));
set s = x + (c * u);
set t = n + ((4 * d) * y);
a ^2 = a * a by SQUARE_1:def 1;
then a ^2 >= 1 + 0 by NAT_1:13;
then A22: (a ^2) -' 1 = (a ^2) - 1 by XREAL_1:233;
A23: ( u ^2 = u * u & ((4 * r) * (y ^2)) ^2 = ((4 * r) * (y ^2)) * ((4 * r) * (y ^2)) & r ^2 = r * r & y ^2 = y * y ) by SQUARE_1:def 1;
r <> 0

proof

assume r = 0 ; :: thesis: contradiction
then A24: u = 1 by A14, NAT_1:15, A23;
then (x + (c * u)) * (x + (c * u)) = 1 by A15, A23, SQUARE_1:def 1;
then x + c = 1 + 0 by A24, NAT_1:15;
hence contradiction by A21, XREAL_1:8; :: thesis: verum

end;

then A25: r ^2 >= 1 + 0 by A23, NAT_1:13;
A26: y ^2 >= 1 * 1 by A23, A20, XREAL_1:66;
a * a > a * 1 by XREAL_1:97, NEWTON03:def 1;
then a * a >= a + 1 by NAT_1:13;
then ( (a * a) - 1 >= a & a ^2 = a * a ) by XREAL_1:19, SQUARE_1:def 1;
then 16 * ((a ^2) - 1) >= 1 * a by XREAL_1:66;
then (16 * ((a ^2) - 1)) * (r ^2) >= a * 1 by A25, XREAL_1:66;
then ((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2) >= a * 1 by A26, XREAL_1:66;
then ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 > a * 1 by NAT_1:13, A26, XREAL_1:66;
then (u ^2) - a > 0 by A14, XREAL_1:50;
then a + ((u ^2) * ((u ^2) - a)) >= a + 0 by XREAL_1:7;
then ( a + ((u ^2) * ((u ^2) - a)) > 1 & a + ((u ^2) * ((u ^2) - a)) in NAT ) by NEWTON03:def 1, XXREAL_0:2, INT_1:3;
then reconsider b = a + ((u ^2) * ((u ^2) - a)) as non trivial Element of NAT by NEWTON03:def 1;
b ^2 = b * b by SQUARE_1:def 1;
then b ^2 >= 1 + 0 by NAT_1:13;
then (b ^2) -' 1 = (b ^2) - 1 by XREAL_1:233;
then ((x + (c * u)) ^2) - (((b ^2) -' 1) * ((n + ((4 * d) * y)) ^2)) = 1 by A15;
then A27: [(x + (c * u)),(n + ((4 * d) * y))] is Pell's_solution of (b ^2) -' 1 by Lm1;
u ^2 = (((a ^2) - 1) * (((4 * r) * (y ^2)) ^2)) + 1 by A23, A14;
then (u ^2) - (((a ^2) -' 1) * (((4 * r) * (y ^2)) ^2)) = 1 by A22;
then [u,((4 * r) * (y ^2))] is Pell's_solution of (a ^2) -' 1 by Lm1;
hence y = Py (a,n) by A1, Th26, A27, A13, A16; :: thesis: verum