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