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

per cases ( a <> 0 or b <> 0 or c <> 0 or d <> 0 ) by A3;

suppose a <> 0 ; :: thesis: contradiction

then A4: 0 < (a ^2 ) + (b ^2 ) by A2, XREAL_1:36, SQUARE_1:74;
0 <= (c ^2 ) + (d ^2 ) by A2;
then 0 < ((a ^2 ) + (b ^2 )) + ((c ^2 ) + (d ^2 )) by A4;
hence contradiction by A1; :: thesis: verum

end;

suppose b <> 0 ; :: thesis: contradiction

then A5: 0 < (a ^2 ) + (b ^2 ) by A2, XREAL_1:36, SQUARE_1:74;
0 <= (c ^2 ) + (d ^2 ) by A2;
then 0 < ((a ^2 ) + (b ^2 )) + ((c ^2 ) + (d ^2 )) by A5;
hence contradiction by A1; :: thesis: verum

end;

suppose c <> 0 ; :: thesis: contradiction

then A6: 0 < (c ^2 ) + (d ^2 ) by A2, XREAL_1:36, SQUARE_1:74;
0 <= (a ^2 ) + (b ^2 ) by A2;
then 0 < ((a ^2 ) + (b ^2 )) + ((c ^2 ) + (d ^2 )) by A6;
hence contradiction by A1; :: thesis: verum

end;

suppose d <> 0 ; :: thesis: contradiction

then A7: 0 < (c ^2 ) + (d ^2 ) by A2, XREAL_1:36, SQUARE_1:74;
0 <= (a ^2 ) + (b ^2 ) by A2;
then 0 < ((a ^2 ) + (b ^2 )) + ((c ^2 ) + (d ^2 )) by A7;
hence contradiction by A1; :: thesis: verum

end;

end;