let cseq be Complex_Sequence; :: thesis: ( cseq is absolutely_summable & Sum |.cseq.| = 0 implies for n being Element of NAT holds cseq . n = 0c )
assume that
A1: cseq is absolutely_summable and
A2: Sum |.cseq.| = 0 ; :: thesis: for n being Element of NAT holds cseq . n = 0c
reconsider rseq = |.cseq.| as Real_Sequence ;
A3: for n being Element of NAT holds 0 <= |.cseq.| . n

proof

let n be Element of NAT ; :: thesis: 0 <= |.cseq.| . n
0 <= |.(cseq . n).| by COMPLEX1:46;
hence 0 <= |.cseq.| . n by VALUED_1:18; :: thesis: verum

end;

A4: rseq is summable by A1, COMSEQ_3:def 9;
for n being Element of NAT holds cseq . n = 0c

proof

let n be Element of NAT ; :: thesis: cseq . n = 0c
|.cseq.| . n = 0 by A2, A4, A3, RSSPACE:17;
then |.(cseq . n).| = 0 by VALUED_1:18;
hence cseq . n = 0c by COMPLEX1:45; :: thesis: verum

end;

hence for n being Element of NAT holds cseq . n = 0c ; :: thesis: verum