theorem Th25: :: QUATERN3:25

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