let m1, m2, m3, m4, n1, n2, n3, n4 be real number ; :: 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 Lm23;
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 4; :: thesis: verum