let z be Quaternion; :: thesis: Rea ((1 / (|.z.| ^2)) * (z *')) = (1 / (|.z.| ^2)) * (Rea 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 Rea ((1 / (|.z.| ^2)) * (z *')) = (1 / (|.z.| ^2)) * (Rea z) by QUATERNI:23; :: thesis: verum