let z be quaternion number ; :: thesis: |.(z * z).| = |.(z * (z *' )).|
thus |.(z * z).| = |.z.| * |.z.| by Th87
.= |.z.| * |.(z *' ).| by Th73
.= |.(z * (z *' )).| by Th87 ; :: thesis: verum