let z1, z2, z3 be quaternion number ; :: 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 h
.= (|.z1.| ^2 ) * ((|.z2.| ^2 ) * (|.z3.| ^2 )) by h
.= ((|.z1.| ^2 ) * (|.z2.| ^2 )) * (|.z3.| ^2 ) ;
hence |.((z1 * z2) * z3).| ^2 = ((|.z1.| ^2 ) * (|.z2.| ^2 )) * (|.z3.| ^2 ) ; :: thesis: verum