for a being Ordinal
for f being Ordinal-Sequence st 0 in a & ( for b being Ordinal st b in dom f holds
f . b = a |^|^ b ) holds
f is non-decreasing