let seq be Complex_Sequence; :: thesis: ( seq is summable implies ( seq is convergent & lim seq = 0c ) )
assume seq is summable ; :: thesis: ( seq is convergent & lim seq = 0c )
then Partial_Sums seq is convergent ;
then ( Re (Partial_Sums seq) is convergent & Im (Partial_Sums seq) is convergent ) ;
then ( Partial_Sums (Re seq) is convergent & Partial_Sums (Im seq) is convergent ) by Th26;
then ( Re seq is summable & Im seq is summable ) by SERIES_1:def 2;
then ( Re seq is convergent & lim (Re seq) = 0 & Im seq is convergent & lim (Im seq) = 0 ) by SERIES_1:7;
then ( seq is convergent & Re (lim seq) = 0 & Im (lim seq) = 0 ) by Th42;
hence ( seq is convergent & lim seq = 0c ) by Lm1, COMPLEX1:29; :: thesis: verum