theorem Th82: :: SURREALC:82

for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence ex s being uSurreal-Sequence st
( dom s = succ ((dom r) /\ (dom y)) & s,y,r simplest_up_to dom s )