theorem :: QUATERN2:54

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