let seq be Complex_Sequence; :: thesis: ( seq is summable implies ( seq is convergent & lim seq = 0c ) )
assume A1: seq is summable ; :: thesis: ( seq is convergent & lim seq = 0c )
then Re (Partial_Sums seq) is convergent ;
then Partial_Sums (Re seq) is convergent by Th26;
then A2: Re seq is summable ;
Im (Partial_Sums seq) is convergent by A1;
then Partial_Sums (Im seq) is convergent by Th26;
then A3: Im seq is summable ;
then lim (Im seq) = 0 by SERIES_1:4;
then A4: Im (lim seq) = 0 by A2, A3, Th42;
lim (Re seq) = 0 by A2, SERIES_1:4;
then Re (lim seq) = 0 by A2, A3, Th42;
hence ( seq is convergent & lim seq = 0c ) by A2, A3, A4, Lm1, Th42, COMPLEX1:13; :: thesis: verum