theorem Th96: :: SURREALC:96

for r being Sequence of REAL
for y being Surreal-Sequence
for s being uSurreal-Sequence
for A being Ordinal st s,y,r simplest_up_to A & A c= succ (dom y) holds
s | A is one-to-one