let z be quaternion number ; :: thesis: |.((z *' ) * (z *' )).| = |.z.| ^2
|.((z *' ) * (z *' )).| = |.(z * z).| by thc;
hence |.((z *' ) * (z *' )).| = |.z.| ^2 by QUATERNI:87; :: thesis: verum