let n be Element of NAT ; :: thesis: for z being Element of COMPLEX n holds 0 <= |.z.|
let z be Element of COMPLEX n; :: thesis: 0 <= |.z.|
( |.z.| = sqrt (Sum (sqr (abs z))) & 0 <= Sum (sqr (abs z)) ) by RVSUM_1:116;
hence 0 <= |.z.| by SQUARE_1:def 4; :: thesis: verum