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 Th115;
hence |.(z1 - z2).| <= |.z1.| + |.z2.| by Th108; :: thesis: verum