let n be Element of NAT ; :: thesis: for z being Element of COMPLEX n st |.z.| = 0 holds
z = 0c n
let z be Element of COMPLEX n; :: thesis: ( |.z.| = 0 implies z = 0c n )
assume A1: |.z.| = 0 ; :: thesis: z = 0c n

now

let j be Nat; :: thesis: ( j in Seg n implies z . j = (n |-> 0c) . j )
assume A2: j in Seg n ; :: thesis: z . j = (n |-> 0c) . j
then reconsider c = z . j as Element of COMPLEX by Th74;
0 <= Sum (sqr (abs z)) by RVSUM_1:86;
then (abs z) . j = (n |-> 0) . j by A1, RVSUM_1:91, SQUARE_1:24;
then |.c.| = (n |-> 0) . j by A2, Th106;
then c = 0c by A2, COMPLEX1:45, FUNCOP_1:7;
hence z . j = (n |-> 0c) . j by A2, FUNCOP_1:7; :: thesis: verum

end;

hence z = 0c n by FINSEQ_2:119; :: thesis: verum