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