let z be quaternion number ; (1 / (|.z.| ^2 )) * (z *' ) = [*((1 / (|.z.| ^2 )) * (Rea z)),(- ((1 / (|.z.| ^2 )) * (Im1 z))),(- ((1 / (|.z.| ^2 )) * (Im2 z))),(- ((1 / (|.z.| ^2 )) * (Im3 z)))*]
set zz = |.z.| ^2 ;
A1:
(1 / (|.z.| ^2 )) * (z *' ) = [*(Rea ((1 / (|.z.| ^2 )) * (z *' ))),(Im1 ((1 / (|.z.| ^2 )) * (z *' ))),(Im2 ((1 / (|.z.| ^2 )) * (z *' ))),(Im3 ((1 / (|.z.| ^2 )) * (z *' )))*]
by QUATERNI:24;
A2:
(1 / (|.z.| ^2 )) * (z *' ) = [*((1 / (|.z.| ^2 )) * (Rea z)),(Im1 ((1 / (|.z.| ^2 )) * (z *' ))),(Im2 ((1 / (|.z.| ^2 )) * (z *' ))),(Im3 ((1 / (|.z.| ^2 )) * (z *' )))*]
by A1, Th24;
A3:
(1 / (|.z.| ^2 )) * (z *' ) = [*((1 / (|.z.| ^2 )) * (Rea z)),(- ((1 / (|.z.| ^2 )) * (Im1 z))),(Im2 ((1 / (|.z.| ^2 )) * (z *' ))),(Im3 ((1 / (|.z.| ^2 )) * (z *' )))*]
by A2, Th25;
A4:
(1 / (|.z.| ^2 )) * (z *' ) = [*((1 / (|.z.| ^2 )) * (Rea z)),(- ((1 / (|.z.| ^2 )) * (Im1 z))),(- ((1 / (|.z.| ^2 )) * (Im2 z))),(Im3 ((1 / (|.z.| ^2 )) * (z *' )))*]
by A3, Th26;
thus
(1 / (|.z.| ^2 )) * (z *' ) = [*((1 / (|.z.| ^2 )) * (Rea z)),(- ((1 / (|.z.| ^2 )) * (Im1 z))),(- ((1 / (|.z.| ^2 )) * (Im2 z))),(- ((1 / (|.z.| ^2 )) * (Im3 z)))*]
by A4, Th27; verum