let c1, c2 be quaternion number ; (c1 - c2) .|. (c1 - c2) = (((c1 .|. c1) - (c1 .|. c2)) - (c2 .|. c1)) + (c2 .|. c2)
(c1 - c2) .|. (c1 - c2) =
(c1 - c2) * ((c1 *' ) - (c2 *' ))
by QUATERNI:56
.=
((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 Th20
.=
((c1 .|. c1) + (- (c2 * (c1 *' )))) + ((- (c1 * (c2 *' ))) + ((- c2) * (- (c2 *' ))))
by Th21
.=
((c1 .|. c1) + (- (c2 .|. c1))) + ((- (c1 .|. c2)) + (c2 .|. c2))
by Th22
.=
(((c1 .|. c1) + (- (c2 .|. c1))) + (- (c1 .|. c2))) + (c2 .|. c2)
by Th2
.=
(((c1 .|. c1) + (- (c1 .|. c2))) + (- (c2 .|. c1))) + (c2 .|. c2)
by Th2
;
hence
(c1 - c2) .|. (c1 - c2) = (((c1 .|. c1) - (c1 .|. c2)) - (c2 .|. c1)) + (c2 .|. c2)
; verum