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