let seq be Complex_Sequence; :: thesis: ( seq is summable implies for n being Nat holds seq ^\ n is summable )
assume A1: seq is summable ; :: thesis: for n being Nat holds seq ^\ n is summable
let n be Nat; :: thesis: seq ^\ n is summable
A2: ( Re (seq ^\ n) = (Re seq) ^\ n & Im (seq ^\ n) = (Im seq) ^\ n ) by Th23;
( (Re seq) ^\ n is summable & (Im seq) ^\ n is summable ) by A1, SERIES_1:12;
hence seq ^\ n is summable by A2, Th57; :: thesis: verum