let z be quaternion number ; :: thesis: z ~ = |.(z * (z *' )).|
|.(z * z).| = |.(z * (z *' )).| by QUATERNI:89;
hence z ~ = |.(z * (z *' )).| by QUATERNI:88; :: thesis: verum