theorem :: CSSPACE2:9

for seq being Complex_Sequence st seq is summable holds
Sum (seq *') = (Sum seq) *' by Lm5;