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