theorem Th17: :: QUATERN2:17

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