theorem :: COMPLFLD:62

for z1, z2 being Element of F_Complex holds |.(z1 + z2).| <= |.z1.| + |.z2.| by COMPLEX1:56;