let z1, z2, z3, z4 be Quaternion; :: thesis: (z1 - z2) * (z3 + z4) = (((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4)
(z1 - z2) * (z3 + z4) = ((z1 - z2) * z3) + ((z1 - z2) * z4) by QUATERN2:17
.= ((z1 * z3) - (z2 * z3)) + ((z1 - z2) * z4) by QUATERN2:23
.= ((z1 * z3) - (z2 * z3)) + ((z1 * z4) - (z2 * z4)) by QUATERN2:23
.= (((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4) by QUATERN2:2 ;
hence (z1 - z2) * (z3 + z4) = (((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4) ; :: thesis: verum