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