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 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:40, RCOMP_1:def 1, XXREAL_1:34;
A14: the carrier of (I[01] | Poz) = [#] (I[01] | Poz)
.= Poz by PRE_TOPC:def 5 ;
A15: dom F = [#] I[01] by A2, TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40 ;
A16: F is one-to-one by A2, TOPS_2:def 5;
then A17: P c= Poz by A7, A13, A15, BORSUK_1:40, FUNCT_1:87;
Poz c= P by A7, A13, A15, A16, BORSUK_1:40, FUNCT_1:87;
then A18: P = Poz by A17;
set gg = F | P;
reconsider gg = F | P as Function of (I[01] | Poz),((TOP-REAL 2) | Q) by A14, A18, FUNCT_2:32;
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 5 ;
A20: rng gg c= SEG

proof

let ii be object ; :: according to TARSKI:def 3 :: thesis:
assume ii in rng gg ; :: thesis:
then consider j being object such that
A21: j in dom gg and
A22: ii = gg . j by FUNCT_1:def 3;
j in (dom F) /\ Poz by A18, A21, RELAT_1:61;
then j in dom F by XBOOLE_0:def 4;
then F . j in LSeg (f,i) by A13, A14, A21, FUNCT_1:def 6;
hence ii in SEG by A14, A18, A21, A22, FUNCT_1:49; :: 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:2;
reconsider hh9 = gg as Function of (I[01] | Poz),(((TOP-REAL 2) | Q) | SEG) by A19, A20, FUNCT_2:6;
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:7;
then A26: hh9 is continuous by TOPMETR:6;
A27: hh9 is one-to-one by A25, FUNCT_1:52;
reconsider hh = hh9 as Function of (I[01] | Poz),((TOP-REAL 2) | R) by A9, GOBOARD9:2;
A28: dom hh = [#] (I[01] | Poz) by FUNCT_2:def 1;
then A29: dom hh = Poz by PRE_TOPC:def 5;
A30: rng hh = hh .: (dom hh) by A28, RELSET_1:22
.= [#] (((TOP-REAL 2) | Q) | SEG) by A7, A13, A15, A16, A19, A29, BORSUK_1:40, FUNCT_1:87, RELAT_1:129 ;
reconsider A = Closed-Interval-TSpace (ppi,pi1) as strict SubSpace of I[01] by A10, A11, A12, TOPMETR:20, TREAL_1:3;
A31: Poz = [#] A by A10, TOPMETR:18;
Closed-Interval-TSpace (ppi,pi1) is compact by A10, HEINE:4;
then [#] (Closed-Interval-TSpace (ppi,pi1)) is compact by COMPTS_1:1;
then for P being Subset of A st P = Poz holds
P is compact by A10, TOPMETR:18;
then Poz is compact by A31, COMPTS_1:2;
then A32: I[01] | Poz is compact by COMPTS_1:3;
(TOP-REAL 2) | R is T_2 by TOPMETR:2;
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, A30, A32, COMPTS_1:17; :: thesis: