theorem Th8: :: ORDINAL5:8

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 = exp (a,b) ) holds
f is non-decreasing