let c1, c2 be Quaternion; (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