let z be Quaternion; 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 *'))))) * <i>)) + ((((((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 *'))))) * <j>)) + ((((((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 *'))))) * <k>)
by QUATERNI:93
.=
[*(((((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