let m1, m2, m4, m3, n1, n2, n3, n4 be real number ; :: thesis: ((sqrt ((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 ))) + (sqrt ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )))) ^2 = ((((((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) + (n1 ^2 )) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )) + (2 * (sqrt (((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) * ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )))))
set a = (((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 );
set b = (((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 );
A1: ( (((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 ) >= 0 & (((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 ) >= 0 ) by Lm21;
((sqrt ((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 ))) + (sqrt ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )))) ^2 = (((sqrt ((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 ))) ^2 ) + ((2 * (sqrt ((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )))) * (sqrt ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 ))))) + ((sqrt ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 ))) ^2 )
.= (((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) + ((2 * (sqrt ((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )))) * (sqrt ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 ))))) + ((sqrt ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 ))) ^2 ) by A1, SQUARE_1:def 4
.= (((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) + (2 * ((sqrt ((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 ))) * (sqrt ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )))))) + ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )) by A1, SQUARE_1:def 4
.= (((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) + (2 * (sqrt (((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) * ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )))))) + ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )) by A1, SQUARE_1:97 ;
hence ((sqrt ((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 ))) + (sqrt ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )))) ^2 = ((((((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) + (n1 ^2 )) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )) + (2 * (sqrt (((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) * ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 ))))) ; :: thesis: verum