let n be 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 :: thesis: for j being Nat st j in Seg n holds
z . j = (n |-> 0c) . j
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 Th57;
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, Th88;
then c = 0c by COMPLEX1:45;
hence z . j = (n |-> 0c) . j ; :: thesis: verum
end;
hence z = 0c n by FINSEQ_2:119; :: thesis: verum