let z1, z2, z3, z4 be Quaternion; :: thesis: ((z1 - z2) - z3) * z4 = ((z1 * z4) - (z2 * z4)) - (z3 * z4)
((z1 - z2) - z3) * z4 = ((z1 - z2) * z4) - (z3 * z4) by QUATERN2:23
.= ((z1 * z4) - (z2 * z4)) - (z3 * z4) by QUATERN2:23 ;
hence ((z1 - z2) - z3) * z4 = ((z1 * z4) - (z2 * z4)) - (z3 * z4) ; :: thesis: verum