reconsider A = a as non trivial Nat by A1;
let p1, p2 be Nat; :: thesis: ( ( for b being non trivial Nat st b = a holds
(Px (b,n)) + (p1 * (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 ) & ( for b being non trivial Nat st b = a holds
(Px (b,n)) + (p2 * (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 ) implies p1 = p2 )
assume that
A3: for b being non trivial Nat st b = a holds
(Px (b,n)) + (p1 * (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 and
A4: for b being non trivial Nat st b = a holds
(Px (b,n)) + (p2 * (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 ; :: thesis: p1 = p2
set m = min_Pell's_solution_of ((A ^2) -' 1);
( (Px (A,n)) + (p1 * (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 & (((min_Pell's_solution_of ((A ^2) -' 1)) `1) + (((min_Pell's_solution_of ((A ^2) -' 1)) `2) * (sqrt ((A ^2) -' 1)))) |^ n = (Px (A,n)) + (p2 * (sqrt ((A ^2) -' 1))) ) by A3, A4;
hence p1 = p2 by PELLS_EQ:3; :: thesis: verum