let c1, c2, c3 be Quaternion; :: thesis: c1 .|. (c2 + c3) = (c1 .|. c2) + (c1 .|. c3)
thus c1 .|. (c2 + c3) = c1 * ((c2 *') + (c3 *')) by QUATERNI:54
.= (c1 .|. c2) + (c1 .|. c3) by Th17 ; :: thesis: verum