let D be non square Nat; :: thesis: for a, b, c, d being Integer st a + (b * (sqrt D)) = c + (d * (sqrt D)) holds
( a = c & b = d )
let a, b, c, d be Integer; :: thesis: ( a + (b * (sqrt D)) = c + (d * (sqrt D)) implies ( a = c & b = d ) )
assume A1: a + (b * (sqrt D)) = c + (d * (sqrt D)) ; :: thesis: ( a = c & b = d )
A2: a - c = (d - b) * (sqrt D) by A1;
(a - c) * (a - c) = ((d - b) * (sqrt D)) * ((d - b) * (sqrt D)) by A1
.= ((d - b) * (d - b)) * ((sqrt D) ^2)
.= ((d - b) * (d - b)) * D by SQUARE_1:def 2 ;
then d - b = 0 ;
then ( d = b & a - c = 0 ) by A2;
hence ( a = c & b = d ) ; :: thesis: verum