theorem :: QUATERN2:28

for r being Quaternion holds r " = ((((Rea r) / (|.r.| ^2)) - (((Im1 r) / (|.r.| ^2)) * <i>)) - (((Im2 r) / (|.r.| ^2)) * <j>)) - (((Im3 r) / (|.r.| ^2)) * <k>)