for p, q being non empty increasing FinSequence of REAL st p . (len p) < q . 1 holds
p ^ q is non empty increasing FinSequence of REAL