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