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