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