let z be Quaternion; :: 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