:: deftheorem defines Sum BHSP_4:def 3 :
for X being RealUnitarySpace
for seq being sequence of X holds Sum seq = lim (Partial_Sums seq);