:: deftheorem Def14 defines Sum TOPALG_6:def 14 :
for T being TopStruct
for f being FinSequence of Curves T holds
( ( len f > 0 implies Sum f = (Partial_Sums f) . (len f) ) & ( not len f > 0 implies Sum f = {} ) );