let a, b be real number ; :: thesis: ( 0 <= a & 0 <= b implies 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b) )
assume A1: ( 0 <= a & 0 <= b ) ; :: thesis: 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)

per cases ( a <> b or a = b ) ;

suppose a <> b ; :: thesis: 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)

hence 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (((sqrt a) ^2 ) - ((sqrt b) ^2 )) by A1, Lm6, Th71
.= ((sqrt a) + (sqrt b)) / (a - ((sqrt b) ^2 )) by A1, Def4
.= ((sqrt a) + (sqrt b)) / (a - b) by A1, Def4 ;
:: thesis: verum

end;

suppose a = b ; :: thesis: 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)

then ( 1 / ((sqrt a) - (sqrt b)) = 0 & ((sqrt a) + (sqrt b)) / (a - b) = 0 ) by XCMPLX_1:49;
hence 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b) ; :: thesis: verum

end;

end;