:: deftheorem defines Sum CLOPBAN3:def 2 :
for X being ComplexNormSpace
for seq being sequence of X holds Sum seq = lim (Partial_Sums seq);