theorem Th14: :: QUATERN2:14

for c being Quaternion holds c * 1q = c