theorem Th24: :: QUATERN3:24

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