let seq be Complex_Sequence; :: thesis: ( ex n being Nat st seq ^\ n is summable implies seq is summable )
given n being Nat such that A1: seq ^\ n is summable ; :: thesis: seq is summable
Im (seq ^\ n) = (Im seq) ^\ n by Th23;
then A2: Im seq is summable by A1, SERIES_1:13;
Re (seq ^\ n) = (Re seq) ^\ n by Th23;
then Re seq is summable by A1, SERIES_1:13;
hence seq is summable by A2, Th57; :: thesis: verum