theorem Th24: :: QUATERN2:24

for c1, c2, c3 being Quaternion holds c1 * (c2 - c3) = (c1 * c2) - (c1 * c3)