let c be quaternion number ; :: thesis: (c *' ) *' = c
A1: ( Rea (c *' ) = Rea c & Im1 (c *' ) = - (Im1 c) & Im2 (c *' ) = - (Im2 c) & Im3 (c *' ) = - (Im3 c) ) by QUATERNI:44;
(c *' ) *' = [*(Rea c),(- (- (Im1 c))),(- (- (Im2 c))),(- (- (Im3 c)))*] by A1, QUATERNI:43
.= c by QUATERNI:24 ;
hence (c *' ) *' = c ; :: thesis: verum