:: deftheorem defines Partial_Sums CARDFIL3:def 5 :
for I being non empty set
for L being AbGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for b₄ being Function of ([#] (OrderedFIN I)), the carrier of L holds
( b₄ = Partial_Sums x iff for j being Element of Fin I holds b₄ . j = Sum (x,j) );