let a, b be real number ; :: thesis: ( 0 <= a & 0 <= b implies ((sqrt a) - (sqrt b)) * ((sqrt a) + (sqrt b)) = a - b )
assume A1: ( 0 <= a & 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, Def4
.= a - b by A1, Def4 ; :: thesis: verum