let n be Nat; :: thesis: for a being non trivial Nat holds ((Px (a,n)) ^2) - (((a ^2) -' 1) * ((Py (a,n)) ^2)) = 1
let a be non trivial Nat; :: thesis: ((Px (a,n)) ^2) - (((a ^2) -' 1) * ((Py (a,n)) ^2)) = 1
set m = min_Pell's_solution_of ((a ^2) -' 1);

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

suppose n = 0 ; :: thesis: ((Px (a,n)) ^2) - (((a ^2) -' 1) * ((Py (a,n)) ^2)) = 1

then ( Px (a,n) = 1 & Py (a,n) = 0 ) by Th6;
hence ((Px (a,n)) ^2) - (((a ^2) -' 1) * ((Py (a,n)) ^2)) = 1 ; :: thesis: verum

end;

suppose A1: n > 0 ; :: thesis: ((Px (a,n)) ^2) - (((a ^2) -' 1) * ((Py (a,n)) ^2)) = 1

(Px (a,n)) + ((Py (a,n)) * (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 Def2;
then reconsider PP = [(Px (a,n)),(Py (a,n))] as positive Pell's_solution of (a ^2) -' 1 by A1, PELLS_EQ:20;
((PP `1) ^2) - (((a ^2) -' 1) * ((PP `2) ^2)) = 1 by PELLS_EQ:def 1;
hence ((Px (a,n)) ^2) - (((a ^2) -' 1) * ((Py (a,n)) ^2)) = 1 ; :: thesis: verum

end;

end;