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