reconsider A = a as non trivial Nat by A1;
consider y being Nat such that
A2: (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;
take y ; :: thesis: for b being non trivial Nat st b = a holds
(Px (b,n)) + (y * (sqrt ((b ^2) -' 1))) = (((min_Pell's_solution_of ((b ^2) -' 1)) `1) + (((min_Pell's_solution_of ((b ^2) -' 1)) `2) * (sqrt ((b ^2) -' 1)))) |^ n
thus for b being non trivial Nat st b = a holds
(Px (b,n)) + (y * (sqrt ((b ^2) -' 1))) = (((min_Pell's_solution_of ((b ^2) -' 1)) `1) + (((min_Pell's_solution_of ((b ^2) -' 1)) `2) * (sqrt ((b ^2) -' 1)))) |^ n by A2; :: thesis: verum