let z be quaternion number ; :: thesis: |.z.| ^2 = |.(z * (z *' )).|
A1: |.(z * z).| = |.(z * (z *' )).| by QUATERNI:89;
|.z.| ^2 = ((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ) by Th1;
hence |.z.| ^2 = |.(z * (z *' )).| by QUATERNI:88, A1; :: thesis: verum