let z be Element of COMPLEX ; :: thesis: |.z.| <= (abs (Re z)) + (abs (Im z))
z = (Re z) + ((Im z) * <i>) by COMPLEX1:13;
then A1: |.z.| <= |.((Re z) + (0 * <i>)).| + |.(0 + ((Im z) * <i>)).| by COMPLEX1:56;
( Re (0 + ((Im z) * <i>)) = 0 & Im (0 + ((Im z) * <i>)) = Im z ) by COMPLEX1:12;
hence |.z.| <= (abs (Re z)) + (abs (Im z)) by A1, COMPLEX1:51; :: thesis: verum