theorem Th25: :: ORDINAL5:25

for a being Ordinal
for f being Ordinal-Sequence st 1 in a & dom f c= omega & ( for b being Ordinal st b in dom f holds
f . b = a |^|^ b ) holds
f is increasing