let z be Quaternion; (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 ;
(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;
then
(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 Th24;
then
(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 Th25;
then
(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 Th26;
hence
(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 Th27; verum