theorem :: QUATERNI:89

for z being quaternion number holds |.(z * z).| = |.(z * (z *')).|