theorem Th16: :: QUATERN2:16

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