let f be FinSequence of (TOP-REAL 2); :: thesis:
let Q, R be non empty Subset of (TOP-REAL 2); :: thesis:
let F be Function of I[01] ,((TOP-REAL 2) | Q); :: thesis:
let i be Element of NAT ; :: thesis:
let P be non empty Subset of I[01] ; :: thesis:
assume that
A1: f is being_S-Seq and
A2: F is being_homeomorphism and
A3: F . 0 = f /. 1 and
A4: F . 1 = f /. (len f) and
A5: 1 <= i and
A6: i + 1 <= len f and
A7: F .: P = LSeg f,i and
A8: Q = L~ f and
A9: R = LSeg f,i ; :: thesis:
consider ppi, pi1 being Real such that
A10: ppi < pi1 and
A11: 0 <= ppi and
ppi <= 1 and
0 <= pi1 and
A12: pi1 <= 1 and
A13: LSeg f,i = F .: [.ppi,pi1.] and
F . ppi = f /. i and
F . pi1 = f /. (i + 1) by A1, A2, A3, A4, A5, A6, A8, Th7;
ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A10;
then reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01] by A11, A12, BORSUK_1:83, RCOMP_1:def 1, XXREAL_1:34;
A14: the carrier of (I[01] | Poz) = [#] (I[01] | Poz)
.= Poz by PRE_TOPC:def 10 ;
A15: dom F = [#] I[01] by A2, TOPS_2:def 5
.= [.0 ,1.] by BORSUK_1:83 ;
A16: F is one-to-one by A2, TOPS_2:def 5;
then A17: P c= Poz by A7, A13, A15, BORSUK_1:83, FUNCT_1:157;
Poz c= P by A7, A13, A15, A16, BORSUK_1:83, FUNCT_1:157;
then A18: P = Poz by A17, XBOOLE_0:def 10;
set gg = F | P;
reconsider gg = F | P as Function of (I[01] | Poz),((TOP-REAL 2) | Q) by A14, A18, FUNCT_2:38;
reconsider SEG = LSeg f,i as non empty Subset of ((TOP-REAL 2) | Q) by A7, A9;
A19: the carrier of (((TOP-REAL 2) | Q) | SEG) = [#] (((TOP-REAL 2) | Q) | SEG)
.= SEG by PRE_TOPC:def 10 ;
A20: rng gg c= SEG

proof

let ii be set ; :: according to TARSKI:def 3 :: thesis:
assume ii in rng gg ; :: thesis:
then consider j being set such that
A21: j in dom gg and
A22: ii = gg . j by FUNCT_1:def 5;
j in (dom F) /\ Poz by A18, A21, RELAT_1:90;
then j in dom F by XBOOLE_0:def 4;
then F . j in LSeg f,i by A13, A14, A21, FUNCT_1:def 12;
hence ii in SEG by A14, A18, A21, A22, FUNCT_1:72; :: thesis:

end;

reconsider SEG = SEG as non empty Subset of ((TOP-REAL 2) | Q) ;
A23: ((TOP-REAL 2) | Q) | SEG = (TOP-REAL 2) | R by A9, GOBOARD9:4;
reconsider hh9 = gg as Function of (I[01] | Poz),(((TOP-REAL 2) | Q) | SEG) by A19, A20, FUNCT_2:8;
A24: F is continuous by A2, TOPS_2:def 5;
A25: F is one-to-one by A2, TOPS_2:def 5;
gg is continuous by A18, A24, TOPMETR:10;
then A26: hh9 is continuous by TOPMETR:9;
A27: hh9 is one-to-one by A25, FUNCT_1:84;
reconsider hh = hh9 as Function of (I[01] | Poz),((TOP-REAL 2) | R) by A9, GOBOARD9:4;
A28: dom hh = [#] (I[01] | Poz) by FUNCT_2:def 1;
then A29: dom hh = Poz by PRE_TOPC:def 10;
A30: rng hh = hh .: (dom hh) by A28, FUNCT_2:45
.= [#] (((TOP-REAL 2) | Q) | SEG) by A7, A13, A15, A16, A19, A29, BORSUK_1:83, FUNCT_1:157, RELAT_1:162 ;
reconsider A = Closed-Interval-TSpace ppi,pi1 as strict SubSpace of I[01] by A10, A11, A12, TOPMETR:27, TREAL_1:6;
A31: Poz = [#] A by A10, TOPMETR:25;
Closed-Interval-TSpace ppi,pi1 is compact by A10, HEINE:11;
then [#] (Closed-Interval-TSpace ppi,pi1) is compact by COMPTS_1:10;
then for P being Subset of A st P = Poz holds
P is compact by A10, TOPMETR:25;
then Poz is compact by A31, COMPTS_1:11;
then A32: I[01] | Poz is compact by COMPTS_1:12;
(TOP-REAL 2) | R is T_2 by TOPMETR:3;
hence ex G being Function of (I[01] | P),((TOP-REAL 2) | R) st
( G = F | P & G is being_homeomorphism ) by A18, A23, A26, A27, A28, A30, A32, COMPTS_1:26; :: thesis: