theorem :: QUATERN3:28

for z being Quaternion holds (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),(- ((1 / (|.z.| ^2)) * (Im1 z))),(- ((1 / (|.z.| ^2)) * (Im2 z))),(- ((1 / (|.z.| ^2)) * (Im3 z)))*]