theorem :: QUATERN2:58

for c1, c2, c3 being Quaternion holds (c1 - c2) .|. c3 = (c1 .|. c3) - (c2 .|. c3) by Th23;