theorem Th80: :: SURREALC:80

for r being Sequence of REAL
for y, s being Sequence
for alpha being Ordinal holds
( s | (succ alpha),y,r simplest_on_position alpha iff s,y,r simplest_on_position alpha )