let z be Quaternion; :: thesis: |.(- z).| = |.z.|
A1: - z = [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Th55;
then A2: Rea (- z) = - (Rea z) by Th16;
A3: Im1 (- z) = - (Im1 z) by A1, Th16;
A4: Im2 (- z) = - (Im2 z) by A1, Th16;
Im3 (- z) = - (Im3 z) by A1, Th16;
hence |.(- z).| = |.z.| by A2, A3, A4; :: thesis: verum