theorem :: JORDAN5B:8

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