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