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