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