theorem Th7: :: JORDAN5B:7

for f being FinSequence of (TOP-REAL 2)
for P being non empty Subset of (TOP-REAL 2)
for F being Function of I[01],((TOP-REAL 2) | P)
for i being Nat st 1 <= i & i + 1 <= len f & f is being_S-Seq & P = L~ f & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = F .: [.p1,p2.] & F . p1 = f /. i & F . p2 = f /. (i + 1) )