for n1, n2, n3, n4, m1, m2, m3, m4 being Nat holds ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)) * ((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) = (((((((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) ;