theorem Th76: :: SURREALC:76

for r being Sequence of REAL
for y, s1, s2 being Sequence
for alpha being Ordinal st s1 . alpha is uSurreal & s2 . alpha is uSurreal & s1 | alpha = s2 | alpha & s1,y,r simplest_on_position alpha & s2,y,r simplest_on_position alpha holds
s1 . alpha = s2 . alpha