let a, b be real number ; :: thesis: ( (a ^2 ) + (b ^2 ) = 0 implies a = 0 )
assume A1: (a ^2 ) + (b ^2 ) = 0 ; :: thesis: a = 0
A2: ( 0 <= a ^2 & 0 <= b ^2 ) by XREAL_1:65;
assume a <> 0 ; :: thesis: contradiction
hence contradiction by A1, A2; :: thesis: verum