let z be Element of F_Complex; :: thesis: ( 0 <= Re z & Im z = 0 implies |.z.| = Re z )
assume that
A1: 0 <= Re z and
A2: Im z = 0 ; :: thesis: |.z.| = Re z
reconsider a = z as Element of COMPLEX by COMPLFLD:def 1;
|.a.| = |.(Re a).| by A2, COMPLEX1:50;
hence |.z.| = Re z by A1, ABSVALUE:def 1; :: thesis: verum