let a, b be real number ; :: 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, Def4
.= a - b by A2, Def4 ; :: thesis: verum