theorem :: QUATERN3:29

for z being Quaternion holds z * ((1 / (|.z.| ^2)) * (z *')) = [*((|.z.| ^2) / (|.z.| ^2)),0,0,0*]