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