theorem Th80: :: QUATERNI:87

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