let z be quaternion number ; :: thesis: (- z) *' = - (z *' )
A1: ( z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] & (- z) *' = [*(Rea (- z)),(- (Im1 (- z))),(- (Im2 (- z))),(- (Im3 (- z)))*] ) by Th43;
then (- z) *' = [*(- (Rea z)),(- (Im1 (- z))),(- (Im2 (- z))),(- (Im3 (- z)))*] by Th41
.= [*(- (Rea z)),(- (- (Im1 z))),(- (Im2 (- z))),(- (Im3 (- z)))*] by Th41
.= [*(- (Rea z)),(Im1 z),(- (- (Im2 z))),(- (Im3 (- z)))*] by Th41
.= [*(- (Rea z)),(Im1 z),(Im2 z),(- (- (Im3 z)))*] by Th41
.= [*(- (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, Def7
.= 0 by Lm5 ;
hence (- z) *' = - (z *' ) by Def8; :: thesis: verum