let a, b be Real; :: thesis: ( 0 <= b & b < a implies 1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (a - b) )
assume that
A1: 0 <= b and
A2: b < a ; :: thesis: 1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (a - b)
thus 1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (((sqrt a) ^2) - ((sqrt b) ^2)) by A1, A2, Lm5, Th10
.= ((sqrt a) - (sqrt b)) / (a - ((sqrt b) ^2)) by A1, A2, Def2
.= ((sqrt a) - (sqrt b)) / (a - b) by A1, Def2 ; :: thesis: verum