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