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