let z be Quaternion; :: 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