theorem :: CSSPACE2:13

for seq being Complex_Sequence st seq is absolutely_summable & Sum |.seq.| = 0 holds
for n being Nat holds seq . n = 0c