let z be Quaternion; :: thesis: (z *') " = (z ") *'
Im1 ((z *') ") = - ((Im1 (z *')) / (|.(z *').| ^2)) by QUATERN2:29;
then A1: Im1 ((z *') ") = - ((- (Im1 z)) / (|.(z *').| ^2)) by QUATERNI:44;
Im2 ((z *') ") = - ((Im2 (z *')) / (|.(z *').| ^2)) by QUATERN2:29;
then A2: Im2 ((z *') ") = - ((- (Im2 z)) / (|.(z *').| ^2)) by QUATERNI:44;
Im2 ((z ") *') = - (Im2 (z ")) by QUATERNI:44;
then Im2 ((z ") *') = - (- ((Im2 z) / (|.z.| ^2))) by QUATERN2:29;
then A3: Im2 ((z ") *') = - (- ((Im2 z) / (|.(z *').| ^2))) by QUATERNI:73;
Im1 ((z ") *') = - (Im1 (z ")) by QUATERNI:44;
then Im1 ((z ") *') = - (- ((Im1 z) / (|.z.| ^2))) by QUATERN2:29;
then A4: Im1 ((z ") *') = - (- ((Im1 z) / (|.(z *').| ^2))) by QUATERNI:73;
Im3 ((z ") *') = - (Im3 (z ")) by QUATERNI:44;
then Im3 ((z ") *') = - (- ((Im3 z) / (|.z.| ^2))) by QUATERN2:29;
then A5: Im3 ((z ") *') = - (- ((Im3 z) / (|.(z *').| ^2))) by QUATERNI:73;
Rea ((z ") *') = Rea (z ") by QUATERNI:44;
then Rea ((z ") *') = (Rea z) / (|.z.| ^2) by QUATERN2:29;
then A6: Rea ((z ") *') = (Rea z) / (|.(z *').| ^2) by QUATERNI:73;
Im3 ((z *') ") = - ((Im3 (z *')) / (|.(z *').| ^2)) by QUATERN2:29;
then A7: Im3 ((z *') ") = - ((- (Im3 z)) / (|.(z *').| ^2)) by QUATERNI:44;
Rea ((z *') ") = (Rea (z *')) / (|.(z *').| ^2) by QUATERN2:29;
then Rea ((z *') ") = (Rea z) / (|.(z *').| ^2) by QUATERNI:44;
hence (z *') " = (z ") *' by A1, A2, A7, A6, A4, A3, A5, QUATERNI:25; :: thesis: verum