let m1, m2, m3, m4, n1, n2, n3, n4 be Real; :: thesis: (sqrt (((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2))) ^2 = ((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2)
((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2) >= 0 by Th67;
hence (sqrt (((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2))) ^2 = ((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2) by SQUARE_1:def 2; :: thesis: verum