let c be quaternion number ; (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
; verum