let z be quaternion number ; :: thesis: ( Rea (- z) = - (Rea z) & Im1 (- z) = - (Im1 z) & Im2 (- z) = - (Im2 z) & Im3 (- z) = - (Im3 z) )
- z = [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Lm18;
hence ( Rea (- z) = - (Rea z) & Im1 (- z) = - (Im1 z) & Im2 (- z) = - (Im2 z) & Im3 (- z) = - (Im3 z) ) by Th23; :: thesis: verum