theorem Th19: :: ORDINAL4:19

for fi being Ordinal-Sequence
for C being Ordinal st C <> {} & ( for A being Ordinal st A in dom fi holds
fi . A = A *^ C ) holds
fi is increasing