let h be FinSequence of (TOP-REAL 2); :: thesis:
set P = L~ h;
set p1 = h /. 1;
deffunc H₁( Nat) -> Subset of (TOP-REAL 2) = L~ (h | ($1 + 2));
defpred S₁[ Nat] means ( 1 <= $1 + 2 & $1 + 2 <= len h implies ex NE being non empty Subset of (TOP-REAL 2) st
( NE = H₁($1) & ex f being Function of I[01] ,((TOP-REAL 2) | NE) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. ($1 + 2) ) ) );
set p2 = h /. (1 + 1);
assume A1: h is being_S-Seq ; :: thesis:
then A2: len h >= 1 + 1 by Def10;
then 1 <= len h by XXREAL_0:2;
then A3: 1 in Seg (len h) by FINSEQ_1:3;
A4: h is one-to-one by A1, Def10;
A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A6: S₁[n] ; :: thesis:
set pn = h /. (n + 2);
set pn1 = h /. ((n + 2) + 1);
A7: (n + 1) + 1 <> (n + 2) + 1 ;
reconsider NE1 = H₁(n) \/ (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1))) as non empty Subset of (TOP-REAL 2) ;
assume that
A8: 1 <= (n + 1) + 2 and
A9: (n + 1) + 2 <= len h ; :: thesis:
A10: (n + 2) + 1 in dom h by A8, A9, FINSEQ_3:27;
A11: (n + 1) + 1 <= (n + 2) + 1 by NAT_1:11;
then consider NE being non empty Subset of (TOP-REAL 2) such that
A12: NE = H₁(n) and
A13: ex f being Function of I[01] ,((TOP-REAL 2) | NE) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (n + 2) ) by A6, A9, NAT_1:11, XXREAL_0:2;
A14: (n + 1) + 1 = n + (1 + 1) ;

now

let x be set ; :: thesis:
assume A15: x in H₁(n) \/ (LSeg h,(n + 2)) ; :: thesis:

now

per cases by A15, XBOOLE_0:def 3;

suppose A16: x in H₁(n) ; :: thesis:

A17: n + 1 <= n + (1 + 1) by XREAL_1:8;
consider X being set such that
A18: x in X and
A19: X in { (LSeg (h | (n + 2)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by A16, TARSKI:def 4;
consider i being Element of NAT such that
A20: X = LSeg (h | (n + 2)),i and
A21: 1 <= i and
A22: i + 1 <= len (h | (n + 2)) by A19;
i + 1 <= (n + 1) + 1 by A9, A11, A22, FINSEQ_1:80, XXREAL_0:2;
then i <= n + 1 by XREAL_1:8;
then A23: i <= n + 2 by A17, XXREAL_0:2;
len (h | (n + 2)) = n + 2 by A9, A11, FINSEQ_1:80, XXREAL_0:2;
then i in Seg (len (h | (n + 2))) by A21, A23, FINSEQ_1:3;
then A24: i in dom (h | (n + 2)) by FINSEQ_1:def 3;
set p19 = (h | (n + 2)) /. i;
set p29 = (h | (n + 2)) /. (i + 1);
A25: n + 2 <= (n + 2) + 1 by NAT_1:11;
then i <= (n + 1) + 2 by A23, XXREAL_0:2;
then i in Seg ((n + 1) + 2) by A21, FINSEQ_1:3;
then i in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:80;
then i in dom (h | ((n + 1) + 2)) by FINSEQ_1:def 3;
then A26: (h | ((n + 1) + 2)) /. i = h /. i by FINSEQ_4:85
.= (h | (n + 2)) /. i by A24, FINSEQ_4:85 ;
i + 1 <= n + 2 by A9, A11, A22, FINSEQ_1:80, XXREAL_0:2;
then A27: i + 1 <= (n + 1) + 2 by A25, XXREAL_0:2;
A28: len (h | ((n + 1) + 2)) = (n + 1) + 2 by A9, FINSEQ_1:80;
A29: len (h | ((n + 1) + 2)) = n + (1 + 2) by A9, FINSEQ_1:80;
A30: n + 2 <= n + 3 by XREAL_1:8;
1 <= i + 1 by NAT_1:11;
then i + 1 in Seg (len (h | (n + 2))) by A22, FINSEQ_1:3;
then A31: i + 1 in dom (h | (n + 2)) by FINSEQ_1:def 3;
1 <= 1 + i by NAT_1:11;
then i + 1 in Seg ((n + 1) + 2) by A27, FINSEQ_1:3;
then i + 1 in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:80;
then i + 1 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def 3;
then A32: (h | ((n + 1) + 2)) /. (i + 1) = h /. (i + 1) by FINSEQ_4:85
.= (h | (n + 2)) /. (i + 1) by A31, FINSEQ_4:85 ;
i + 1 <= n + (1 + 1) by A9, A11, A22, FINSEQ_1:80, XXREAL_0:2;
then A33: i + 1 <= len (h | ((n + 1) + 2)) by A29, A30, XXREAL_0:2;
X = LSeg ((h | (n + 2)) /. i),((h | (n + 2)) /. (i + 1)) by A20, A21, A22, Def5
.= LSeg (h | ((n + 1) + 2)),i by A21, A27, A28, A26, A32, Def5 ;
then X in { (LSeg (h | ((n + 1) + 2)),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (h | ((n + 1) + 2)) ) } by A21, A33;
hence x in H₁(n + 1) by A18, TARSKI:def 4; :: thesis:

end;

suppose A34: x in LSeg h,(n + 2) ; :: thesis:

A35: 1 <= n + 2 by A14, NAT_1:11;
A36: len (h | ((n + 1) + 2)) = (n + 1) + 2 by A9, FINSEQ_1:80;
then (n + 2) + 1 in Seg (len (h | ((n + 1) + 2))) by A8, FINSEQ_1:3;
then A37: (n + 2) + 1 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def 3;
then A38: (n + 2) + 1 <= len (h | ((n + 1) + 2)) by FINSEQ_3:27;
n + 2 <= (n + 2) + 1 by NAT_1:11;
then n + 2 in Seg (len (h | ((n + 1) + 2))) by A36, A35, FINSEQ_1:3;
then A39: n + 2 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def 3;
then A40: 1 <= n + 2 by FINSEQ_3:27;
A41: h /. ((n + 2) + 1) = (h | ((n + 1) + 2)) /. ((n + 2) + 1) by A37, FINSEQ_4:85;
A42: h /. (n + 2) = (h | ((n + 1) + 2)) /. (n + 2) by A39, FINSEQ_4:85;
LSeg h,(n + 2) = LSeg (h /. (n + 2)),(h /. ((n + 2) + 1)) by A9, A35, Def5
.= LSeg (h | ((n + 1) + 2)),(n + 2) by A36, A35, A42, A41, Def5 ;
then LSeg h,(n + 2) in { (LSeg (h | ((n + 1) + 2)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | ((n + 1) + 2)) ) } by A40, A38;
hence x in H₁(n + 1) by A34, TARSKI:def 4; :: thesis:

end;

hence x in H₁(n + 1) ; :: thesis:

end;

then A43: H₁(n) \/ (LSeg h,(n + 2)) c= H₁(n + 1) by TARSKI:def 3;
take NE1 ; :: thesis:
A44: 1 <= (n + 1) + 1 by NAT_1:11;

now

let x be set ; :: thesis:
A45: n + (1 + 1) = (n + 1) + 1 ;
A46: (len (h | ((n + 1) + 2))) - 1 = ((n + 1) + 2) - 1 by A9, FINSEQ_1:80
.= n + (1 + 1) ;
assume x in H₁(n + 1) ; :: thesis:
then consider X being set such that
A47: x in X and
A48: X in { (LSeg (h | ((n + 1) + 2)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | ((n + 1) + 2)) ) } by TARSKI:def 4;
consider i being Element of NAT such that
A49: X = LSeg (h | ((n + 1) + 2)),i and
A50: 1 <= i and
A51: i + 1 <= len (h | ((n + 1) + 2)) by A48;
(i + 1) - 1 = i ;
then A52: i <= (len (h | ((n + 1) + 2))) - 1 by A51, XREAL_1:11;

now

per cases by A52, A46, A45, NAT_1:8;

suppose A53: i = n + 2 ; :: thesis:

A54: len (h | ((n + 1) + 2)) = (n + 1) + 2 by A9, FINSEQ_1:80;
1 <= (n + 2) + 1 by NAT_1:11;
then (n + 2) + 1 in Seg (len (h | ((n + 1) + 2))) by A54, FINSEQ_1:3;
then (n + 2) + 1 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def 3;
then A55: (h | ((n + 1) + 2)) /. ((n + 2) + 1) = h /. (n + (2 + 1)) by FINSEQ_4:85;
A56: 1 <= n + 2 by A14, NAT_1:11;
(n + 1) + 2 = (n + 2) + 1 ;
then n + 2 <= (n + 1) + 2 by NAT_1:11;
then n + 2 in Seg (len (h | ((n + 1) + 2))) by A54, A56, FINSEQ_1:3;
then n + 2 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def 3;
then (h | ((n + 1) + 2)) /. (n + 2) = h /. (n + 2) by FINSEQ_4:85;
then LSeg (h | ((n + 1) + 2)),(n + 2) = LSeg (h /. (n + 2)),(h /. ((n + 2) + 1)) by A54, A56, A55, Def5
.= LSeg h,(n + 2) by A9, A44, Def5 ;
hence x in H₁(n) \/ (LSeg h,(n + 2)) by A47, A49, A53, XBOOLE_0:def 3; :: thesis:

end;

suppose A57: i <= n + 1 ; :: thesis:

then i + 1 <= (n + 1) + 1 by XREAL_1:8;
then i + 1 <= len (h | (n + 2)) by A9, A11, FINSEQ_1:80, XXREAL_0:2;
then A58: LSeg (h | (n + 2)),i in { (LSeg (h | (n + 2)),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (h | (n + 2)) ) } by A50;
set p19 = (h | (n + 2)) /. i;
set p29 = (h | (n + 2)) /. (i + 1);
A59: 1 <= 1 + i by NAT_1:11;
A60: len (h | (n + 2)) = n + (1 + 1) by A9, A11, FINSEQ_1:80, XXREAL_0:2;
n + 1 <= (n + 1) + 1 by NAT_1:11;
then A61: i <= n + 2 by A57, XXREAL_0:2;
then i in Seg (len (h | (n + 2))) by A50, A60, FINSEQ_1:3;
then A62: i in dom (h | (n + 2)) by FINSEQ_1:def 3;
A63: i + 1 <= (n + 1) + 1 by A57, XREAL_1:9;
then i + 1 in Seg (len (h | (n + 2))) by A60, A59, FINSEQ_1:3;
then A64: i + 1 in dom (h | (n + 2)) by FINSEQ_1:def 3;
n + 2 <= (n + 2) + 1 by NAT_1:11;
then i <= (n + 1) + 2 by A61, XXREAL_0:2;
then i in Seg ((n + 1) + 2) by A50, FINSEQ_1:3;
then i in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:80;
then i in dom (h | ((n + 1) + 2)) by FINSEQ_1:def 3;
then A65: (h | ((n + 1) + 2)) /. i = h /. i by FINSEQ_4:85
.= (h | (n + 2)) /. i by A62, FINSEQ_4:85 ;
i + 1 <= (n + 1) + 2 by A57, XREAL_1:9;
then i + 1 in Seg ((n + 1) + 2) by A59, FINSEQ_1:3;
then i + 1 in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:80;
then i + 1 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def 3;
then A66: (h | ((n + 1) + 2)) /. (i + 1) = h /. (i + 1) by FINSEQ_4:85
.= (h | (n + 2)) /. (i + 1) by A64, FINSEQ_4:85 ;
LSeg (h | (n + 2)),i = LSeg ((h | (n + 2)) /. i),((h | (n + 2)) /. (i + 1)) by A50, A60, A63, Def5
.= LSeg (h | ((n + 1) + 2)),i by A50, A51, A65, A66, Def5 ;
then x in union { (LSeg (h | (n + 2)),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (h | (n + 2)) ) } by A47, A49, A58, TARSKI:def 4;
hence x in H₁(n) \/ (LSeg h,(n + 2)) by XBOOLE_0:def 3; :: thesis:

end;

hence x in H₁(n) \/ (LSeg h,(n + 2)) ; :: thesis:

end;

then H₁(n + 1) c= H₁(n) \/ (LSeg h,(n + 2)) by TARSKI:def 3;
then H₁(n + 1) = H₁(n) \/ (LSeg h,(n + 2)) by A43, XBOOLE_0:def 10;
hence NE1 = H₁(n + 1) by A9, A44, Def5; :: thesis:
A67: (n + 1) + 1 <= len h by A9, A11, XXREAL_0:2;
then (n + 1) + 1 in dom h by A44, FINSEQ_3:27;
then LSeg (h /. (n + 2)),(h /. ((n + 2) + 1)) is_an_arc_of h /. (n + 2),h /. ((n + 2) + 1) by A4, A7, A10, Th15, PARTFUN2:17;
then consider f1 being Function of I[01] ,((TOP-REAL 2) | (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1)))) such that
A68: f1 is being_homeomorphism and
A69: f1 . 0 = h /. (n + 2) and
A70: f1 . 1 = h /. ((n + 2) + 1) by Def2;
consider f being Function of I[01] ,((TOP-REAL 2) | NE) such that
f is being_homeomorphism and
A71: f . 0 = h /. 1 and
f . 1 = h /. (n + 2) by A13;
for x being set holds
( x in H₁(n) /\ (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1))) iff x = h /. (n + 2) )

proof

let x be set ; :: thesis:
A72: 1 <= n + 1 by NAT_1:11;
thus ( x in H₁(n) /\ (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1))) implies x = h /. (n + 2) ) :: thesis:

proof

A73: 1 <= n + 1 by NAT_1:11;
h is unfolded by A1, Def10;
then A74: (LSeg h,(n + 1)) /\ (LSeg h,((n + 1) + 1)) = {(h /. ((n + 1) + 1))} by A9, A73, Def8;
A75: (n + 1) + 1 <= len h by A9, A11, XXREAL_0:2;
assume A76: x in H₁(n) /\ (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1))) ; :: thesis:
then A77: x in LSeg (h /. (n + 2)),(h /. ((n + 2) + 1)) by XBOOLE_0:def 4;
A78: LSeg (h /. (n + 2)),(h /. ((n + 2) + 1)) = LSeg h,((n + 1) + 1) by A9, A44, Def5;
set p19 = h /. (n + 1);
set p29 = h /. ((n + 1) + 1);
A79: 1 <= 1 + n by NAT_1:11;
x in H₁(n) by A76, XBOOLE_0:def 4;
then consider X being set such that
A80: x in X and
A81: X in { (LSeg (h | (n + 2)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by TARSKI:def 4;
consider i being Element of NAT such that
A82: X = LSeg (h | (n + 2)),i and
A83: 1 <= i and
A84: i + 1 <= len (h | (n + 2)) by A81;
A85: len (h | (n + 2)) = n + (1 + 1) by A9, A11, FINSEQ_1:80, XXREAL_0:2;
n + 1 <= (n + 1) + 1 by NAT_1:11;
then n + 1 in Seg (len (h | (n + 2))) by A85, A79, FINSEQ_1:3;
then n + 1 in dom (h | (n + 2)) by FINSEQ_1:def 3;
then A86: (h | (n + 2)) /. (n + 1) = h /. (n + 1) by FINSEQ_4:85;
1 <= 1 + (n + 1) by NAT_1:11;
then (n + 1) + 1 in Seg (len (h | (n + 2))) by A85, FINSEQ_1:3;
then (n + 1) + 1 in dom (h | (n + 2)) by FINSEQ_1:def 3;
then A87: (h | (n + 2)) /. ((n + 1) + 1) = h /. ((n + 1) + 1) by FINSEQ_4:85;
A88: len (h | (n + 2)) = (n + 1) + 1 by A9, A11, FINSEQ_1:80, XXREAL_0:2;
then A89: i <= n + 1 by A84, XREAL_1:8;
then 1 <= n + 1 by A83, XXREAL_0:2;
then A90: LSeg h,(n + 1) = LSeg (h /. (n + 1)),(h /. ((n + 1) + 1)) by A75, Def5
.= LSeg (h | (n + 2)),(n + 1) by A85, A79, A86, A87, Def5 ;
A91: h is s.n.c. by A1, Def10;

now

set p19 = h /. i;
set p29 = h /. (i + 1);
assume A92: i < n + 1 ; :: thesis:
then A93: i + 1 < (n + 1) + 1 by XREAL_1:8;
n + 1 <= (n + 1) + 1 by NAT_1:11;
then i <= n + 2 by A92, XXREAL_0:2;
then i in Seg (len (h | (n + 2))) by A83, A85, FINSEQ_1:3;
then i in dom (h | (n + 2)) by FINSEQ_1:def 3;
then A94: (h | (n + 2)) /. i = h /. i by FINSEQ_4:85;
A95: LSeg h,(n + 2) = LSeg (h /. (n + 2)),(h /. ((n + 2) + 1)) by A9, A44, Def5;
1 <= 1 + i by NAT_1:11;
then i + 1 in Seg (len (h | (n + 2))) by A84, FINSEQ_1:3;
then i + 1 in dom (h | (n + 2)) by FINSEQ_1:def 3;
then A96: (h | (n + 2)) /. (i + 1) = h /. (i + 1) by FINSEQ_4:85;
i + 1 <= len h by A67, A84, A88, XXREAL_0:2;
then LSeg h,i = LSeg (h /. i),(h /. (i + 1)) by A83, Def5
.= LSeg (h | (n + 2)),i by A83, A84, A94, A96, Def5 ;
then LSeg (h | (n + 2)),i misses LSeg (h /. (n + 2)),(h /. ((n + 2) + 1)) by A91, A93, A95, Def9;
hence contradiction by A77, A80, A82, XBOOLE_0:3; :: thesis:

end;

then i = n + 1 by A89, XXREAL_0:1;
then x in (LSeg h,(n + 1)) /\ (LSeg h,((n + 1) + 1)) by A77, A80, A82, A90, A78, XBOOLE_0:def 4;
hence x = h /. (n + 2) by A74, TARSKI:def 1; :: thesis:

end;

assume A97: x = h /. (n + 2) ; :: thesis:
A98: 1 <= n + 1 by NAT_1:11;
(n + 1) + 1 <= len (h | (n + 2)) by A9, A11, FINSEQ_1:80, XXREAL_0:2;
then A99: LSeg (h | (n + 2)),(n + 1) in { (LSeg (h | (n + 2)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by A98;
A100: n + 2 in Seg (n + 2) by A44, FINSEQ_1:3;
A101: len (h | (n + 2)) = n + 2 by A9, A11, FINSEQ_1:80, XXREAL_0:2;
then dom (h | (n + 2)) = Seg (n + 2) by FINSEQ_1:def 3;
then x = (h | (n + 2)) /. ((n + 1) + 1) by A97, A100, FINSEQ_4:85;
then x in LSeg (h | (n + 2)),(n + 1) by A101, A72, Th27;
then A102: x in union { (LSeg (h | (n + 2)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by A99, TARSKI:def 4;
x in LSeg (h /. (n + 2)),(h /. ((n + 2) + 1)) by A97, RLTOPSP1:69;
hence x in H₁(n) /\ (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1))) by A102, XBOOLE_0:def 4; :: thesis:

end;

then H₁(n) /\ (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1))) = {(h /. (n + 2))} by TARSKI:def 1;
then consider hh being Function of I[01] ,((TOP-REAL 2) | NE1) such that
A103: hh is being_homeomorphism and
A104: hh . 0 = f . 0 and
A105: hh . 1 = f1 . 1 by A12, A13, A71, A68, A69, TOPMETR2:6;
take hh ; :: thesis:
thus ( hh is being_homeomorphism & hh . 0 = h /. 1 & hh . 1 = h /. ((n + 1) + 2) ) by A71, A70, A103, A104, A105; :: thesis:

end;

h | 2 = h | (Seg 2) by FINSEQ_1:def 15;
then A106: dom (h | 2) = (dom h) /\ (Seg 2) by RELAT_1:90
.= (Seg (len h)) /\ (Seg 2) by FINSEQ_1:def 3
.= Seg 2 by A2, FINSEQ_1:9 ;
then A107: len (h | 2) = 1 + 1 by FINSEQ_1:def 3;
then A108: 2 in Seg (len (h | 2)) by FINSEQ_1:3;
A109: 1 in Seg (len (h | 2)) by A107, FINSEQ_1:3;

now

let x be set ; :: thesis:
A110: h /. (1 + 1) = (h | 2) /. 2 by A106, A107, A108, FINSEQ_4:85;
thus ( x in { (LSeg (h | 2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } implies x = LSeg h,1 ) :: thesis:

proof

assume x in { (LSeg (h | 2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } ; :: thesis:
then consider i being Element of NAT such that
A111: x = LSeg (h | 2),i and
A112: 1 <= i and
A113: i + 1 <= len (h | 2) ;
i + 1 <= 1 + 1 by A106, A113, FINSEQ_1:def 3;
then i <= 1 by XREAL_1:8;
then A114: 1 = i by A112, XXREAL_0:1;
A115: (h | 2) /. (1 + 1) = h /. (1 + 1) by A106, A107, A108, FINSEQ_4:85;
(h | 2) /. 1 = h /. 1 by A106, A107, A109, FINSEQ_4:85;
hence x = LSeg (h /. 1),(h /. (1 + 1)) by A107, A111, A114, A115, Def5
.= LSeg h,1 by A2, Def5 ;
:: thesis:

end;

assume x = LSeg h,1 ; :: thesis:
then A116: x = LSeg (h /. 1),(h /. (1 + 1)) by A2, Def5;
h /. 1 = (h | 2) /. 1 by A106, A107, A109, FINSEQ_4:85;
then x = LSeg (h | 2),1 by A107, A116, A110, Def5;
hence x in { (LSeg (h | 2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } by A107; :: thesis:

end;

then { (LSeg (h | 2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } = {(LSeg h,1)} by TARSKI:def 1;
then A117: H₁( 0 ) = LSeg h,1 by ZFMISC_1:31
.= LSeg (h /. 1),(h /. (1 + 1)) by A2, Def5 ;
A118: 1 + 1 in Seg (len h) by A2, FINSEQ_1:3;
( 1 <= 0 + 2 & 0 + 2 <= len h implies ex f being Function of I[01] ,((TOP-REAL 2) | (LSeg (h /. 1),(h /. (1 + 1)))) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (0 + 2) ) )

proof

assume that
1 <= 0 + 2 and
0 + 2 <= len h ; :: thesis:
A119: 2 in dom h by A118, FINSEQ_1:def 3;
1 in dom h by A3, FINSEQ_1:def 3;
then LSeg (h /. 1),(h /. (1 + 1)) is_an_arc_of h /. 1,h /. (1 + 1) by A4, A119, Th15, PARTFUN2:17;
hence ex f being Function of I[01] ,((TOP-REAL 2) | (LSeg (h /. 1),(h /. (1 + 1)))) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (0 + 2) ) by Def2; :: thesis:

end;

then A120: S₁[ 0 ] by A117;
A121: for n being Nat holds S₁[n] from NAT_1:sch 2(A120, A5);
(len h) - 2 in NAT by A2, INT_1:18;
then reconsider h1 = (len h) - 2 as Nat ;
1 <= h1 + 2 by NAT_1:12;
then consider NE being non empty Subset of (TOP-REAL 2) such that
A122: NE = H₁(h1) and
A123: ex f being Function of I[01] ,((TOP-REAL 2) | NE) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (h1 + 2) ) by A121;
consider f being Function of I[01] ,((TOP-REAL 2) | NE) such that
A124: f is being_homeomorphism and
A125: f . 0 = h /. 1 and
A126: f . 1 = h /. (h1 + 2) by A123;
A127: h | (len h) = h | (Seg (len h)) by FINSEQ_1:def 15
.= h | (dom h) by FINSEQ_1:def 3
.= h by RELAT_1:97 ;
then reconsider f = f as Function of I[01] ,((TOP-REAL 2) | (L~ h)) by A122;
take f ; :: according to TOPREAL1:def 2 :: thesis:
thus f is being_homeomorphism by A122, A124, A127; :: thesis:
thus ( f . 0 = h /. 1 & f . 1 = h /. (len h) ) by A125, A126; :: thesis: