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