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