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