for p being increasing FinSequence of REAL
for n being Element of NAT st n <= len p holds
p /^ n is increasing FinSequence of REAL