let z be quaternion number ; (z *' ) " = (z " ) *'
A1:
Im1 ((z *' ) " ) = - ((Im1 (z *' )) / (|.(z *' ).| ^2 ))
by QUATERN2:29;
A2:
Im1 ((z *' ) " ) = - ((- (Im1 z)) / (|.(z *' ).| ^2 ))
by A1, QUATERNI:44;
A3:
Im2 ((z *' ) " ) = - ((Im2 (z *' )) / (|.(z *' ).| ^2 ))
by QUATERN2:29;
A4:
Im2 ((z *' ) " ) = - ((- (Im2 z)) / (|.(z *' ).| ^2 ))
by A3, QUATERNI:44;
A5:
Im2 ((z " ) *' ) = - (Im2 (z " ))
by QUATERNI:44;
A6:
Im2 ((z " ) *' ) = - (- ((Im2 z) / (|.z.| ^2 )))
by A5, QUATERN2:29;
A7:
Im2 ((z " ) *' ) = - (- ((Im2 z) / (|.(z *' ).| ^2 )))
by A6, QUATERNI:73;
A8:
Im1 ((z " ) *' ) = - (Im1 (z " ))
by QUATERNI:44;
A9:
Im1 ((z " ) *' ) = - (- ((Im1 z) / (|.z.| ^2 )))
by A8, QUATERN2:29;
A10:
Im1 ((z " ) *' ) = - (- ((Im1 z) / (|.(z *' ).| ^2 )))
by A9, QUATERNI:73;
A11:
Im3 ((z " ) *' ) = - (Im3 (z " ))
by QUATERNI:44;
A12:
Im3 ((z " ) *' ) = - (- ((Im3 z) / (|.z.| ^2 )))
by A11, QUATERN2:29;
A13:
Im3 ((z " ) *' ) = - (- ((Im3 z) / (|.(z *' ).| ^2 )))
by A12, QUATERNI:73;
A14:
Rea ((z " ) *' ) = Rea (z " )
by QUATERNI:44;
A15:
Rea ((z " ) *' ) = (Rea z) / (|.z.| ^2 )
by A14, QUATERN2:29;
A16:
Rea ((z " ) *' ) = (Rea z) / (|.(z *' ).| ^2 )
by A15, QUATERNI:73;
A17:
Im3 ((z *' ) " ) = - ((Im3 (z *' )) / (|.(z *' ).| ^2 ))
by QUATERN2:29;
A18:
Im3 ((z *' ) " ) = - ((- (Im3 z)) / (|.(z *' ).| ^2 ))
by A17, QUATERNI:44;
A19:
Rea ((z *' ) " ) = (Rea (z *' )) / (|.(z *' ).| ^2 )
by QUATERN2:29;
A20:
Rea ((z *' ) " ) = (Rea z) / (|.(z *' ).| ^2 )
by A19, QUATERNI:44;
thus
(z *' ) " = (z " ) *'
by A20, A2, A4, A18, A16, A10, A7, A13, QUATERNI:25; verum