let m1, m2, m4, m3, n1, n2, n3, n4 be Real; ((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
by Th67;
A2:
(((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2) >= 0
by Th67;
((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 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)))))) + ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2))
by A2, SQUARE_1:def 2
.=
(((((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, A2, SQUARE_1:29
;
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)))))
; verum