theorem Th13: :: ORDINAL6:13

for a being Ordinal
for f being Ordinal-Sequence st f is non-decreasing holds
f | a is non-decreasing