let a, b be Real; :: thesis: ( (a ^2) + (b ^2) = 0 implies a = 0 )
( 0 <= a ^2 & 0 <= b ^2 ) by XREAL_1:63;
hence ( (a ^2) + (b ^2) = 0 implies a = 0 ) ; :: thesis: verum