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