theorem Th5: :: SURREALR:5

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