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