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