theorem Th100: :: SURREALC:100

for x being Surreal ex r being non-zero Sequence of REAL ex y being strictly_decreasing uSurreal-Sequence st
( dom r = dom y & dom y c= born_eq x & Sum (r,y) == x )