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