let z be Element of COMPLEX ; :: thesis: |.z.| <= (abs (Re z)) + (abs (Im z))
z = (Re z) + ((Im z) * <i> ) by COMPLEX1:29;
then A1: |.z.| <= |.((Re z) + (0 * <i> )).| + |.(0 + ((Im z) * <i> )).| by COMPLEX1:142;
( Re (0 + ((Im z) * <i> )) = 0 & Im (0 + ((Im z) * <i> )) = Im z ) by COMPLEX1:28;
hence |.z.| <= (abs (Re z)) + (abs (Im z)) by A1, COMPLEX1:137; :: thesis: verum