:: deftheorem Def9 defines Ordinal-Sequence-valued ORDINAL6:def 9 :
for g being Function holds
( g is Ordinal-Sequence-valued iff for x being set st x in rng g holds
x is Ordinal-Sequence );