theorem :: SURREALC:93

for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for A being Ordinal st A c= (dom r) /\ (dom y) holds
(Partial_Sums (r,y)) . A = Sum ((r | A),(y | A))