let seq be Complex_Sequence; :: thesis: ( seq is summable implies for z being Complex holds
( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) ) )
assume A1: seq is summable ; :: thesis: for z being Complex holds
( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) )
let z be Complex; :: thesis: ( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) )
A2: 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 A1, A2; :: thesis: verum