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