theorem :: QUATERN2:59
for c1, c2, c3 being Quaternion holds c1 .|. (c2 - c3) = (c1 .|. c2) - (c1 .|. c3)