let z be Quaternion; :: thesis: z " = [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(- ((Im2 z) / (|.z.| ^2))),(- ((Im3 z) / (|.z.| ^2)))*]
z " = [*(Rea (z ")),(Im1 (z ")),(Im2 (z ")),(Im3 (z "))*] by QUATERNI:24
.= [*((Rea z) / (|.z.| ^2)),(Im1 (z ")),(Im2 (z ")),(Im3 (z "))*] by QUATERN2:29
.= [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(Im2 (z ")),(Im3 (z "))*] by QUATERN2:29
.= [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(- ((Im2 z) / (|.z.| ^2))),(Im3 (z "))*] by QUATERN2:29
.= [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(- ((Im2 z) / (|.z.| ^2))),(- ((Im3 z) / (|.z.| ^2)))*] by QUATERN2:29 ;
hence z " = [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(- ((Im2 z) / (|.z.| ^2))),(- ((Im3 z) / (|.z.| ^2)))*] ; :: thesis: verum