theorem :: QUATERN2:53

for c1, c2, c3 being Quaternion holds (c1 + c2) .|. c3 = (c1 .|. c3) + (c2 .|. c3) by Th18;