theorem Th80: :: QUATERNI:87

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