let z be quaternion number ; :: thesis: Rea ((1 / (|.z.| ^2 )) * (z *' )) = (1 / (|.z.| ^2 )) * (Rea z)
A1: z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by QUATERNI:43;
A2: (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 A1, QUATERNI:def 21;
thus Rea ((1 / (|.z.| ^2 )) * (z *' )) = (1 / (|.z.| ^2 )) * (Rea z) by A2, QUATERNI:23; :: thesis: verum