:: deftheorem Def19 defines PartSums INTEGRA1:def 20 :
for p, b₂ being FinSequence of REAL holds
( b₂ = PartSums p iff ( len b₂ = len p & ( for i being Nat st i in dom p holds
b₂ . i = Sum (p | i) ) ) );