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