let z be quaternion number ; :: thesis: (1 / (z ~ )) * (z *' ) = [*((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Rea z)),(- ((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Im1 z))),(- ((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Im2 z))),(- ((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Im3 z)))*]
(1 / (z ~ )) * (z *' ) = [*(Rea ((1 / (z ~ )) * (z *' ))),(Im1 ((1 / (z ~ )) * (z *' ))),(Im2 ((1 / (z ~ )) * (z *' ))),(Im3 ((1 / (z ~ )) * (z *' )))*] by QUATERNI:24;
then (1 / (z ~ )) * (z *' ) = [*((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Rea z)),(Im1 ((1 / (z ~ )) * (z *' ))),(Im2 ((1 / (z ~ )) * (z *' ))),(Im3 ((1 / (z ~ )) * (z *' )))*] by Th5;
then (1 / (z ~ )) * (z *' ) = [*((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Rea z)),(- ((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Im1 z))),(Im2 ((1 / (z ~ )) * (z *' ))),(Im3 ((1 / (z ~ )) * (z *' )))*] by Th6;
then (1 / (z ~ )) * (z *' ) = [*((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Rea z)),(- ((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Im1 z))),(- ((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Im2 z))),(Im3 ((1 / (z ~ )) * (z *' )))*] by Th7;
hence (1 / (z ~ )) * (z *' ) = [*((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Rea z)),(- ((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Im1 z))),(- ((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Im2 z))),(- ((1 / (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ))) * (Im3 z)))*] by Th8; :: thesis: verum