let c1, c2, c3 be quaternion number ; :: thesis: (c1 - c2) * c3 = (c1 * c3) - (c2 * c3)
(c1 - c2) * c3 = (c1 * c3) + ((- c2) * c3) by Th11;
hence (c1 - c2) * c3 = (c1 * c3) - (c2 * c3) by Thd3; :: thesis: verum