let z1, z2, z3 be Quaternion; :: thesis: |.((z1 * z2) * z3).| = (|.z1.| * |.z2.|) * |.z3.|
|.((z1 * z2) * z3).| = |.(z1 * (z2 * z3)).| by QUATERN2:16
.= |.z1.| * |.(z2 * z3).| by QUATERNI:87
.= |.z1.| * (|.z2.| * |.z3.|) by QUATERNI:87
.= (|.z1.| * |.z2.|) * |.z3.| ;
hence |.((z1 * z2) * z3).| = (|.z1.| * |.z2.|) * |.z3.| ; :: thesis: verum