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