theorem Th85: :: SURREALC:85

for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for A being Ordinal holds (Partial_Sums (r,y)) | (succ A) = Partial_Sums ((r | A),(y | A))