theorem Th56: :: COMSEQ_3:56

for seq being Complex_Sequence st seq is summable holds
for z being Complex holds
( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) )