theorem Th21: :: QUATERN2:21

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