let z be quaternion number ; :: thesis: z ~ = |.(z *' ).| ^2
|.(z *' ).| ^2 = |.z.| ^2 by QUATERNI:73;
hence z ~ = |.(z *' ).| ^2 by Th4; :: thesis: verum