let z be quaternion number ; :: thesis: |.(z *').| = |.z.|
A1: z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Th43;
then A2: Im1 (z *') = - (Im1 z) by Th23;
A3: Im2 (z *') = - (Im2 z) by A1, Th23;
Im3 (z *') = - (Im3 z) by A1, Th23;
hence |.(z *').| = |.z.| by A1, A2, A3, Th23; :: thesis: verum