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) )
assume A1:
h is being_S-Seq
; :: thesis: L~ h is_an_arc_of h /. 1,h /. (len h)
set P = L~ h;
set p1 = h /. 1;
A2:
h is one-to-one
by A1, Def10;
A3:
len h >= 1 + 1
by A1, Def10;
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) ) ) );
1 <= len h
by A3, XXREAL_0:2;
then A4:
1 in Seg (len h)
by FINSEQ_1:3;
A5:
1 + 1 in Seg (len h)
by A3, FINSEQ_1:3;
set p2 = h /. (1 + 1);
h | 2 = h | (Seg 2)
by FINSEQ_1:def 15;
then A6: dom (h | 2) =
(dom h) /\ (Seg 2)
by RELAT_1:90
.=
(Seg (len h)) /\ (Seg 2)
by FINSEQ_1:def 3
.=
Seg 2
by A3, FINSEQ_1:9
;
then A7:
len (h | 2) = 1 + 1
by FINSEQ_1:def 3;
then A8:
( 1 in Seg (len (h | 2)) & 2 in Seg (len (h | 2)) )
by FINSEQ_1:3;
{ (LSeg (h | 2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } = {(LSeg h,1)}
proof
now let x be
set ;
:: thesis: ( ( x in { (LSeg (h | 2),i) where i is Element of 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 Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } ) )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: ( x = LSeg h,1 implies x in { (LSeg (h | 2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } )proof
assume
x in { (LSeg (h | 2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) }
;
:: thesis: x = LSeg h,1
then consider i being
Element of
NAT such that A9:
x = LSeg (h | 2),
i
and A10:
( 1
<= i &
i + 1
<= len (h | 2) )
;
( 1
<= i &
i + 1
<= 1
+ 1 )
by A6, A10, FINSEQ_1:def 3;
then
( 1
<= i &
i <= 1 )
by XREAL_1:8;
then A11:
1
= i
by XXREAL_0:1;
(
(h | 2) /. 1
= h /. 1 &
(h | 2) /. (1 + 1) = h /. (1 + 1) )
by A6, A7, A8, FINSEQ_4:85;
hence x =
LSeg (h /. 1),
(h /. (1 + 1))
by A7, A9, A11, Def5
.=
LSeg h,1
by A3, Def5
;
:: thesis: verum
end; assume
x = LSeg h,1
;
:: thesis: x in { (LSeg (h | 2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } then A12:
x = LSeg (h /. 1),
(h /. (1 + 1))
by A3, Def5;
(
h /. 1
= (h | 2) /. 1 &
h /. (1 + 1) = (h | 2) /. 2 )
by A6, A7, A8, FINSEQ_4:85;
then
x = LSeg (h | 2),1
by A7, A12, Def5;
hence
x in { (LSeg (h | 2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) }
by A7;
:: thesis: verum end;
hence
{ (LSeg (h | 2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } = {(LSeg h,1)}
by TARSKI:def 1;
:: thesis: verum
end;
then A13: H1( 0 ) =
LSeg h,1
by ZFMISC_1:31
.=
LSeg (h /. 1),(h /. (1 + 1))
by A3, Def5
;
( 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
( 1
<= 0 + 2 &
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) )
( 1
<> 2 & 1
in dom h & 2
in dom h )
by A4, A5, FINSEQ_1:def 3;
then
LSeg (h /. 1),
(h /. (1 + 1)) is_an_arc_of h /. 1,
h /. (1 + 1)
by A2, 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: verum
end;
then A14:
S1[ 0 ]
by A13;
A15:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A16:
S1[
n]
;
:: thesis: S1[n + 1]
assume A17:
( 1
<= (n + 1) + 2 &
(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) ) )
then A18:
( 1
<= (n + 1) + 1 &
(n + 1) + 1
<= (n + 2) + 1 &
(n + 2) + 1
<= len h )
by NAT_1:11;
then A19:
( 1
<= (n + 1) + 1 &
(n + 1) + 1
<= len h )
by XXREAL_0:2;
A20:
(n + 1) + 1
= n + (1 + 1)
;
consider NE being non
empty Subset of
(TOP-REAL 2) such that A21:
(
NE = H1(
n) & 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 A16, A18, XXREAL_0:2;
consider f being
Function of
I[01] ,
((TOP-REAL 2) | NE) such that A22:
(
f is
being_homeomorphism &
f . 0 = h /. 1 &
f . 1
= h /. (n + 2) )
by A21;
set pn =
h /. (n + 2);
set pn1 =
h /. ((n + 2) + 1);
A23:
(n + 1) + 1
<> (n + 2) + 1
;
(
(n + 1) + 1
in dom h &
(n + 2) + 1
in dom h )
by A17, A19, FINSEQ_3:27;
then
LSeg (h /. (n + 2)),
(h /. ((n + 2) + 1)) is_an_arc_of h /. (n + 2),
h /. ((n + 2) + 1)
by A2, A23, Th15, PARTFUN2:17;
then consider f1 being
Function of
I[01] ,
((TOP-REAL 2) | (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1)))) such that A24:
(
f1 is
being_homeomorphism &
f1 . 0 = h /. (n + 2) &
f1 . 1
= h /. ((n + 2) + 1) )
by Def2;
A25:
H1(
n + 1)
= H1(
n)
\/ (LSeg h,(n + 2))
proof
now let x be
set ;
:: thesis: ( x in H1(n + 1) implies x in H1(n) \/ (LSeg h,(n + 2)) )assume
x in H1(
n + 1)
;
:: thesis: x in H1(n) \/ (LSeg h,(n + 2))then consider X being
set such that A26:
x in X
and A27:
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 A28:
X = LSeg (h | ((n + 1) + 2)),
i
and A29:
( 1
<= i &
i + 1
<= len (h | ((n + 1) + 2)) )
by A27;
(i + 1) - 1
= i
;
then A30:
i <= (len (h | ((n + 1) + 2))) - 1
by A29, XREAL_1:11;
A31:
(len (h | ((n + 1) + 2))) - 1 =
((n + 1) + 2) - 1
by A17, FINSEQ_1:80
.=
n + (1 + 1)
;
A32:
n + (1 + 1) = (n + 1) + 1
;
now per cases
( i = n + 2 or i <= n + 1 )
by A30, A31, A32, NAT_1:8;
suppose A33:
i = n + 2
;
:: thesis: x in H1(n) \/ (LSeg h,(n + 2))A34:
len (h | ((n + 1) + 2)) = (n + 1) + 2
by A17, FINSEQ_1:80;
(n + 1) + 2
= (n + 2) + 1
;
then A35:
( 1
<= n + 2 &
n + 2
<= (n + 1) + 2 &
(n + 2) + 1
<= (n + 1) + 2 & 1
<= (n + 2) + 1 )
by A20, NAT_1:11;
then
(
n + 2
in Seg (len (h | ((n + 1) + 2))) &
(n + 2) + 1
in Seg (len (h | ((n + 1) + 2))) )
by A34, FINSEQ_1:3;
then A36:
(
n + 2
in dom (h | ((n + 1) + 2)) &
(n + 2) + 1
in dom (h | ((n + 1) + 2)) )
by FINSEQ_1:def 3;
then A37:
(h | ((n + 1) + 2)) /. (n + 2) = h /. (n + 2)
by FINSEQ_4:85;
(h | ((n + 1) + 2)) /. ((n + 2) + 1) = h /. (n + (2 + 1))
by A36, FINSEQ_4:85;
then LSeg (h | ((n + 1) + 2)),
(n + 2) =
LSeg (h /. (n + 2)),
(h /. ((n + 2) + 1))
by A34, A35, A37, Def5
.=
LSeg h,
(n + 2)
by A18, Def5
;
hence
x in H1(
n)
\/ (LSeg h,(n + 2))
by A26, A28, A33, XBOOLE_0:def 3;
:: thesis: verum end; suppose A38:
i <= n + 1
;
:: thesis: x in H1(n) \/ (LSeg h,(n + 2))A39:
len (h | (n + 2)) = n + (1 + 1)
by A18, FINSEQ_1:80, XXREAL_0:2;
i + 1
<= (n + 1) + 1
by A38, XREAL_1:8;
then
i + 1
<= len (h | (n + 2))
by A18, FINSEQ_1:80, XXREAL_0:2;
then A40:
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 A29;
A41:
( 1
<= 1
+ i &
n + 1
<= (n + 1) + 1 &
(n + 1) + 1
= n + (1 + 1) &
i + 1
<= (n + 1) + 1 )
by A38, NAT_1:11, XREAL_1:9;
then A42:
( 1
<= i + 1 &
i <= n + 2 &
i + 1
<= n + 2 )
by A38, XXREAL_0:2;
then A43:
(
i in Seg (len (h | (n + 2))) &
i + 1
in Seg (len (h | (n + 2))) )
by A29, A39, FINSEQ_1:3;
set p1' =
(h | (n + 2)) /. i;
set p2' =
(h | (n + 2)) /. (i + 1);
A44:
(
i in dom (h | (n + 2)) &
i + 1
in dom (h | (n + 2)) )
by A43, FINSEQ_1:def 3;
(
n + 2
<= (n + 2) + 1 &
(n + 2) + 1
= (n + 1) + 2 )
by NAT_1:11;
then
(
i <= (n + 1) + 2 &
i + 1
<= (n + 1) + 2 )
by A42, XXREAL_0:2;
then
(
i in Seg ((n + 1) + 2) &
i + 1
in Seg ((n + 1) + 2) &
(n + 1) + 2
<= len h )
by A17, A29, A41, FINSEQ_1:3;
then
(
i in Seg (len (h | ((n + 1) + 2))) &
i + 1
in Seg (len (h | ((n + 1) + 2))) )
by FINSEQ_1:80;
then A45:
(
i in dom (h | ((n + 1) + 2)) &
i + 1
in dom (h | ((n + 1) + 2)) )
by FINSEQ_1:def 3;
then A46:
(h | ((n + 1) + 2)) /. i =
h /. i
by FINSEQ_4:85
.=
(h | (n + 2)) /. i
by A44, FINSEQ_4:85
;
A47:
(h | ((n + 1) + 2)) /. (i + 1) =
h /. (i + 1)
by A45, FINSEQ_4:85
.=
(h | (n + 2)) /. (i + 1)
by A44, FINSEQ_4:85
;
LSeg (h | (n + 2)),
i =
LSeg ((h | (n + 2)) /. i),
((h | (n + 2)) /. (i + 1))
by A29, A39, A41, Def5
.=
LSeg (h | ((n + 1) + 2)),
i
by A29, A46, A47, 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 A26, A28, A40, TARSKI:def 4;
hence
x in H1(
n)
\/ (LSeg h,(n + 2))
by XBOOLE_0:def 3;
:: thesis: verum end; hence
x in H1(
n)
\/ (LSeg h,(n + 2))
;
:: thesis: verum end;
then A48:
H1(
n + 1)
c= H1(
n)
\/ (LSeg h,(n + 2))
by TARSKI:def 3;
now let x be
set ;
:: thesis: ( x in H1(n) \/ (LSeg h,(n + 2)) implies x in H1(n + 1) )assume A49:
x in H1(
n)
\/ (LSeg h,(n + 2))
;
:: thesis: x in H1(n + 1)now per cases
( x in H1(n) or x in LSeg h,(n + 2) )
by A49, XBOOLE_0:def 3;
suppose
x in H1(
n)
;
:: thesis: x in H1(n + 1)then consider X being
set such that A50:
x in X
and A51:
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 A52:
X = LSeg (h | (n + 2)),
i
and A53:
( 1
<= i &
i + 1
<= len (h | (n + 2)) )
by A51;
A54:
(
(n + 1) + 2
<= len h &
n + 2
<= len h )
by A18, XXREAL_0:2;
A55:
(
i + 1
<= n + (1 + 1) &
len (h | ((n + 1) + 2)) = n + (1 + 2) )
by A18, A53, FINSEQ_1:80, XXREAL_0:2;
i + 1
<= (n + 1) + 1
by A18, A53, FINSEQ_1:80, XXREAL_0:2;
then A56:
(
i <= n + 1 &
n + 1
<= n + (1 + 1) )
by XREAL_1:8;
n + 2
<= n + 3
by XREAL_1:8;
then A57:
( 1
<= i &
i + 1
<= len (h | ((n + 1) + 2)) )
by A53, A55, XXREAL_0:2;
A58:
len (h | (n + 2)) = n + 2
by A18, FINSEQ_1:80, XXREAL_0:2;
A59:
( 1
<= 1
+ i &
(n + 1) + 1
= n + (1 + 1) &
i + 1
<= (n + 1) + 1 )
by A53, A54, FINSEQ_1:80, NAT_1:11;
A60:
( 1
<= i + 1 &
i <= n + 2 &
i + 1
<= n + 2 )
by A53, A54, A56, FINSEQ_1:80, NAT_1:11, XXREAL_0:2;
then A61:
(
i in Seg (len (h | (n + 2))) &
i + 1
in Seg (len (h | (n + 2))) )
by A53, A58, FINSEQ_1:3;
set p1' =
(h | (n + 2)) /. i;
set p2' =
(h | (n + 2)) /. (i + 1);
A62:
(
i in dom (h | (n + 2)) &
i + 1
in dom (h | (n + 2)) )
by A61, FINSEQ_1:def 3;
(
n + 2
<= (n + 2) + 1 &
(n + 2) + 1
= (n + 1) + 2 )
by NAT_1:11;
then A63:
(
i <= (n + 1) + 2 &
i + 1
<= (n + 1) + 2 )
by A60, XXREAL_0:2;
then
(
i in Seg ((n + 1) + 2) &
i + 1
in Seg ((n + 1) + 2) &
(n + 1) + 2
<= len h )
by A17, A53, A59, FINSEQ_1:3;
then A64:
(
i in Seg (len (h | ((n + 1) + 2))) &
i + 1
in Seg (len (h | ((n + 1) + 2))) &
len (h | ((n + 1) + 2)) = (n + 1) + 2 )
by FINSEQ_1:80;
then A65:
(
i in dom (h | ((n + 1) + 2)) &
i + 1
in dom (h | ((n + 1) + 2)) )
by FINSEQ_1:def 3;
then A66:
(h | ((n + 1) + 2)) /. i =
h /. i
by FINSEQ_4:85
.=
(h | (n + 2)) /. i
by A62, FINSEQ_4:85
;
A67:
(h | ((n + 1) + 2)) /. (i + 1) =
h /. (i + 1)
by A65, FINSEQ_4:85
.=
(h | (n + 2)) /. (i + 1)
by A62, FINSEQ_4:85
;
X =
LSeg ((h | (n + 2)) /. i),
((h | (n + 2)) /. (i + 1))
by A52, A53, Def5
.=
LSeg (h | ((n + 1) + 2)),
i
by A53, A63, A64, A66, A67, 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 A57;
hence
x in H1(
n + 1)
by A50, TARSKI:def 4;
:: thesis: verum end; suppose A68:
x in LSeg h,
(n + 2)
;
:: thesis: x in H1(n + 1)A69:
(
len (h | ((n + 1) + 2)) = (n + 1) + 2 & 1
<= (n + 1) + 2 &
n + 2
<= (n + 2) + 1 & 1
<= n + 2 &
(n + 1) + 2
= (n + 2) + 1 )
by A17, A20, FINSEQ_1:80, NAT_1:11;
then
(
n + 2
in Seg (len (h | ((n + 1) + 2))) &
(n + 2) + 1
in Seg (len (h | ((n + 1) + 2))) )
by FINSEQ_1:3;
then A70:
(
n + 2
in dom (h | ((n + 1) + 2)) &
(n + 2) + 1
in dom (h | ((n + 1) + 2)) )
by FINSEQ_1:def 3;
then A71:
( 1
<= n + 2 &
(n + 2) + 1
<= len (h | ((n + 1) + 2)) )
by FINSEQ_3:27;
A72:
h /. (n + 2) = (h | ((n + 1) + 2)) /. (n + 2)
by A70, FINSEQ_4:85;
A73:
h /. ((n + 2) + 1) = (h | ((n + 1) + 2)) /. ((n + 2) + 1)
by A70, FINSEQ_4:85;
LSeg h,
(n + 2) =
LSeg (h /. (n + 2)),
(h /. ((n + 2) + 1))
by A17, A69, Def5
.=
LSeg (h | ((n + 1) + 2)),
(n + 2)
by A69, A72, A73, 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 A71;
hence
x in H1(
n + 1)
by A68, TARSKI:def 4;
:: thesis: verum end; hence
x in H1(
n + 1)
;
:: thesis: verum end;
then
H1(
n)
\/ (LSeg h,(n + 2)) c= H1(
n + 1)
by TARSKI:def 3;
hence
H1(
n + 1)
= H1(
n)
\/ (LSeg h,(n + 2))
by A48, XBOOLE_0:def 10;
:: thesis: verum
end;
for
x being
set holds
(
x in H1(
n)
/\ (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1))) iff
x = h /. (n + 2) )
proof
let x be
set ;
:: thesis: ( x in H1(n) /\ (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1))) iff x = h /. (n + 2) )
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
assume
x in H1(
n)
/\ (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1)))
;
:: thesis: x = h /. (n + 2)
then A74:
(
x in LSeg (h /. (n + 2)),
(h /. ((n + 2) + 1)) &
x in H1(
n) )
by XBOOLE_0:def 4;
then consider X being
set such that A75:
x in X
and A76:
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 A77:
X = LSeg (h | (n + 2)),
i
and A78:
( 1
<= i &
i + 1
<= len (h | (n + 2)) )
by A76;
A79:
len (h | (n + 2)) = n + (1 + 1)
by A18, FINSEQ_1:80, XXREAL_0:2;
A80:
len (h | (n + 2)) = (n + 1) + 1
by A18, FINSEQ_1:80, XXREAL_0:2;
then A81:
i <= n + 1
by A78, XREAL_1:8;
A82:
h is
s.n.c.
by A1, Def10;
A83:
h is
unfolded
by A1, Def10;
now assume A84:
i < n + 1
;
:: thesis: contradictionA85:
( 1
<= 1
+ i &
i + 1
<= n + (1 + 1) )
by A19, A78, FINSEQ_1:80, NAT_1:11;
A86:
i + 1
<= len h
by A19, A78, A80, XXREAL_0:2;
A87:
i + 1
< (n + 1) + 1
by A84, XREAL_1:8;
set p1' =
h /. i;
set p2' =
h /. (i + 1);
(
n + 1
<= (n + 1) + 1 &
(n + 1) + 1
= n + (1 + 1) )
by NAT_1:11;
then
i <= n + 2
by A84, XXREAL_0:2;
then
(
i in Seg (len (h | (n + 2))) &
i + 1
in Seg (len (h | (n + 2))) )
by A78, A79, A85, FINSEQ_1:3;
then A88:
(
i in dom (h | (n + 2)) &
i + 1
in dom (h | (n + 2)) )
by FINSEQ_1:def 3;
then A89:
(h | (n + 2)) /. i = h /. i
by FINSEQ_4:85;
A90:
(h | (n + 2)) /. (i + 1) = h /. (i + 1)
by A88, FINSEQ_4:85;
A91:
LSeg h,
i =
LSeg (h /. i),
(h /. (i + 1))
by A78, A86, Def5
.=
LSeg (h | (n + 2)),
i
by A78, A89, A90, Def5
;
LSeg h,
(n + 2) = LSeg (h /. (n + 2)),
(h /. ((n + 2) + 1))
by A18, Def5;
then
LSeg (h | (n + 2)),
i misses LSeg (h /. (n + 2)),
(h /. ((n + 2) + 1))
by A82, A87, A91, Def9;
hence
contradiction
by A74, A75, A77, XBOOLE_0:3;
:: thesis: verum end;
then A92:
i = n + 1
by A81, XXREAL_0:1;
A93:
( 1
<= n + 1 & 1
<= (n + 1) + 1 &
(n + 1) + 1
<= len h )
by A18, A78, A81, XXREAL_0:2;
set p1' =
h /. (n + 1);
set p2' =
h /. ((n + 1) + 1);
A94:
(
n + 1
<= (n + 1) + 1 &
(n + 1) + 1
= n + (1 + 1) & 1
<= 1
+ n & 1
<= 1
+ (n + 1) )
by NAT_1:11;
then
(
n + 1
in Seg (len (h | (n + 2))) &
(n + 1) + 1
in Seg (len (h | (n + 2))) )
by A79, FINSEQ_1:3;
then A95:
(
n + 1
in dom (h | (n + 2)) &
(n + 1) + 1
in dom (h | (n + 2)) )
by FINSEQ_1:def 3;
then A96:
(h | (n + 2)) /. (n + 1) = h /. (n + 1)
by FINSEQ_4:85;
A97:
(h | (n + 2)) /. ((n + 1) + 1) = h /. ((n + 1) + 1)
by A95, FINSEQ_4:85;
A98:
LSeg h,
(n + 1) =
LSeg (h /. (n + 1)),
(h /. ((n + 1) + 1))
by A93, Def5
.=
LSeg (h | (n + 2)),
(n + 1)
by A79, A94, A96, A97, Def5
;
LSeg (h /. (n + 2)),
(h /. ((n + 2) + 1)) = LSeg h,
((n + 1) + 1)
by A18, Def5;
then A99:
x in (LSeg h,(n + 1)) /\ (LSeg h,((n + 1) + 1))
by A74, A75, A77, A92, A98, XBOOLE_0:def 4;
1
<= n + 1
by NAT_1:11;
then
(LSeg h,(n + 1)) /\ (LSeg h,((n + 1) + 1)) = {(h /. ((n + 1) + 1))}
by A17, A83, Def8;
hence
x = h /. (n + 2)
by A99, TARSKI:def 1;
:: thesis: verum
end;
assume A100:
x = h /. (n + 2)
;
:: thesis: x in H1(n) /\ (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1)))
then A101:
x in LSeg (h /. (n + 2)),
(h /. ((n + 2) + 1))
by RLTOPSP1:69;
A102:
len (h | (n + 2)) = n + 2
by A18, FINSEQ_1:80, XXREAL_0:2;
then
(
dom (h | (n + 2)) = Seg (n + 2) &
n + 2
in Seg (n + 2) )
by A18, FINSEQ_1:3, FINSEQ_1:def 3;
then A103:
x = (h | (n + 2)) /. ((n + 1) + 1)
by A100, FINSEQ_4:85;
1
<= n + 1
by NAT_1:11;
then A104:
x in LSeg (h | (n + 2)),
(n + 1)
by A102, A103, Th27;
( 1
<= 1
+ n &
(n + 1) + 1
<= n + (1 + 1) &
n + 2
<= len h )
by A18, NAT_1:11, XXREAL_0:2;
then
( 1
<= n + 1 &
(n + 1) + 1
<= len (h | (n + 2)) )
by FINSEQ_1:80;
then
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)) ) }
;
then
x in union { (LSeg (h | (n + 2)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) }
by A104, TARSKI:def 4;
hence
x in H1(
n)
/\ (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1)))
by A101, XBOOLE_0:def 4;
:: thesis: verum
end;
then A105:
H1(
n)
/\ (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1))) = {(h /. (n + 2))}
by TARSKI:def 1;
reconsider NE1 =
H1(
n)
\/ (LSeg (h /. (n + 2)),(h /. ((n + 2) + 1))) as non
empty Subset of
(TOP-REAL 2) ;
consider hh being
Function of
I[01] ,
((TOP-REAL 2) | NE1) such that A106:
(
hh is
being_homeomorphism &
hh . 0 = f . 0 &
hh . 1
= f1 . 1 )
by A21, A22, A24, A105, TOPMETR2:6;
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) ) )
thus
NE1 = H1(
n + 1)
by A18, A25, Def5;
:: 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) )
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 A22, A24, A106;
:: thesis: verum
end;
A107:
for n being Nat holds S1[n]
from NAT_1:sch 2(A14, A15);
(len h) - 2 in NAT
by A3, 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
A108:
( NE = H1(h1) & 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 A107;
consider f being Function of I[01] ,((TOP-REAL 2) | NE) such that
A109:
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (h1 + 2) )
by A108;
A110: 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 A108;
take
f
; :: according to TOPREAL1:def 2 :: thesis: ( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (len h) )
thus
f is being_homeomorphism
by A108, A109, A110; :: thesis: ( f . 0 = h /. 1 & f . 1 = h /. (len h) )
thus
( f . 0 = h /. 1 & f . 1 = h /. (len h) )
by A109; :: thesis: verum