let z1, z2 be quaternion number ; :: thesis: (z1 * z2) *' = (z2 *' ) * (z1 *' )
z1 * z2 = [*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),(((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))),(((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))),(((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)))*] by QUATERN2:1;
then a: ( Rea (z1 * z2) = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) & Im1 (z1 * z2) = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)) ) by QUATERNI:23;
A1: (z1 * z2) *' = (((Rea ((z1 * z2) *' )) + ((Im1 ((z1 * z2) *' )) * <i> )) + ((Im2 ((z1 * z2) *' )) * <j> )) + ((Im3 ((z1 * z2) *' )) * <k> ) by QUATERNI:37
.= (((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((Im1 ((z1 * z2) *' )) * <i> )) + ((Im2 ((z1 * z2) *' )) * <j> )) + ((Im3 ((z1 * z2) *' )) * <k> ) by a, QUATERNI:44
.= (((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((- (((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)))) * <i> )) + ((Im2 ((z1 * z2) *' )) * <j> )) + ((Im3 ((z1 * z2) *' )) * <k> ) by a, QUATERNI:44
.= (((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((- (((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)))) * <i> )) + ((- (((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)))) * <j> )) + ((Im3 ((z1 * z2) *' )) * <k> ) by a, QUATERNI:44
.= (((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((- (((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)))) * <i> )) + ((- (((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)))) * <j> )) + ((- (((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)))) * <k> ) by a, QUATERNI:44 ;
A2: ( Rea (z2 *' ) = Rea z2 & Im1 (z2 *' ) = - (Im1 z2) & Im2 (z2 *' ) = - (Im2 z2) & Im3 (z2 *' ) = - (Im3 z2) ) by QUATERNI:44;
( Rea (z1 *' ) = Rea z1 & Im1 (z1 *' ) = - (Im1 z1) & Im2 (z1 *' ) = - (Im2 z1) & Im3 (z1 *' ) = - (Im3 z1) ) by QUATERNI:44;
hence (z1 * z2) *' = (z2 *' ) * (z1 *' ) by A1, A2; :: thesis: verum