let z be Complex; :: thesis: |.z.| <= |.(Re z).| + |.(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.| <= |.(Re z).| + |.(Im z).| by A1, COMPLEX1:51; :: thesis: verum