theorem :: QUATERN3:34

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