let D be Nat; :: thesis: for c, d being Integer
for n being Nat ex a, b being Integer st a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ n
let c, d be Integer; :: thesis: for n being Nat ex a, b being Integer st a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ n
set cd = c + (d * (sqrt D));
defpred S₁[ Nat] means ex a, b being Integer st a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ $1;
A1: S₁[ 0 ]

proof

take 1 ; :: thesis: ex b being Integer st 1 + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ 0
take 0 ; :: thesis: 1 + (0 * (sqrt D)) = (c + (d * (sqrt D))) |^ 0
thus 1 + (0 * (sqrt D)) = (c + (d * (sqrt D))) |^ 0 by NEWTON:4; :: thesis: verum

end;

A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then consider a, b being Integer such that
A3: a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ n ;
A4: D = (sqrt D) ^2 by SQUARE_1:def 2;
(c + (d * (sqrt D))) |^ (n + 1) = (c + (d * (sqrt D))) * (a + (b * (sqrt D))) by A3, NEWTON:6
.= ((c * a) + ((d * b) * D)) + ((sqrt D) * ((c * b) + (a * d))) by A4 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence for n being Nat ex a, b being Integer st a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ n ; :: thesis: verum