theorem Th25: :: ORDINAL2:25

for A being Ordinal
for fi being Ordinal-Sequence st A in dom fi holds
fi . A is Ordinal