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

proof

let a, b, c, d be Integer; :: thesis: ( a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ 0 implies a - (b * (sqrt D)) = (c - (d * (sqrt D))) |^ 0 )
assume A2: a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ 0 ; :: thesis: a - (b * (sqrt D)) = (c - (d * (sqrt D))) |^ 0
( (c + (d * (sqrt D))) |^ 0 = 1 + (0 * (sqrt D)) & 1 + (0 * (sqrt D)) = (c - (d * (sqrt D))) |^ 0 ) by NEWTON:4;
then ( a = 1 & b = 0 ) by Th3, A2;
hence a - (b * (sqrt D)) = (c - (d * (sqrt D))) |^ 0 by NEWTON:4; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
let a, b, c, d be Integer; :: thesis: ( a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ (n + 1) implies a - (b * (sqrt D)) = (c - (d * (sqrt D))) |^ (n + 1) )
assume A5: a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ (n + 1) ; :: thesis: a - (b * (sqrt D)) = (c - (d * (sqrt D))) |^ (n + 1)
set cPd = c + (d * (sqrt D));
set cMd = c - (d * (sqrt D));
consider a1, b1 being Integer such that
A6: a1 + (b1 * (sqrt D)) = (c + (d * (sqrt D))) |^ n by Th5;
A7: D = (sqrt D) ^2 by SQUARE_1:def 2;
a + (b * (sqrt D)) = (c + (d * (sqrt D))) * (a1 + (b1 * (sqrt D))) by A5, A6, NEWTON:6
.= ((c * a1) + ((d * b1) * D)) + ((sqrt D) * ((c * b1) + (d * a1))) by A7 ;
then ( a = (c * a1) + ((d * b1) * D) & b = (c * b1) + (d * a1) ) by Th3;
hence a - (b * (sqrt D)) = (c - (d * (sqrt D))) * (a1 - (b1 * (sqrt D))) by A7
.= (c - (d * (sqrt D))) * ((c - (d * (sqrt D))) |^ n) by A4, A6
.= (c - (d * (sqrt D))) |^ (n + 1) by NEWTON:6 ;
:: thesis: verum

end;

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