theorem :: NUMBER14:25

for f being real-valued increasing FinSequence holds max_p f = len f