theorem :: QUATERN3:30

for z1, z2, z3 being Quaternion holds |.((z1 * z2) * z3).| ^2 = ((|.z1.| ^2) * (|.z2.| ^2)) * (|.z3.| ^2)