theorem Th9: :: QUATERN2:9

for c being Quaternion
for x1 being Real holds (- x1) * c = - (x1 * c)