let z be quaternion number ; z * ((1 / (|.z.| ^2 )) * (z *' )) = [*((|.z.| ^2 ) / (|.z.| ^2 )),0 ,0 ,0 *]
set zz = |.z.| ^2 ;
set z3 = (1 / (|.z.| ^2 )) * (z *' );
z * ((1 / (|.z.| ^2 )) * (z *' )) =
[*(((((Rea z) * (Rea ((1 / (|.z.| ^2 )) * (z *' )))) - ((Im1 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im3 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by QUATERN2:1
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im3 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th24
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im3 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th25
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im3 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th26
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th27
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im1 z)))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th25
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th24
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th27
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th26
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im2 z)))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th26
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th24
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' ))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th25
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2 )) * (z *' )))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th27
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im3 z)))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2 )) * (z *' ))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th27
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im3 z)))) + ((Im3 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2 )) * (z *' ))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th24
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im3 z)))) + ((Im3 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2 )) * (z *' )))))*]
by Th26
.=
[*(((((Rea z) * ((1 / (|.z.| ^2 )) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2 )) * (Im3 z)))) + ((Im3 z) * ((1 / (|.z.| ^2 )) * (Rea z)))) + ((Im1 z) * (- ((1 / (|.z.| ^2 )) * (Im2 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2 )) * (Im1 z)))))*]
by Th25
.=
[*((((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 )) / (|.z.| ^2 )),0 ,0 ,0 *]
.=
[*((|.z.| ^2 ) / (|.z.| ^2 )),0 ,0 ,0 *]
by Th11
;
hence
z * ((1 / (|.z.| ^2 )) * (z *' )) = [*((|.z.| ^2 ) / (|.z.| ^2 )),0 ,0 ,0 *]
; verum