let seq be Complex_Sequence; :: thesis: ( ex n being Element of NAT st seq ^\ n is summable implies seq is summable )
given n being Element of NAT such that A1: seq ^\ n is summable ; :: thesis: seq is summable
A2: ( Re (seq ^\ n) is summable & Im (seq ^\ n) is summable ) by A1;
( Re (seq ^\ n) = (Re seq) ^\ n & Im (seq ^\ n) = (Im seq) ^\ n ) by Th23;
then ( Re seq is summable & Im seq is summable ) by A2, SERIES_1:16;
hence seq is summable by Th58; :: thesis: verum