let z be quaternion number ; :: 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