let z1, z2, z3 be quaternion number ; :: thesis: ((z1 * z2) * z3) ~ = ((z1 ~ ) * (z2 ~ )) * (z3 ~ )
((z1 * z2) * z3) ~ = (z1 * (z2 * z3)) ~ by QUATERN2:16
.= (z1 ~ ) * ((z2 * z3) ~ ) by h
.= (z1 ~ ) * ((z2 ~ ) * (z3 ~ )) by h
.= ((z1 ~ ) * (z2 ~ )) * (z3 ~ ) ;
hence ((z1 * z2) * z3) ~ = ((z1 ~ ) * (z2 ~ )) * (z3 ~ ) ; :: thesis: verum