theorem :: QUATERNI:89

for z being Quaternion holds |.(z * z).| = |.(z * (z *')).|