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
ex y being Nat st p1 + (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 ) & ( for b being non trivial Nat st b = a holds
ex y being Nat st p2 + (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 ) implies p1 = p2 )
assume that
A3: for b being non trivial Nat st b = a holds
ex y being Nat st p1 + (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 and
A4: for b being non trivial Nat st b = a holds
ex y being Nat st p2 + (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 ; :: thesis: p1 = p2
set m = min_Pell's_solution_of ((A ^2) -' 1);
A5: ex y being Nat st p1 + (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 A3;
ex y being Nat st p2 + (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 A4;
hence p1 = p2 by A5, PELLS_EQ:3; :: thesis: verum