let c1, c2 be Quaternion; :: thesis: |.(c1 .|. c2).| = |.c1.| * |.c2.|
thus |.(c1 .|. c2).| = |.c1.| * |.(c2 *').| by QUATERNI:87
.= |.c1.| * |.c2.| by QUATERNI:73 ; :: thesis: verum