let z1, z2, z3 be quaternion number ; :: thesis: (z1 - z2) * z3 = (z2 - z1) * (- z3)
A1: (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) ;
thus (z1 - z2) * z3 = (z2 - z1) * (- z3) by A1, QUATERN2:23; :: thesis: verum