theorem Th26: :: QUATERN3:26

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