theorem Th18: :: QUATERN2:18

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