for U being Universe
for g being Ordinal-Sequence-valued Sequence st dom g <> {} & dom g in U & ( for a being Ordinal st a in dom g holds
g . a is Ordinal-Sequence of U ) holds
lims g is Ordinal-Sequence of U