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

proof

assume A2: sqrt (a + b) = 0 ; :: thesis: ( a = 0 & b = 0 )
0 + 0 <= a + b by A1, XREAL_1:9;
then a + b = 0 by A2, SQUARE_1:92;
hence ( a = 0 & b = 0 ) by A1, XREAL_1:29; :: thesis: verum

end;

thus ( a = 0 & b = 0 implies sqrt (a + b) = 0 ) by SQUARE_1:82; :: thesis: verum