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