let z be quaternion number ; :: thesis: Im2 ((1 / (z ~ )) * (z *' )) = - ((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Im2 z))
z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by QUATERNI:43;
then (1 / (z ~ )) * (z *' ) = [*((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Rea z)),((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (- (Im1 z))),((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (- (Im2 z))),((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (- (Im3 z)))*] by QUATERNI:def 21;
hence Im2 ((1 / (z ~ )) * (z *' )) = - ((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Im2 z)) by QUATERNI:23; :: thesis: verum