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