theorem ConcatIsIncreasing: :: NUMBER12:8

for f being increasing FinSequence of NAT
for x being Nat st ( for i being Nat st i in dom f holds
f . i < x ) holds
f ^ <*x*> is increasing