let c1, c2, c3 be quaternion number ; :: thesis: c1 .|. (c2 - c3) = (c1 .|. c2) - (c1 .|. c3)
c1 .|. (c2 - c3) = c1 * ((c2 *' ) - (c3 *' )) by QUATERNI:56
.= (c1 * (c2 *' )) - (c1 * (c3 *' )) by Thd7 ;
hence c1 .|. (c2 - c3) = (c1 .|. c2) - (c1 .|. c3) ; :: thesis: verum