theorem Th1: :: SURREALR:1

for f being Function-yielding c=-monotone Sequence
for o being object st o in dom (union (rng f)) holds
ex A being Ordinal st
( A in dom f & o in dom (f . A) )