let c1, c2, c3 be Quaternion; :: thesis: c1 * (c2 - c3) = (c1 * c2) - (c1 * c3)
c1 * (c2 - c3) = (c1 * c2) + (c1 * (- c3)) by Th17;
hence c1 * (c2 - c3) = (c1 * c2) - (c1 * c3) by Th21; :: thesis: verum