theorem Th17: :: QUATERN3:17

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