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