let z1, z2 be Quaternion; :: thesis: - (z1 - z2) = (- z1) + z2
- (z1 - z2) = (- 1q) * (z1 - z2) by QUATERN2:19
.= ((- 1q) * z1) - ((- 1q) * z2) by QUATERN2:24
.= ((- 1q) * z1) - (- z2) by QUATERN2:19 ;
hence - (z1 - z2) = (- z1) + z2 by QUATERN2:19; :: thesis: verum