reconsider A = a as non trivial Nat by A1;
consider x, y being Nat such that
A2: x + (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 PELLS_EQ:4;
take x ; :: thesis: for b being non trivial Nat st b = a holds
ex y being Nat st x + (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
ex y being Nat st x + (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