let a, b, c, d be Real; :: 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 by XREAL_1:63;
A3: 0 <= b ^2 by XREAL_1:63;
A4: 0 <= c ^2 by XREAL_1:63;
A5: 0 <= d ^2 by XREAL_1:63;
assume A6: ( 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 A6;

suppose a <> 0 ; :: thesis: contradiction

then 0 < (a ^2) + (b ^2) by A3, SQUARE_1:12, XREAL_1:34;
hence contradiction by A1, A4, A5; :: thesis: verum

end;

suppose b <> 0 ; :: thesis: contradiction

then 0 < (a ^2) + (b ^2) by A2, SQUARE_1:12, XREAL_1:34;
hence contradiction by A1, A4, A5; :: thesis: verum

end;

suppose c <> 0 ; :: thesis: contradiction

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

end;

suppose d <> 0 ; :: thesis: contradiction

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

end;

end;