let z1, z2 be Quaternion; (z1 * z2) " = (z2 ") * (z1 ")
set z3 = z1 * z2;
A1: ((((Rea (z2 ")) * (Im1 (z1 "))) + ((Im1 (z2 ")) * (Rea (z1 ")))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 "))) =
(((((Rea z2) / (|.z2.| ^2)) * (Im1 (z1 "))) + ((Im1 (z2 ")) * (Rea (z1 ")))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((Im1 (z2 ")) * (Rea (z1 ")))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (Rea (z1 ")))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2))))) - ((Im3 (z2 ")) * (Im2 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (Im2 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * ((- (Im1 z1)) / (|.z1.| ^2))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))
by QUATERN2:29
.=
(((((Rea z2) * (- (Im1 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im1 z2)) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))
by XCMPLX_1:76
.=
(((((Rea z2) * (- (Im1 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im1 z2)) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im2 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2)))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))
by XCMPLX_1:76
.=
(((((Rea z2) * (- (Im1 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im1 z2)) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im2 z2) * (Im3 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im3 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))
by XCMPLX_1:76
.=
(((((Rea z2) * (- (Im1 z1))) + ((- (Im1 z2)) * (Rea z1))) + ((Im2 z2) * (Im3 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) * (Im2 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))
by XCMPLX_1:76
.=
(((((Rea z2) * (- (Im1 z1))) + ((- (Im1 z2)) * (Rea z1))) + ((Im2 z2) * (Im3 z1))) - ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2)
;
A2: ((((Rea (z2 ")) * (Im2 (z1 "))) + ((Im2 (z2 ")) * (Rea (z1 ")))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 "))) =
(((((Rea z2) / (|.z2.| ^2)) * (Im2 (z1 "))) + ((Im2 (z2 ")) * (Rea (z1 ")))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((Im2 (z2 ")) * (Rea (z1 ")))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (Rea (z1 ")))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((Im1 (z2 ")) * (Im3 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (Im3 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2))))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * ((- (Im2 z1)) / (|.z1.| ^2))) + (((- (Im2 z2)) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + (((Im3 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2)))
.=
(((((Rea z2) * (- (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im2 z2)) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + (((Im3 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2)))
by XCMPLX_1:76
.=
(((((Rea z2) * (- (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im2 z2)) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im3 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2)))
by XCMPLX_1:76
.=
(((((Rea z2) * (- (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im2 z2)) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im3 z2) * (Im1 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2)))
by XCMPLX_1:76
.=
(((((Rea z2) * (- (Im2 z1))) + ((- (Im2 z2)) * (Rea z1))) + ((Im3 z2) * (Im1 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im1 z2) * (Im3 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))
by XCMPLX_1:76
.=
(((((Rea z2) * (- (Im2 z1))) + ((- (Im2 z2)) * (Rea z1))) + ((Im3 z2) * (Im1 z1))) - ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)
;
A3: ((((Rea (z2 ")) * (Im3 (z1 "))) + ((Im3 (z2 ")) * (Rea (z1 ")))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 "))) =
(((((Rea z2) / (|.z2.| ^2)) * (Im3 (z1 "))) + ((Im3 (z2 ")) * (Rea (z1 ")))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((Im3 (z2 ")) * (Rea (z1 ")))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (Rea (z1 ")))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((Im2 (z2 ")) * (Im1 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (Im1 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * ((- (Im3 z1)) / (|.z1.| ^2))) - (((Im3 z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + (((Im1 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))
.=
(((((Rea z2) * (- (Im3 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + (((Im1 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))
by XCMPLX_1:76
.=
(((((Rea z2) * (- (Im3 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im1 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))
by XCMPLX_1:76
.=
(((((Rea z2) * (- (Im3 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im1 z2) * (Im2 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))
by XCMPLX_1:76
.=
(((((Rea z2) * (- (Im3 z1))) - ((Im3 z2) * (Rea z1))) + ((Im1 z2) * (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im2 z2) * (Im1 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))
by XCMPLX_1:76
.=
(((((Rea z2) * (- (Im3 z1))) - ((Im3 z2) * (Rea z1))) + ((Im1 z2) * (Im2 z1))) - ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2)
;
((((Rea (z2 ")) * (Rea (z1 "))) - ((Im1 (z2 ")) * (Im1 (z1 ")))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 "))) =
(((((Rea z2) / (|.z2.| ^2)) * (Rea (z1 "))) - ((Im1 (z2 ")) * (Im1 (z1 ")))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((Im1 (z2 ")) * (Im1 (z1 ")))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (Im1 (z1 ")))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((Im3 (z2 ")) * (Im3 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (Im3 (z1 ")))
by QUATERN2:29
.=
(((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2))))
by QUATERN2:29
.=
(((((Rea z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im3 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2)))
by XCMPLX_1:76
.=
(((((Rea z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im1 z2) * (Im1 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im3 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2)))
by XCMPLX_1:76
.=
(((((Rea z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im1 z2) * (Im1 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im2 z2) * (Im2 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im3 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2)))
by XCMPLX_1:76
.=
(((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) * (Im3 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))
by XCMPLX_1:76
.=
(((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)
;
then A4: (z2 ") * (z1 ") =
((((((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) + ((- ((((((Rea z2) * (Im1 z1)) + ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2))) * <i>)) + ((- ((((((Rea z2) * (Im2 z1)) + ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) + ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2))) * <j>)) + ((- ((((((Rea z2) * (Im3 z1)) + ((Im3 z2) * (Rea z1))) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2))) * <k>)
by A1, A2, A3, QUATERNI:93
.=
((((((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) + (- (((((((Rea z2) * (Im1 z1)) + ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2)) * <i>))) + ((- ((((((Rea z2) * (Im2 z1)) + ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) + ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2))) * <j>)) + ((- ((((((Rea z2) * (Im3 z1)) + ((Im3 z2) * (Rea z1))) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2))) * <k>)
by QUATERN2:9
.=
((((((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) + (- (((((((Rea z2) * (Im1 z1)) + ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2)) * <i>))) + (- (((((((Rea z2) * (Im2 z1)) + ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) + ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) * <j>))) + ((- ((((((Rea z2) * (Im3 z1)) + ((Im3 z2) * (Rea z1))) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2))) * <k>)
by QUATERN2:9
.=
((((((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) - (((((((Rea z2) * (Im1 z1)) + ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2)) * <i>)) - (((((((Rea z2) * (Im2 z1)) + ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) + ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) * <j>)) - (((((((Rea z2) * (Im3 z1)) + ((Im3 z2) * (Rea z1))) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2)) * <k>)
by QUATERN2:9
;
(z1 * z2) " =
((((Rea (z1 * z2)) / (|.(z1 * z2).| ^2)) - (((Im1 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <i>)) - (((Im2 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <j>)) - (((Im3 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <k>)
by QUATERN2:28
.=
((((Rea (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <i>)) - (((Im2 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <j>)) - (((Im3 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <k>)
by QUATERNI:87
.=
((((Rea (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <i>)) - (((Im2 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <j>)) - (((Im3 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <k>)
by QUATERNI:87
.=
((((Rea (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <i>)) - (((Im2 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <j>)) - (((Im3 (z1 * z2)) / (|.(z1 * z2).| ^2)) * <k>)
by QUATERNI:87
.=
((((Rea (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <i>)) - (((Im2 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <j>)) - (((Im3 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <k>)
by QUATERNI:87
.=
((((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <i>)) - (((Im2 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <j>)) - (((Im3 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <k>)
by QUATERNI:97
.=
((((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) - (((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) / ((|.z1.| * |.z2.|) ^2)) * <i>)) - (((Im2 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <j>)) - (((Im3 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <k>)
by QUATERNI:97
.=
((((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) - (((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) / ((|.z1.| * |.z2.|) ^2)) * <i>)) - (((((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) * <j>)) - (((Im3 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * <k>)
by QUATERNI:97
.=
((((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) - (((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) / ((|.z1.| * |.z2.|) ^2)) * <i>)) - (((((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) * <j>)) - (((((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2))) / ((|.z1.| * |.z2.|) ^2)) * <k>)
by QUATERNI:97
;
hence
(z1 * z2) " = (z2 ") * (z1 ")
by A4; verum