consider n1, n2, n3, n4 being Nat such that
A1:
n = (((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)
by Sum4Sq;
consider m1, m2, m3, m4 being Nat such that
A2:
m = (((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)
by Sum4Sq;
WW:
n * m = (((((((n1 * m1) - (n2 * m2)) - (n3 * m3)) - (n4 * m4)) ^2) + (((((n1 * m2) + (n2 * m1)) + (n3 * m4)) - (n4 * m3)) ^2)) + (((((n1 * m3) - (n2 * m4)) + (n3 * m1)) + (n4 * m2)) ^2)) + (((((n1 * m4) + (n2 * m3)) - (n3 * m2)) + (n4 * m1)) ^2)
by A1, A2;
set z1 = (((n1 * m1) - (n2 * m2)) - (n3 * m3)) - (n4 * m4);
set z2 = (((n1 * m2) + (n2 * m1)) + (n3 * m4)) - (n4 * m3);
set z3 = (((n1 * m3) - (n2 * m4)) + (n3 * m1)) + (n4 * m2);
set z4 = (((n1 * m4) + (n2 * m3)) - (n3 * m2)) + (n4 * m1);
reconsider N1 = |.((((n1 * m1) - (n2 * m2)) - (n3 * m3)) - (n4 * m4)).|, N2 = |.((((n1 * m2) + (n2 * m1)) + (n3 * m4)) - (n4 * m3)).|, N3 = |.((((n1 * m3) - (n2 * m4)) + (n3 * m1)) + (n4 * m2)).|, N4 = |.((((n1 * m4) + (n2 * m3)) - (n3 * m2)) + (n4 * m1)).| as natural Number ;
reconsider N1 = N1, N2 = N2, N3 = N3, N4 = N4 as Nat by TARSKI:1;
( N1 ^2 = ((((n1 * m1) - (n2 * m2)) - (n3 * m3)) - (n4 * m4)) ^2 & N2 ^2 = ((((n1 * m2) + (n2 * m1)) + (n3 * m4)) - (n4 * m3)) ^2 & N3 ^2 = ((((n1 * m3) - (n2 * m4)) + (n3 * m1)) + (n4 * m2)) ^2 & N4 ^2 = ((((n1 * m4) + (n2 * m3)) - (n3 * m2)) + (n4 * m1)) ^2 )
by COMPLEX1:75;
hence
m * n is a_sum_of_four_squares
by WW; verum