theorem Th15: :: QUATERN2:15

for c being Quaternion holds 1q * c = c