theorem Th7: :: QUATERN2:7

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