let seq be Complex_Sequence; :: thesis: ( seq is summable implies for n being Element of NAT holds seq ^\ n is summable )
assume A1: seq is summable ; :: thesis: for n being Element of NAT holds seq ^\ n is summable

now

let n be Element of 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:15;
hence seq ^\ n is summable by A2, Th58; :: thesis: verum

end;

hence for n being Element of NAT holds seq ^\ n is summable ; :: thesis: verum