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