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:24 ;
z - (z1 - z2) = z + (((- 1q ) * z1) - (- z2)) by A, QUATERN2:19
.= (z + ((- 1q ) * z1)) + z2 by QUATERN2:2 ;
hence z - (z1 - z2) = (z - z1) + z2 by QUATERN2:19; :: thesis: verum