let n1, n2 be Nat; :: thesis: for a being non trivial Nat st [n1,n2] is Pell's_solution of (a ^2) -' 1 holds
ex n being Nat st
( n1 = Px (a,n) & n2 = Py (a,n) )
let a be non trivial Nat; :: thesis: ( [n1,n2] is Pell's_solution of (a ^2) -' 1 implies ex n being Nat st
( n1 = Px (a,n) & n2 = Py (a,n) ) )
set D = (a ^2) -' 1;
assume A1: [n1,n2] is Pell's_solution of (a ^2) -' 1 ; :: thesis: ex n being Nat st
( n1 = Px (a,n) & n2 = Py (a,n) )
then reconsider N = [n1,n2] as Pell's_solution of (a ^2) -' 1 ;
A2: (n1 ^2) - (((a ^2) -' 1) * (n2 ^2)) = 1 by A1, Lm3;

per cases ( n2 = 0 or n2 > 0 ) ;

suppose A3: n2 = 0 ; :: thesis: ex n being Nat st
( n1 = Px (a,n) & n2 = Py (a,n) )

then ( n1 <= 1 & n1 >= 1 ) by A2, SQUARE_1:51, NAT_1:14;
then n1 = 1 by XXREAL_0:1;
then ( n1 = Px (a,0) & n2 = Py (a,0) ) by A3, Th6;
hence ex n being Nat st
( n1 = Px (a,n) & n2 = Py (a,n) ) ; :: thesis: verum

end;

suppose n2 > 0 ; :: thesis: ex n being Nat st
( n1 = Px (a,n) & n2 = Py (a,n) )

then N is positive by A2;
then consider n being positive Nat such that
A4: n1 + (n2 * (sqrt ((a ^2) -' 1))) = (((min_Pell's_solution_of ((a ^2) -' 1)) `1) + (((min_Pell's_solution_of ((a ^2) -' 1)) `2) * (sqrt ((a ^2) -' 1)))) |^ n by PELLS_EQ:21;
consider y being Nat such that
A5: (Px (a,n)) + (y * (sqrt ((a ^2) -' 1))) = (((min_Pell's_solution_of ((a ^2) -' 1)) `1) + (((min_Pell's_solution_of ((a ^2) -' 1)) `2) * (sqrt ((a ^2) -' 1)))) |^ n by Def1;
A6: n1 = Px (a,n) by A5, A4, PELLS_EQ:3;
(Px (a,n)) + ((Py (a,n)) * (sqrt ((a ^2) -' 1))) = n1 + (n2 * (sqrt ((a ^2) -' 1))) by A4, Def2;
then n2 = Py (a,n) by PELLS_EQ:3;
hence ex n being Nat st
( n1 = Px (a,n) & n2 = Py (a,n) ) by A6; :: thesis: verum

end;

end;