:: deftheorem defines Sum BHSP_4:def 4 :
for X being RealUnitarySpace
for seq being sequence of X
for n being Nat holds Sum (seq,n) = (Partial_Sums seq) . n;