theorem Th89: :: SURREALC:89

for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence holds Sum (r,y) in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y)