let z1, z2, z3, z4 be Quaternion; (z1 - z2) * (z3 - z4) = (z2 - z1) * (z4 - z3)
(z2 - z1) * (z4 - z3) =
((z2 - z1) * z4) - ((z2 - z1) * z3)
by QUATERN2:24
.=
((z2 * z4) - (z1 * z4)) - ((z2 - z1) * z3)
by QUATERN2:23
.=
((z2 * z4) - (z1 * z4)) - ((z2 * z3) - (z1 * z3))
by QUATERN2:23
.=
(((z2 * z4) - (z1 * z4)) - (z2 * z3)) + (z1 * z3)
by Th55
.=
(((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4)
by Th70
;
hence
(z1 - z2) * (z3 - z4) = (z2 - z1) * (z4 - z3)
by Th57; verum