theorem :: SURREALC:78

for r being Sequence of REAL
for y, s being Sequence
for alpha, beta being Ordinal st beta c= alpha & s,y,r simplest_up_to alpha holds
s,y,r simplest_up_to beta ;