let n be Nat; :: thesis: for z being Element of COMPLEX n holds 0 <= |.z.|
let z be Element of COMPLEX n; :: thesis: 0 <= |.z.|
0 <= Sum (sqr (abs z)) by RVSUM_1:86;
hence 0 <= |.z.| by SQUARE_1:def 2; :: thesis: verum