let z1, z2 be quaternion number ; :: thesis: (z1 * z2) " = (z2 " ) * (z1 " )
set z3 = z1 * z2;
A: (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 th9
.= ((((((((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 th10
.= ((((((((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 th11
.= ((((((((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 th12 ;
B1: ((((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:77
.= (((((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:77
.= (((((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:77
.= (((((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:77
.= (((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2 ) ;
B2: ((((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:77
.= (((((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:77
.= (((((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:77
.= (((((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:77
.= (((((Rea z2) * (- (Im1 z1))) + ((- (Im1 z2)) * (Rea z1))) + ((Im2 z2) * (Im3 z1))) - ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2 ) ;
B3: ((((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:77
.= (((((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:77
.= (((((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:77
.= (((((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:77
.= (((((Rea z2) * (- (Im2 z1))) + ((- (Im2 z2)) * (Rea z1))) + ((Im3 z2) * (Im1 z1))) - ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2 ) ;
B4: ((((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:77
.= (((((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:77
.= (((((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:77
.= (((((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:77
.= (((((Rea z2) * (- (Im3 z1))) - ((Im3 z2) * (Rea z1))) + ((Im1 z2) * (Im2 z1))) - ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2 ) ;
(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 B1, B2, B3, B4
.= ((((((((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 ;
hence (z1 * z2) " = (z2 " ) * (z1 " ) by A; :: thesis: verum