let z be Quaternion; :: thesis: (- z) *' = - (z *')
A1: z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Th36;
(- z) *' = [*(Rea (- z)),(- (Im1 (- z))),(- (Im2 (- z))),(- (Im3 (- z)))*] by Th36;
then (- z) *' = [*(- (Rea z)),(- (Im1 (- z))),(- (Im2 (- z))),(- (Im3 (- z)))*] by Th34
.= [*(- (Rea z)),(- (- (Im1 z))),(- (Im2 (- z))),(- (Im3 (- z)))*] by Th34
.= [*(- (Rea z)),(Im1 z),(- (- (Im2 z))),(- (Im3 (- z)))*] by Th34
.= [*(- (Rea z)),(Im1 z),(Im2 z),(- (- (Im3 z)))*] by Th34
.= [*(- (Rea z)),(Im1 z),(Im2 z),(Im3 z)*] ;
then (z *') + ((- z) *') = [*((Rea z) + (- (Rea z))),((- (Im1 z)) + (Im1 z)),((- (Im2 z)) + (Im2 z)),((- (Im3 z)) + (Im3 z))*] by A1, Def6
.= 0 by Lm6 ;
hence (- z) *' = - (z *') by Def7; :: thesis: verum