let seq be Complex_Sequence; :: thesis: ( seq is summable implies for z being complex number holds
( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) ) )
assume seq is summable ; :: thesis: for z being complex number holds
( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) )
then A1: Partial_Sums seq is convergent ;
let z be complex number ; :: thesis: ( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) )
A2: z (#) (Partial_Sums seq) is convergent by A1;
A3: Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq) by Th29;
Sum (z (#) seq) = lim (z (#) (Partial_Sums seq)) by Th29
.= z * (Sum seq) by A1, COMSEQ_2:18 ;
hence ( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) ) by A2, A3, Def10; :: thesis: verum