theorem Th27: :: QUATERN3:27

for z being Quaternion holds Im3 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im3 z))