let h be FinSequence of (TOP-REAL 2); :: thesis: ( h is being_S-Seq implies L~ h is_an_arc_of h /. 1,h /. (len h) )
set P = L~ h;
set p1 = h /. 1;
deffunc H1( Nat) -> Subset of (TOP-REAL 2) = L~ (h | ($1 + 2));
defpred S1[ Nat] means ( 1 <= $1 + 2 & $1 + 2 <= len h implies ex NE being non empty Subset of (TOP-REAL 2) st
( NE = H1($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: L~ h is_an_arc_of h /. 1,h /. (len h)
then A2: len h >= 1 + 1 ;
then 1 <= len h by XXREAL_0:2;
then A3: 1 in Seg (len h) by FINSEQ_1:1;
A4: h is one-to-one by A1;
A5: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A6: S1[n] ; :: thesis: S1[n + 1]
set pn = h /. (n + 2);
set pn1 = h /. ((n + 2) + 1);
A7: (n + 1) + 1 <> (n + 2) + 1 ;
reconsider NE1 = H1(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: ex NE being non empty Subset of (TOP-REAL 2) st
( NE = H1(n + 1) & ex f being Function of I[01],((TOP-REAL 2) | NE) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. ((n + 1) + 2) ) )
A10: (n + 2) + 1 in dom h by A8, A9, FINSEQ_3:25;
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 = H1(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 :: thesis: for x being object st x in H1(n) \/ (LSeg (h,(n + 2))) holds
x in H1(n + 1)
let x be object ; :: thesis: ( x in H1(n) \/ (LSeg (h,(n + 2))) implies x in H1(n + 1) )
assume A15: x in H1(n) \/ (LSeg (h,(n + 2))) ; :: thesis: x in H1(n + 1)
now :: thesis: x in H1(n + 1)
per cases ( x in H1(n) or x in LSeg (h,(n + 2)) ) by A15, XBOOLE_0:def 3;
suppose A16: x in H1(n) ; :: thesis: x in H1(n + 1)
A17: n + 1 <= n + (1 + 1) by XREAL_1:6;
consider X being set such that
A18: x in X and
A19: X in { (LSeg ((h | (n + 2)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by A16, TARSKI:def 4;
consider i being 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:59, XXREAL_0:2;
then i <= n + 1 by XREAL_1:6;
then A23: i <= n + 2 by A17, XXREAL_0:2;
len (h | (n + 2)) = n + 2 by A9, A11, FINSEQ_1:59, XXREAL_0:2;
then i in Seg (len (h | (n + 2))) by A21, A23, FINSEQ_1:1;
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:1;
then i in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:59;
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:70
.= (h | (n + 2)) /. i by A24, FINSEQ_4:70 ;
i + 1 <= n + 2 by A9, A11, A22, FINSEQ_1:59, 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:59;
A29: len (h | ((n + 1) + 2)) = n + (1 + 2) by A9, FINSEQ_1:59;
A30: n + 2 <= n + 3 by XREAL_1:6;
1 <= i + 1 by NAT_1:11;
then i + 1 in Seg (len (h | (n + 2))) by A22, FINSEQ_1:1;
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:1;
then i + 1 in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:59;
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:70
.= (h | (n + 2)) /. (i + 1) by A31, FINSEQ_4:70 ;
i + 1 <= n + (1 + 1) by A9, A11, A22, FINSEQ_1:59, 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, Def3
.= LSeg ((h | ((n + 1) + 2)),i) by A21, A27, A28, A26, A32, Def3 ;
then X in { (LSeg ((h | ((n + 1) + 2)),j)) where j is Nat : ( 1 <= j & j + 1 <= len (h | ((n + 1) + 2)) ) } by A21, A33;
hence x in H1(n + 1) by A18, TARSKI:def 4; :: thesis: verum
end;
suppose A34: x in LSeg (h,(n + 2)) ; :: thesis: x in H1(n + 1)
A35: 1 <= n + 2 by A14, NAT_1:11;
A36: len (h | ((n + 1) + 2)) = (n + 1) + 2 by A9, FINSEQ_1:59;
then (n + 2) + 1 in Seg (len (h | ((n + 1) + 2))) by A8, FINSEQ_1:1;
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:25;
n + 2 <= (n + 2) + 1 by NAT_1:11;
then n + 2 in Seg (len (h | ((n + 1) + 2))) by A36, A35, FINSEQ_1:1;
then A39: n + 2 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def 3;
then A40: 1 <= n + 2 by FINSEQ_3:25;
A41: h /. ((n + 2) + 1) = (h | ((n + 1) + 2)) /. ((n + 2) + 1) by A37, FINSEQ_4:70;
A42: h /. (n + 2) = (h | ((n + 1) + 2)) /. (n + 2) by A39, FINSEQ_4:70;
LSeg (h,(n + 2)) = LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by A9, A35, Def3
.= LSeg ((h | ((n + 1) + 2)),(n + 2)) by A36, A35, A42, A41, Def3 ;
then LSeg (h,(n + 2)) in { (LSeg ((h | ((n + 1) + 2)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (h | ((n + 1) + 2)) ) } by A40, A38;
hence x in H1(n + 1) by A34, TARSKI:def 4; :: thesis: verum
end;
end;
end;
hence x in H1(n + 1) ; :: thesis: verum
end;
then A43: H1(n) \/ (LSeg (h,(n + 2))) c= H1(n + 1) ;
take NE1 ; :: thesis: ( NE1 = H1(n + 1) & ex f being Function of I[01],((TOP-REAL 2) | NE1) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. ((n + 1) + 2) ) )
A44: 1 <= (n + 1) + 1 by NAT_1:11;
now :: thesis: for x being object st x in H1(n + 1) holds
x in H1(n) \/ (LSeg (h,(n + 2)))
let x be object ; :: thesis: ( x in H1(n + 1) implies x in H1(n) \/ (LSeg (h,(n + 2))) )
A45: n + (1 + 1) = (n + 1) + 1 ;
A46: (len (h | ((n + 1) + 2))) - 1 = ((n + 1) + 2) - 1 by A9, FINSEQ_1:59
.= n + (1 + 1) ;
assume x in H1(n + 1) ; :: thesis: x in H1(n) \/ (LSeg (h,(n + 2)))
then consider X being set such that
A47: x in X and
A48: X in { (LSeg ((h | ((n + 1) + 2)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (h | ((n + 1) + 2)) ) } by TARSKI:def 4;
consider i being 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:9;
now :: thesis: x in H1(n) \/ (LSeg (h,(n + 2)))
per cases ( i = n + 2 or i <= n + 1 ) by A52, A46, A45, NAT_1:8;
suppose A53: i = n + 2 ; :: thesis: x in H1(n) \/ (LSeg (h,(n + 2)))
A54: len (h | ((n + 1) + 2)) = (n + 1) + 2 by A9, FINSEQ_1:59;
1 <= (n + 2) + 1 by NAT_1:11;
then (n + 2) + 1 in Seg (len (h | ((n + 1) + 2))) by A54, FINSEQ_1:1;
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:70;
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:1;
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:70;
then LSeg ((h | ((n + 1) + 2)),(n + 2)) = LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by A54, A56, A55, Def3
.= LSeg (h,(n + 2)) by A9, A44, Def3 ;
hence x in H1(n) \/ (LSeg (h,(n + 2))) by A47, A49, A53, XBOOLE_0:def 3; :: thesis: verum
end;
suppose A57: i <= n + 1 ; :: thesis: x in H1(n) \/ (LSeg (h,(n + 2)))
then i + 1 <= (n + 1) + 1 by XREAL_1:6;
then i + 1 <= len (h | (n + 2)) by A9, A11, FINSEQ_1:59, XXREAL_0:2;
then A58: LSeg ((h | (n + 2)),i) in { (LSeg ((h | (n + 2)),j)) where j is 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:59, 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:1;
then A62: i in dom (h | (n + 2)) by FINSEQ_1:def 3;
A63: i + 1 <= (n + 1) + 1 by A57, XREAL_1:7;
then i + 1 in Seg (len (h | (n + 2))) by A60, A59, FINSEQ_1:1;
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:1;
then i in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:59;
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:70
.= (h | (n + 2)) /. i by A62, FINSEQ_4:70 ;
i + 1 <= (n + 1) + 2 by A57, XREAL_1:7;
then i + 1 in Seg ((n + 1) + 2) by A59, FINSEQ_1:1;
then i + 1 in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:59;
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:70
.= (h | (n + 2)) /. (i + 1) by A64, FINSEQ_4:70 ;
LSeg ((h | (n + 2)),i) = LSeg (((h | (n + 2)) /. i),((h | (n + 2)) /. (i + 1))) by A50, A60, A63, Def3
.= LSeg ((h | ((n + 1) + 2)),i) by A50, A51, A65, A66, Def3 ;
then x in union { (LSeg ((h | (n + 2)),j)) where j is Nat : ( 1 <= j & j + 1 <= len (h | (n + 2)) ) } by A47, A49, A58, TARSKI:def 4;
hence x in H1(n) \/ (LSeg (h,(n + 2))) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence x in H1(n) \/ (LSeg (h,(n + 2))) ; :: thesis: verum
end;
then H1(n + 1) c= H1(n) \/ (LSeg (h,(n + 2))) ;
then H1(n + 1) = H1(n) \/ (LSeg (h,(n + 2))) by A43;
hence NE1 = H1(n + 1) by A9, A44, Def3; :: thesis: ex f being Function of I[01],((TOP-REAL 2) | NE1) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. ((n + 1) + 2) )
A67: (n + 1) + 1 <= len h by A9, A11, XXREAL_0:2;
then (n + 1) + 1 in dom h by A44, FINSEQ_3:25;
then LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) is_an_arc_of h /. (n + 2),h /. ((n + 2) + 1) by A4, A7, A10, Th9, PARTFUN2:10;
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) ;
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 object holds
( x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) iff x = h /. (n + 2) )
proof
let x be object ; :: thesis: ( x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) iff x = h /. (n + 2) )
A72: 1 <= n + 1 by NAT_1:11;
thus ( x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) implies x = h /. (n + 2) ) :: thesis: ( x = h /. (n + 2) implies x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) )
proof
A73: 1 <= n + 1 by NAT_1:11;
h is unfolded by A1;
then A74: (LSeg (h,(n + 1))) /\ (LSeg (h,((n + 1) + 1))) = {(h /. ((n + 1) + 1))} by A9, A73;
A75: (n + 1) + 1 <= len h by A9, A11, XXREAL_0:2;
assume A76: x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) ; :: thesis: x = h /. (n + 2)
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, Def3;
set p19 = h /. (n + 1);
set p29 = h /. ((n + 1) + 1);
A79: 1 <= 1 + n by NAT_1:11;
x in H1(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 Nat : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by TARSKI:def 4;
consider i being 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:59, 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:1;
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:70;
1 <= 1 + (n + 1) by NAT_1:11;
then (n + 1) + 1 in Seg (len (h | (n + 2))) by A85, FINSEQ_1:1;
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:70;
A88: len (h | (n + 2)) = (n + 1) + 1 by A9, A11, FINSEQ_1:59, XXREAL_0:2;
then A89: i <= n + 1 by A84, XREAL_1:6;
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, Def3
.= LSeg ((h | (n + 2)),(n + 1)) by A85, A79, A86, A87, Def3 ;
A91: h is s.n.c. by A1;
now :: thesis: not i < n + 1
set p19 = h /. i;
set p29 = h /. (i + 1);
assume A92: i < n + 1 ; :: thesis: contradiction
then A93: i + 1 < (n + 1) + 1 by XREAL_1:6;
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:1;
then i in dom (h | (n + 2)) by FINSEQ_1:def 3;
then A94: (h | (n + 2)) /. i = h /. i by FINSEQ_4:70;
A95: LSeg (h,(n + 2)) = LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by A9, A44, Def3;
1 <= 1 + i by NAT_1:11;
then i + 1 in Seg (len (h | (n + 2))) by A84, FINSEQ_1:1;
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:70;
i + 1 <= len h by A67, A84, A88, XXREAL_0:2;
then LSeg (h,i) = LSeg ((h /. i),(h /. (i + 1))) by A83, Def3
.= LSeg ((h | (n + 2)),i) by A83, A84, A94, A96, Def3 ;
then LSeg ((h | (n + 2)),i) misses LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by A91, A93, A95;
hence contradiction by A77, A80, A82, XBOOLE_0:3; :: thesis: verum
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: verum
end;
assume A97: x = h /. (n + 2) ; :: thesis: x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))))
A98: 1 <= n + 1 by NAT_1:11;
(n + 1) + 1 <= len (h | (n + 2)) by A9, A11, FINSEQ_1:59, XXREAL_0:2;
then A99: LSeg ((h | (n + 2)),(n + 1)) in { (LSeg ((h | (n + 2)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by A98;
A100: n + 2 in Seg (n + 2) by A44, FINSEQ_1:1;
A101: len (h | (n + 2)) = n + 2 by A9, A11, FINSEQ_1:59, 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:70;
then x in LSeg ((h | (n + 2)),(n + 1)) by A101, A72, Th21;
then A102: x in union { (LSeg ((h | (n + 2)),i)) where i is 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:68;
hence x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) by A102, XBOOLE_0:def 4; :: thesis: verum
end;
then H1(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:3;
take hh ; :: thesis: ( hh is being_homeomorphism & hh . 0 = h /. 1 & hh . 1 = h /. ((n + 1) + 2) )
thus ( hh is being_homeomorphism & hh . 0 = h /. 1 & hh . 1 = h /. ((n + 1) + 2) ) by A71, A70, A103, A104, A105; :: thesis: verum
end;
h | 2 = h | (Seg 2) by FINSEQ_1:def 16;
then A106: dom (h | 2) = (dom h) /\ (Seg 2) by RELAT_1:61
.= (Seg (len h)) /\ (Seg 2) by FINSEQ_1:def 3
.= Seg 2 by A2, FINSEQ_1:7 ;
then A107: len (h | 2) = 1 + 1 by FINSEQ_1:def 3;
then A108: 2 in Seg (len (h | 2)) by FINSEQ_1:1;
A109: 1 in Seg (len (h | 2)) by A107, FINSEQ_1:1;
now :: thesis: for x being object holds
( ( x in { (LSeg ((h | 2),i)) where i is Nat : ( 1 <= i & i + 1 <= len (h | 2) ) } implies x = LSeg (h,1) ) & ( x = LSeg (h,1) implies x in { (LSeg ((h | 2),i)) where i is Nat : ( 1 <= i & i + 1 <= len (h | 2) ) } ) )
let x be object ; :: thesis: ( ( x in { (LSeg ((h | 2),i)) where i is Nat : ( 1 <= i & i + 1 <= len (h | 2) ) } implies x = LSeg (h,1) ) & ( x = LSeg (h,1) implies x in { (LSeg ((h | 2),i)) where i is Nat : ( 1 <= i & i + 1 <= len (h | 2) ) } ) )
A110: h /. (1 + 1) = (h | 2) /. 2 by A106, A107, A108, FINSEQ_4:70;
thus ( x in { (LSeg ((h | 2),i)) where i is Nat : ( 1 <= i & i + 1 <= len (h | 2) ) } implies x = LSeg (h,1) ) :: thesis: ( x = LSeg (h,1) implies x in { (LSeg ((h | 2),i)) where i is Nat : ( 1 <= i & i + 1 <= len (h | 2) ) } )
proof
assume x in { (LSeg ((h | 2),i)) where i is Nat : ( 1 <= i & i + 1 <= len (h | 2) ) } ; :: thesis: x = LSeg (h,1)
then consider i being 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:6;
then A114: 1 = i by A112, XXREAL_0:1;
A115: (h | 2) /. (1 + 1) = h /. (1 + 1) by A106, A107, A108, FINSEQ_4:70;
(h | 2) /. 1 = h /. 1 by A106, A107, A109, FINSEQ_4:70;
hence x = LSeg ((h /. 1),(h /. (1 + 1))) by A107, A111, A114, A115, Def3
.= LSeg (h,1) by A2, Def3 ;
:: thesis: verum
end;
assume x = LSeg (h,1) ; :: thesis: x in { (LSeg ((h | 2),i)) where i is Nat : ( 1 <= i & i + 1 <= len (h | 2) ) }
then A116: x = LSeg ((h /. 1),(h /. (1 + 1))) by A2, Def3;
h /. 1 = (h | 2) /. 1 by A106, A107, A109, FINSEQ_4:70;
then x = LSeg ((h | 2),1) by A107, A116, A110, Def3;
hence x in { (LSeg ((h | 2),i)) where i is Nat : ( 1 <= i & i + 1 <= len (h | 2) ) } by A107; :: thesis: verum
end;
then { (LSeg ((h | 2),i)) where i is Nat : ( 1 <= i & i + 1 <= len (h | 2) ) } = {(LSeg (h,1))} by TARSKI:def 1;
then A117: H1( 0 ) = LSeg (h,1) by ZFMISC_1:25
.= LSeg ((h /. 1),(h /. (1 + 1))) by A2, Def3 ;
A118: 1 + 1 in Seg (len h) by A2, FINSEQ_1:1;
( 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: 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) )
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, Th9, PARTFUN2:10;
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) ) ; :: thesis: verum
end;
then A120: S1[ 0 ] by A117;
A121: for n being Nat holds S1[n] from NAT_1:sch 2(A120, A5);
 (len h) - 2 in NAT by A2, INT_1:5;
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 = H1(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 16
.= h | (dom h) by FINSEQ_1:def 3
.= h by RELAT_1:68 ;
then reconsider f = f as Function of I[01],((TOP-REAL 2) | (L~ h)) by A122;
take f ; :: according to TOPREAL1:def 1 :: thesis: ( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (len h) )
thus f is being_homeomorphism by A122, A124, A127; :: thesis: ( f . 0 = h /. 1 & f . 1 = h /. (len h) )
thus ( f . 0 = h /. 1 & f . 1 = h /. (len h) ) by A125, A126; :: thesis: verum