let n be Element of NAT ; :: thesis: for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| <= |.z1.| + |.z2.|
let z1, z2 be Element of COMPLEX n; :: thesis: |.(z1 - z2).| <= |.z1.| + |.z2.|
|.(z1 - z2).| <= |.z1.| + |.(- z2).| by Th68;
hence |.(z1 - z2).| <= |.z1.| + |.z2.| by Th61; :: thesis: verum