let a be non trivial Nat; :: thesis: ( Px (a,0) = 1 & Py (a,0) = 0 )
set A = (a ^2) -' 1;
set M = min_Pell's_solution_of ((a ^2) -' 1);
(Px (a,0)) + ((Py (a,0)) * (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)))) |^ 0 by Def2
.= 1 + (0 * (sqrt ((a ^2) -' 1))) by NEWTON:4 ;
hence ( Px (a,0) = 1 & Py (a,0) = 0 ) by PELLS_EQ:3; :: thesis: verum