theorem Th99: :: SURREALC:99
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence holds (dom r) /\ (dom y) c= born (Sum (r,y))