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