let z be quaternion number ; (z *' ) " = (z " ) *'
Im1 ((z *' ) " ) = - ((Im1 (z *' )) / (|.(z *' ).| ^2 ))
by QUATERN2:29;
then A2:
Im1 ((z *' ) " ) = - ((- (Im1 z)) / (|.(z *' ).| ^2 ))
by QUATERNI:44;
Im2 ((z *' ) " ) = - ((Im2 (z *' )) / (|.(z *' ).| ^2 ))
by QUATERN2:29;
then A4:
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 A7:
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 A10:
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 A13:
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 A16:
Rea ((z " ) *' ) = (Rea z) / (|.(z *' ).| ^2 )
by QUATERNI:73;
Im3 ((z *' ) " ) = - ((Im3 (z *' )) / (|.(z *' ).| ^2 ))
by QUATERN2:29;
then A18:
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 A2, A4, A18, A16, A10, A7, A13, QUATERNI:25; verum