theorem Th9: :: INTEGR23:7

for p, q being FinSequence of REAL st len p <= len q & ( for i being Nat st i in dom q holds
( ( i <= len p implies q . i = p . i ) & ( len p < i implies q . i = 0 ) ) ) holds
Sum q = Sum p