let f be FinSequence of (TOP-REAL 2); for P being non empty Subset of (TOP-REAL 2)
for F being Function of I[01],((TOP-REAL 2) | P)
for i being Nat st 1 <= i & i + 1 <= len f & f is being_S-Seq & P = L~ f & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = F .: [.p1,p2.] & F . p1 = f /. i & F . p2 = f /. (i + 1) )
let P be non empty Subset of (TOP-REAL 2); for F being Function of I[01],((TOP-REAL 2) | P)
for i being Nat st 1 <= i & i + 1 <= len f & f is being_S-Seq & P = L~ f & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = F .: [.p1,p2.] & F . p1 = f /. i & F . p2 = f /. (i + 1) )
let Ff be Function of I[01],((TOP-REAL 2) | P); for i being Nat st 1 <= i & i + 1 <= len f & f is being_S-Seq & P = L~ f & Ff is being_homeomorphism & Ff . 0 = f /. 1 & Ff . 1 = f /. (len f) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = Ff .: [.p1,p2.] & Ff . p1 = f /. i & Ff . p2 = f /. (i + 1) )
let i be Nat; ( 1 <= i & i + 1 <= len f & f is being_S-Seq & P = L~ f & Ff is being_homeomorphism & Ff . 0 = f /. 1 & Ff . 1 = f /. (len f) implies ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = Ff .: [.p1,p2.] & Ff . p1 = f /. i & Ff . p2 = f /. (i + 1) ) )
assume that
A1:
1 <= i
and
A2:
i + 1 <= len f
and
A3:
f is being_S-Seq
and
A4:
P = L~ f
and
A5:
Ff is being_homeomorphism
and
A6:
Ff . 0 = f /. 1
and
A7:
Ff . 1 = f /. (len f)
; ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = Ff .: [.p1,p2.] & Ff . p1 = f /. i & Ff . p2 = f /. (i + 1) )
A8:
f is one-to-one
by A3;
A9:
the carrier of (Closed-Interval-TSpace ((1 / 2),1)) = [.(1 / 2),1.]
by TOPMETR:18;
A10:
[#] (Closed-Interval-TSpace (0,(1 / 2))) = [.0,(1 / 2).]
by TOPMETR:18;
A11:
[#] (Closed-Interval-TSpace ((1 / 2),1)) = [.(1 / 2),1.]
by TOPMETR:18;
A12:
len f >= 2
by A3, TOPREAL1:def 8;
deffunc H1( Nat) -> Element of K19( the carrier of (TOP-REAL 2)) = L~ (f | ($1 + 2));
defpred S1[ Nat] means ( 1 <= $1 + 2 & $1 + 2 <= len f implies ex NE being non empty Subset of (TOP-REAL 2) st
( NE = H1($1) & ( for j being Nat
for F being Function of I[01],((TOP-REAL 2) | NE) st 1 <= j & j + 1 <= $1 + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. ($1 + 2) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) ) ) );
reconsider h1 = (len f) - 2 as Element of NAT by A12, INT_1:5;
A13: f | (len f) =
f | (Seg (len f))
by FINSEQ_1:def 15
.=
f | (dom f)
by FINSEQ_1:def 3
.=
f
by RELAT_1:68
;
A14:
S1[ 0 ]
proof
assume that A15:
1
<= 0 + 2
and A16:
0 + 2
<= len f
;
ex NE being non empty Subset of (TOP-REAL 2) st
( NE = H1( 0 ) & ( for j being Nat
for F being Function of I[01],((TOP-REAL 2) | NE) st 1 <= j & j + 1 <= 0 + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (0 + 2) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) ) )
A17:
1
<= len (f | 2)
by A15, A16, FINSEQ_1:59;
A18:
2
<= len (f | 2)
by A16, FINSEQ_1:59;
then reconsider NE =
H1(
0 ) as non
empty Subset of
(TOP-REAL 2) by TOPREAL1:23;
take
NE
;
( NE = H1( 0 ) & ( for j being Nat
for F being Function of I[01],((TOP-REAL 2) | NE) st 1 <= j & j + 1 <= 0 + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (0 + 2) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) ) )
thus
NE = H1(
0 )
;
for j being Nat
for F being Function of I[01],((TOP-REAL 2) | NE) st 1 <= j & j + 1 <= 0 + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (0 + 2) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) )
let j be
Nat;
for F being Function of I[01],((TOP-REAL 2) | NE) st 1 <= j & j + 1 <= 0 + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (0 + 2) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) )let F be
Function of
I[01],
((TOP-REAL 2) | NE);
( 1 <= j & j + 1 <= 0 + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (0 + 2) implies ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) )
assume that A19:
1
<= j
and A20:
j + 1
<= 0 + 2
and A21:
F is
being_homeomorphism
and A22:
F . 0 = f /. 1
and A23:
F . 1
= f /. (0 + 2)
;
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) )
j <= (1 + 1) - 1
by A20, XREAL_1:19;
then A24:
j = 1
by A19, XXREAL_0:1;
A25:
len (f | 2) = 2
by A16, FINSEQ_1:59;
A26:
1
in dom (f | 2)
by A17, FINSEQ_3:25;
A27:
2
in dom (f | 2)
by A18, FINSEQ_3:25;
A28:
(f | 2) /. 1
= (f | 2) . 1
by A26, PARTFUN1:def 6;
A29:
(f | 2) /. 2
= (f | 2) . 2
by A27, PARTFUN1:def 6;
A30:
(f | 2) /. 1
= f /. 1
by A26, FINSEQ_4:70;
A31:
1
+ 1
<= len f
by A16;
A32:
rng F =
[#] ((TOP-REAL 2) | NE)
by A21, TOPS_2:def 5
.=
L~ (f | 2)
by PRE_TOPC:def 5
.=
L~ <*((f | 2) /. 1),((f | 2) /. 2)*>
by A25, A28, A29, FINSEQ_1:44
.=
LSeg (
((f | 2) /. 1),
((f | 2) /. 2))
by SPPOL_2:21
.=
LSeg (
(f /. 1),
(f /. 2))
by A27, A30, FINSEQ_4:70
.=
LSeg (
f,1)
by A31, TOPREAL1:def 3
;
take
0
;
ex p2 being Real st
( 0 < p2 & 0 <= 0 & 0 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.0,p2.] & F . 0 = f /. j & F . p2 = f /. (j + 1) )
take
jj
;
( 0 < jj & 0 <= 0 & 0 <= 1 & 0 <= jj & jj <= 1 & LSeg (f,j) = F .: [.0,jj.] & F . 0 = f /. j & F . jj = f /. (j + 1) )
thus
(
0 < jj &
0 <= 0 &
0 <= 1 &
0 <= jj &
jj <= 1 &
LSeg (
f,
j)
= F .: [.0,jj.] &
F . 0 = f /. j &
F . jj = f /. (j + 1) )
by A22, A23, A24, A32, BORSUK_1:40, RELSET_1:22;
verum
end;
A33:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A34:
S1[
n]
;
S1[n + 1]
assume that A35:
1
<= (n + 1) + 2
and A36:
(n + 1) + 2
<= len f
;
ex NE being non empty Subset of (TOP-REAL 2) st
( NE = H1(n + 1) & ( for j being Nat
for F being Function of I[01],((TOP-REAL 2) | NE) st 1 <= j & j + 1 <= (n + 1) + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. ((n + 1) + 2) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) ) )
A37:
2
<= n + 2
by NAT_1:11;
n + 2
<= (n + 2) + 1
by NAT_1:11;
then consider NE being non
empty Subset of
(TOP-REAL 2) such that A38:
NE = H1(
n)
and A39:
for
j being
Nat for
F being
Function of
I[01],
((TOP-REAL 2) | NE) st 1
<= j &
j + 1
<= n + 2 &
F is
being_homeomorphism &
F . 0 = f /. 1 &
F . 1
= f /. (n + 2) holds
ex
p1,
p2 being
Real st
(
p1 < p2 &
0 <= p1 &
p1 <= 1 &
0 <= p2 &
p2 <= 1 &
LSeg (
f,
j)
= F .: [.p1,p2.] &
F . p1 = f /. j &
F . p2 = f /. (j + 1) )
by A34, A36, A37, XXREAL_0:2;
A40:
len (f | ((n + 1) + 2)) = (n + 1) + 2
by A36, FINSEQ_1:59;
A41:
(n + 1) + 2
= (n + 2) + 1
;
A42:
1
<= (n + 1) + 1
by NAT_1:11;
A43:
(n + 1) + 1
<= (n + 2) + 1
by NAT_1:11;
then A44:
(n + 1) + 1
<= len f
by A36, XXREAL_0:2;
A45:
n + 2
<= len f
by A36, A43, XXREAL_0:2;
A46:
n + 2
in dom (f | (n + 3))
by A40, A42, A43, FINSEQ_3:25;
then A47:
f /. (n + 2) = (f | (n + 3)) /. (n + 2)
by FINSEQ_4:70;
reconsider NE1 =
H1(
n + 1) as non
empty Subset of
(TOP-REAL 2) by A40, NAT_1:11, TOPREAL1:23;
take
NE1
;
( NE1 = H1(n + 1) & ( for j being Nat
for F being Function of I[01],((TOP-REAL 2) | NE1) st 1 <= j & j + 1 <= (n + 1) + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. ((n + 1) + 2) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) ) )
thus
NE1 = H1(
n + 1)
;
for j being Nat
for F being Function of I[01],((TOP-REAL 2) | NE1) st 1 <= j & j + 1 <= (n + 1) + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. ((n + 1) + 2) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) )
let j be
Nat;
for F being Function of I[01],((TOP-REAL 2) | NE1) st 1 <= j & j + 1 <= (n + 1) + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. ((n + 1) + 2) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) )let G be
Function of
I[01],
((TOP-REAL 2) | NE1);
( 1 <= j & j + 1 <= (n + 1) + 2 & G is being_homeomorphism & G . 0 = f /. 1 & G . 1 = f /. ((n + 1) + 2) implies ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = G .: [.p1,p2.] & G . p1 = f /. j & G . p2 = f /. (j + 1) ) )
assume that A48:
1
<= j
and A49:
j + 1
<= (n + 1) + 2
and A50:
G is
being_homeomorphism
and A51:
G . 0 = f /. 1
and A52:
G . 1
= f /. ((n + 1) + 2)
;
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = G .: [.p1,p2.] & G . p1 = f /. j & G . p2 = f /. (j + 1) )
A53:
G is
one-to-one
by A50, TOPS_2:def 5;
A54:
rng G = [#] ((TOP-REAL 2) | H1(n + 1))
by A50, TOPS_2:def 5;
A55:
dom G = [#] I[01]
by A50, TOPS_2:def 5;
A56:
rng G = L~ (f | (n + 3))
by A54, PRE_TOPC:def 5;
set pp =
(G ") . (f /. (n + 2));
G is
onto
by A54, FUNCT_2:def 3;
then A57:
(G ") . (f /. (n + 2)) = (G ") . (f /. (n + 2))
by A53, TOPS_2:def 4;
A58:
n + 2
<= len (f | (n + 2))
by A36, A43, FINSEQ_1:59, XXREAL_0:2;
A59:
1
<= len (f | (n + 2))
by A36, A42, A43, FINSEQ_1:59, XXREAL_0:2;
A60:
n + 2
in dom (f | (n + 2))
by A42, A58, FINSEQ_3:25;
A61:
1
in dom (f | (n + 2))
by A59, FINSEQ_3:25;
A62:
f /. (n + 2) in rng G
by A40, A46, A47, A56, GOBOARD1:1, NAT_1:11;
then A63:
(G ") . (f /. (n + 2)) in dom G
by A53, A57, FUNCT_1:32;
A64:
f /. (n + 2) = G . ((G ") . (f /. (n + 2)))
by A53, A57, A62, FUNCT_1:32;
reconsider pp =
(G ") . (f /. (n + 2)) as
Real ;
A65:
(n + 1) + 1
<> (n + 2) + 1
;
A66:
n + 2
<> n + 3
;
A67:
n + 2
in dom f
by A42, A45, FINSEQ_3:25;
A68:
n + 3
in dom f
by A35, A36, FINSEQ_3:25;
A69:
1
<> pp
A70:
0 <= pp
by A63, BORSUK_1:43;
pp <= 1
by A63, BORSUK_1:43;
then A71:
pp < 1
by A69, XXREAL_0:1;
set pn =
f /. (n + 2);
set pn1 =
f /. ((n + 2) + 1);
A72:
f /. (n + 2) = (f | (n + 2)) /. (n + 2)
by A60, FINSEQ_4:70;
A73:
(f | (n + 2)) /. 1
= f /. 1
by A61, FINSEQ_4:70;
A74:
len (f | (n + 2)) = n + 2
by A36, A43, FINSEQ_1:59, XXREAL_0:2;
f | (n + 2) is
being_S-Seq
by A3, JORDAN3:4, NAT_1:11;
then
NE is_an_arc_of (f | (n + 2)) /. 1,
f /. (n + 2)
by A38, A72, A74, TOPREAL1:25;
then consider F being
Function of
I[01],
((TOP-REAL 2) | NE) such that A75:
F is
being_homeomorphism
and A76:
F . 0 = f /. 1
and A77:
F . 1
= f /. (n + 2)
by A73, TOPREAL1:def 1;
A78:
(n + 1) + 1
in dom f
by A42, A44, FINSEQ_3:25;
(n + 2) + 1
in dom f
by A35, A36, FINSEQ_3:25;
then
LSeg (
(f /. (n + 2)),
(f /. ((n + 2) + 1)))
is_an_arc_of f /. (n + 2),
f /. ((n + 2) + 1)
by A8, A65, A78, PARTFUN2:10, TOPREAL1:9;
then consider F9 being
Function of
I[01],
((TOP-REAL 2) | (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))))) such that A79:
F9 is
being_homeomorphism
and A80:
F9 . 0 = f /. (n + 2)
and A81:
F9 . 1
= f /. ((n + 2) + 1)
by TOPREAL1:def 1;
set Ex1 =
P[01] (
0,
(1 / 2),
((#) (0,1)),
((0,1) (#)));
set Ex2 =
P[01] (
(1 / 2),1,
((#) (0,1)),
((0,1) (#)));
set F1 =
F * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))));
set F19 =
F9 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))));
A82:
P[01] (
0,
(1 / 2),
((#) (0,1)),
((0,1) (#))) is
being_homeomorphism
by TREAL_1:17;
A83:
P[01] (
(1 / 2),1,
((#) (0,1)),
((0,1) (#))) is
being_homeomorphism
by TREAL_1:17;
A84:
dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = [#] (Closed-Interval-TSpace (0,(1 / 2)))
by A82, TOPS_2:def 5;
then A85:
dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = [.0,(1 / 2).]
by TOPMETR:18;
dom F = [#] I[01]
by A75, TOPS_2:def 5;
then A86:
rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = dom F
by A82, TOPMETR:20, TOPS_2:def 5;
then
rng (F * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) = rng F
by RELAT_1:28;
then
rng (F * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) = [#] ((TOP-REAL 2) | NE)
by A75, TOPS_2:def 5;
then A87:
rng (F * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) = H1(
n)
by A38, PRE_TOPC:def 5;
dom (F * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) = the
carrier of
(Closed-Interval-TSpace (0,(1 / 2)))
by A84, A86, RELAT_1:27;
then reconsider F1 =
F * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) as
Function of
(Closed-Interval-TSpace (0,(1 / 2))),
((TOP-REAL 2) | NE) by FUNCT_2:def 1;
A88:
F1 is
being_homeomorphism
by A75, A82, TOPMETR:20, TOPS_2:57;
then A89:
rng F1 =
[#] ((TOP-REAL 2) | NE)
by TOPS_2:def 5
.=
H1(
n)
by A38, PRE_TOPC:def 5
;
A90:
dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = [#] (Closed-Interval-TSpace ((1 / 2),1))
by A83, TOPS_2:def 5;
dom F9 = [#] I[01]
by A79, TOPS_2:def 5;
then A91:
rng (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = dom F9
by A83, TOPMETR:20, TOPS_2:def 5;
then
dom (F9 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) = the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by A90, RELAT_1:27;
then reconsider F19 =
F9 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) as
Function of
(Closed-Interval-TSpace ((1 / 2),1)),
((TOP-REAL 2) | (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))))) by FUNCT_2:def 1;
A92:
F19 is
being_homeomorphism
by A79, A83, TOPMETR:20, TOPS_2:57;
then A93:
rng F19 =
[#] ((TOP-REAL 2) | (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))))
by TOPS_2:def 5
.=
LSeg (
(f /. (n + 2)),
(f /. ((n + 2) + 1)))
by PRE_TOPC:def 5
;
set FF =
F1 +* F19;
reconsider T1 =
Closed-Interval-TSpace (
0,
(1 / 2)),
T2 =
Closed-Interval-TSpace (
(1 / 2),1) as
SubSpace of
I[01] by TOPMETR:20, TREAL_1:3;
A94:
H1(
n + 1)
= H1(
n)
\/ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))))
by A67, A68, TOPREAL3:38;
A95: the
carrier of
((TOP-REAL 2) | H1(n + 1)) =
[#] ((TOP-REAL 2) | H1(n + 1))
.=
H1(
n + 1)
by PRE_TOPC:def 5
;
dom F1 = the
carrier of
T1
by A84, A86, RELAT_1:27;
then reconsider g11 =
F1 as
Function of
T1,
((TOP-REAL 2) | NE1) by A87, A94, A95, RELSET_1:4, XBOOLE_1:7;
dom F19 = the
carrier of
T2
by A90, A91, RELAT_1:27;
then reconsider g22 =
F19 as
Function of
T2,
((TOP-REAL 2) | NE1) by A93, A94, A95, RELSET_1:4, XBOOLE_1:7;
A96:
[.0,(1 / 2).] = dom F1
by A10, A88, TOPS_2:def 5;
A97:
[.(1 / 2),1.] = dom F19
by A11, A92, TOPS_2:def 5;
A98:
1
/ 2
in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) }
;
A99:
1
/ 2
in { l where l is Real : ( 1 / 2 <= l & l <= 1 ) }
;
A100:
1
/ 2
in dom F1
by A96, A98, RCOMP_1:def 1;
A101:
1
/ 2
in dom F19
by A97, A99, RCOMP_1:def 1;
A102:
dom (F1 +* F19) =
[.0,(1 / 2).] \/ [.(1 / 2),1.]
by A96, A97, FUNCT_4:def 1
.=
[.0,1.]
by XXREAL_1:174
;
A103:
I[01] is
compact
by HEINE:4, TOPMETR:20;
A104:
(TOP-REAL 2) | NE1 is
T_2
by TOPMETR:2;
A105:
(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . (1 / 2) =
(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . ((0,(1 / 2)) (#))
by TREAL_1:def 2
.=
(
0,1)
(#)
by TREAL_1:13
.=
1
by TREAL_1:def 2
;
A106:
(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . (1 / 2) =
(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . ((#) ((1 / 2),1))
by TREAL_1:def 1
.=
(#) (
0,1)
by TREAL_1:13
.=
0
by TREAL_1:def 1
;
A107:
F1 . (1 / 2) = f /. (n + 2)
by A77, A100, A105, FUNCT_1:12;
A108:
F19 . (1 / 2) = f /. (n + 2)
by A80, A101, A106, FUNCT_1:12;
A109:
[.0,(1 / 2).] /\ [.(1 / 2),1.] = [.(1 / 2),(1 / 2).]
by XXREAL_1:143;
then A110:
(dom F1) /\ (dom F19) = {(1 / 2)}
by A96, A97, XXREAL_1:17;
A111:
for
x being
set holds
(
x in H1(
n)
/\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) iff
x = f /. (n + 2) )
proof
let x be
set ;
( x in H1(n) /\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) iff x = f /. (n + 2) )
thus
(
x in H1(
n)
/\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) implies
x = f /. (n + 2) )
( x = f /. (n + 2) implies x in H1(n) /\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) )proof
assume A112:
x in H1(
n)
/\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))))
;
x = f /. (n + 2)
then A113:
x in LSeg (
(f /. (n + 2)),
(f /. ((n + 2) + 1)))
by XBOOLE_0:def 4;
x in H1(
n)
by A112, XBOOLE_0:def 4;
then
x in union { (LSeg ((f | (n + 2)),k)) where k is Nat : ( 1 <= k & k + 1 <= len (f | (n + 2)) ) }
by TOPREAL1:def 4;
then consider X being
set such that A114:
x in X
and A115:
X in { (LSeg ((f | (n + 2)),k)) where k is Nat : ( 1 <= k & k + 1 <= len (f | (n + 2)) ) }
by TARSKI:def 4;
consider k being
Nat such that A116:
X = LSeg (
(f | (n + 2)),
k)
and A117:
1
<= k
and A118:
k + 1
<= len (f | (n + 2))
by A115;
A119:
len (f | (n + 2)) = n + (1 + 1)
by A36, A43, FINSEQ_1:59, XXREAL_0:2;
A120:
len (f | (n + 2)) = (n + 1) + 1
by A36, A43, FINSEQ_1:59, XXREAL_0:2;
then A121:
k <= n + 1
by A118, XREAL_1:6;
A122:
f is
s.n.c.
by A3;
A123:
f is
unfolded
by A3;
now not k < n + 1assume A124:
k < n + 1
;
contradictionA125:
1
<= 1
+ k
by NAT_1:11;
A126:
k + 1
<= len f
by A44, A118, A120, XXREAL_0:2;
A127:
k + 1
< (n + 1) + 1
by A124, XREAL_1:6;
set p19 =
f /. k;
set p29 =
f /. (k + 1);
n + 1
<= (n + 1) + 1
by NAT_1:11;
then
k <= n + 2
by A124, XXREAL_0:2;
then A128:
k in Seg (len (f | (n + 2)))
by A117, A119, FINSEQ_1:1;
A129:
k + 1
in Seg (len (f | (n + 2)))
by A118, A125, FINSEQ_1:1;
A130:
k in dom (f | (n + 2))
by A128, FINSEQ_1:def 3;
A131:
k + 1
in dom (f | (n + 2))
by A129, FINSEQ_1:def 3;
A132:
(f | (n + 2)) /. k = f /. k
by A130, FINSEQ_4:70;
A133:
(f | (n + 2)) /. (k + 1) = f /. (k + 1)
by A131, FINSEQ_4:70;
A134:
LSeg (
f,
k) =
LSeg (
(f /. k),
(f /. (k + 1)))
by A117, A126, TOPREAL1:def 3
.=
LSeg (
(f | (n + 2)),
k)
by A117, A118, A132, A133, TOPREAL1:def 3
;
LSeg (
f,
(n + 2))
= LSeg (
(f /. (n + 2)),
(f /. ((n + 2) + 1)))
by A36, A42, TOPREAL1:def 3;
then
LSeg (
(f | (n + 2)),
k)
misses LSeg (
(f /. (n + 2)),
(f /. ((n + 2) + 1)))
by A122, A127, A134, TOPREAL1:def 7;
then
(LSeg ((f | (n + 2)),k)) /\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) = {}
;
hence
contradiction
by A113, A114, A116, XBOOLE_0:def 4;
verum end;
then A135:
k = n + 1
by A121, XXREAL_0:1;
A136:
1
<= n + 1
by A117, A121, XXREAL_0:2;
A137:
(n + 1) + 1
<= len f
by A36, A43, XXREAL_0:2;
set p19 =
f /. (n + 1);
set p29 =
f /. ((n + 1) + 1);
A138:
n + 1
<= (n + 1) + 1
by NAT_1:11;
A139:
1
<= 1
+ n
by NAT_1:11;
A140:
1
<= 1
+ (n + 1)
by NAT_1:11;
A141:
n + 1
in Seg (len (f | (n + 2)))
by A119, A138, A139, FINSEQ_1:1;
A142:
(n + 1) + 1
in Seg (len (f | (n + 2)))
by A119, A140, FINSEQ_1:1;
A143:
n + 1
in dom (f | (n + 2))
by A141, FINSEQ_1:def 3;
A144:
(n + 1) + 1
in dom (f | (n + 2))
by A142, FINSEQ_1:def 3;
A145:
(f | (n + 2)) /. (n + 1) = f /. (n + 1)
by A143, FINSEQ_4:70;
A146:
(f | (n + 2)) /. ((n + 1) + 1) = f /. ((n + 1) + 1)
by A144, FINSEQ_4:70;
A147:
LSeg (
f,
(n + 1)) =
LSeg (
(f /. (n + 1)),
(f /. ((n + 1) + 1)))
by A136, A137, TOPREAL1:def 3
.=
LSeg (
(f | (n + 2)),
(n + 1))
by A119, A139, A145, A146, TOPREAL1:def 3
;
LSeg (
(f /. (n + 2)),
(f /. ((n + 2) + 1)))
= LSeg (
f,
((n + 1) + 1))
by A36, A42, TOPREAL1:def 3;
then A148:
x in (LSeg (f,(n + 1))) /\ (LSeg (f,((n + 1) + 1)))
by A113, A114, A116, A135, A147, XBOOLE_0:def 4;
1
<= n + 1
by NAT_1:11;
then
(LSeg (f,(n + 1))) /\ (LSeg (f,((n + 1) + 1))) = {(f /. ((n + 1) + 1))}
by A36, A123, TOPREAL1:def 6;
hence
x = f /. (n + 2)
by A148, TARSKI:def 1;
verum
end;
assume A149:
x = f /. (n + 2)
;
x in H1(n) /\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))))
then A150:
x in LSeg (
(f /. (n + 2)),
(f /. ((n + 2) + 1)))
by RLTOPSP1:68;
A151:
len (f | (n + 2)) = n + 2
by A36, A43, FINSEQ_1:59, XXREAL_0:2;
then A152:
dom (f | (n + 2)) = Seg (n + 2)
by FINSEQ_1:def 3;
n + 2
in Seg (n + 2)
by A42, FINSEQ_1:1;
then A153:
x = (f | (n + 2)) /. ((n + 1) + 1)
by A149, A152, FINSEQ_4:70;
1
<= n + 1
by NAT_1:11;
then A154:
x in LSeg (
(f | (n + 2)),
(n + 1))
by A151, A153, TOPREAL1:21;
A155:
1
<= n + 1
by NAT_1:11;
(n + 1) + 1
<= len (f | (n + 2))
by A36, A43, FINSEQ_1:59, XXREAL_0:2;
then
LSeg (
(f | (n + 2)),
(n + 1))
in { (LSeg ((f | (n + 2)),k)) where k is Nat : ( 1 <= k & k + 1 <= len (f | (n + 2)) ) }
by A155;
then
x in union { (LSeg ((f | (n + 2)),k)) where k is Nat : ( 1 <= k & k + 1 <= len (f | (n + 2)) ) }
by A154, TARSKI:def 4;
then
x in H1(
n)
by TOPREAL1:def 4;
hence
x in H1(
n)
/\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))))
by A150, XBOOLE_0:def 4;
verum
end;
f /. (n + 2) in rng F19
by A101, A108, FUNCT_1:def 3;
then A156:
{(f /. (n + 2))} c= rng F19
by ZFMISC_1:31;
A157:
F1 .: ((dom F1) /\ (dom F19)) =
Im (
F1,
(1 / 2))
by A96, A97, A109, XXREAL_1:17
.=
{(f /. (n + 2))}
by A100, A107, FUNCT_1:59
;
then A158:
rng (F1 +* F19) = H1(
n)
\/ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))))
by A89, A93, A156, TOPMETR2:2;
then A159:
rng (F1 +* F19) = [#] ((TOP-REAL 2) | H1(n + 1))
by A67, A68, A95, TOPREAL3:38;
rng (F1 +* F19) c= the
carrier of
((TOP-REAL 2) | H1(n + 1))
by A89, A93, A94, A95, A156, A157, TOPMETR2:2;
then reconsider FF =
F1 +* F19 as
Function of
I[01],
((TOP-REAL 2) | NE1) by A102, BORSUK_1:40, FUNCT_2:2;
A160:
rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = [#] (Closed-Interval-TSpace (0,1))
by A82, TOPS_2:def 5;
A161:
0 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) }
;
A162:
1
/ 2
in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) }
;
A163:
0 in dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))
by A85, A161, RCOMP_1:def 1;
A164:
1
/ 2
in dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))
by A85, A162, RCOMP_1:def 1;
A165:
(
P[01] (
0,
(1 / 2),
((#) (0,1)),
((0,1) (#))) is
one-to-one &
P[01] (
0,
(1 / 2),
((#) (0,1)),
((0,1) (#))) is
continuous )
by A82, TOPS_2:def 5;
A166:
(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . 0 =
(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . ((#) (0,(1 / 2)))
by TREAL_1:def 1
.=
(#) (
0,1)
by TREAL_1:13
.=
0
by TREAL_1:def 1
;
A167:
P[01] (
0,
(1 / 2),
((#) (0,1)),
((0,1) (#))) is
onto
by A160, FUNCT_2:def 3;
then A168:
((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . 0 =
((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . 0
by A165, TOPS_2:def 4
.=
0
by A163, A165, A166, FUNCT_1:32
;
A169:
(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . (1 / 2) =
(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . ((#) ((1 / 2),1))
by TREAL_1:def 1
.=
(#) (
0,1)
by TREAL_1:13
.=
0
by TREAL_1:def 1
;
A170:
((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . 1 =
((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . 1
by A167, A165, TOPS_2:def 4
.=
1
/ 2
by A105, A164, A165, FUNCT_1:32
;
A171:
(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . 1 =
(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . (((1 / 2),1) (#))
by TREAL_1:def 2
.=
(
0,1)
(#)
by TREAL_1:13
.=
1
by TREAL_1:def 2
;
A172:
LSeg (
(f /. (n + 2)),
(f /. ((n + 2) + 1)))
= F19 .: [.(1 / 2),1.]
by A9, A93, RELSET_1:22;
A173:
FF . (1 / 2) = f /. (n + 2)
by A101, A108, FUNCT_4:13;
A174:
for
x being
set st
x in [.0,(1 / 2).] &
x <> 1
/ 2 holds
not
x in dom F19
A177:
FF .: [.(1 / 2),1.] c= F19 .: [.(1 / 2),1.]
proof
let a be
object ;
TARSKI:def 3 ( not a in FF .: [.(1 / 2),1.] or a in F19 .: [.(1 / 2),1.] )
assume
a in FF .: [.(1 / 2),1.]
;
a in F19 .: [.(1 / 2),1.]
then consider x being
object such that
x in dom FF
and A178:
x in [.(1 / 2),1.]
and A179:
a = FF . x
by FUNCT_1:def 6;
FF . x = F19 . x
by A97, A178, FUNCT_4:13;
hence
a in F19 .: [.(1 / 2),1.]
by A97, A178, A179, FUNCT_1:def 6;
verum
end;
F19 .: [.(1 / 2),1.] c= FF .: [.(1 / 2),1.]
proof
let a be
object ;
TARSKI:def 3 ( not a in F19 .: [.(1 / 2),1.] or a in FF .: [.(1 / 2),1.] )
assume
a in F19 .: [.(1 / 2),1.]
;
a in FF .: [.(1 / 2),1.]
then consider x being
object such that A180:
x in dom F19
and A181:
x in [.(1 / 2),1.]
and A182:
a = F19 . x
by FUNCT_1:def 6;
A183:
x in dom FF
by A180, FUNCT_4:12;
a = FF . x
by A180, A182, FUNCT_4:13;
hence
a in FF .: [.(1 / 2),1.]
by A181, A183, FUNCT_1:def 6;
verum
end;
then A184:
FF .: [.(1 / 2),1.] = F19 .: [.(1 / 2),1.]
by A177;
set GF =
(G ") * FF;
A185:
0 in dom FF
by A102, BORSUK_1:40, BORSUK_1:43;
A186:
1
in dom FF
by A102, BORSUK_1:40, BORSUK_1:43;
0 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) }
;
then
0 in [.0,(1 / 2).]
by RCOMP_1:def 1;
then A187:
FF . 0 =
F1 . 0
by A174, FUNCT_4:11
.=
f /. 1
by A76, A163, A166, FUNCT_1:13
;
1
in { l where l is Real : ( 1 / 2 <= l & l <= 1 ) }
;
then A188:
1
in dom F19
by A97, RCOMP_1:def 1;
then A189:
FF . 1 =
F19 . 1
by FUNCT_4:13
.=
f /. ((n + 2) + 1)
by A81, A171, A188, FUNCT_1:12
;
A190:
0 in dom G
by A55, BORSUK_1:43;
A191:
G is
onto
by A54, FUNCT_2:def 3;
then A192:
(G ") . (f /. 1) =
(G ") . (f /. 1)
by A53, TOPS_2:def 4
.=
0
by A51, A53, A190, FUNCT_1:32
;
then A193:
((G ") * FF) . 0 = 0
by A185, A187, FUNCT_1:13;
A194:
1
in dom G
by A55, BORSUK_1:43;
A195:
(G ") . (f /. ((n + 2) + 1)) =
(G ") . (f /. ((n + 2) + 1))
by A191, A53, TOPS_2:def 4
.=
1
by A52, A53, A194, FUNCT_1:32
;
then A196:
((G ") * FF) . 1
= 1
by A186, A189, FUNCT_1:13;
reconsider ppp = 1
/ 2 as
Point of
I[01] by BORSUK_1:43;
TopSpaceMetr RealSpace is
T_2
by PCOMPS_1:34;
then A197:
I[01] is
T_2
by TOPMETR:2, TOPMETR:20, TOPMETR:def 6;
A198:
T1 is
compact
by HEINE:4;
A199:
T2 is
compact
by HEINE:4;
A200:
F1 is
continuous
by A88, TOPS_2:def 5;
A201:
F19 is
continuous
by A92, TOPS_2:def 5;
A202:
(TOP-REAL 2) | NE is
SubSpace of
(TOP-REAL 2) | NE1
by A38, A94, TOPMETR:4;
A203:
(TOP-REAL 2) | (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) is
SubSpace of
(TOP-REAL 2) | NE1
by A94, TOPMETR:4;
A204:
g11 is
continuous
by A200, A202, PRE_TOPC:26;
A205:
g22 is
continuous
by A201, A203, PRE_TOPC:26;
A206:
[#] T1 = [.0,(1 / 2).]
by TOPMETR:18;
A207:
[#] T2 = [.(1 / 2),1.]
by TOPMETR:18;
then A208:
([#] T1) \/ ([#] T2) = [#] I[01]
by A206, BORSUK_1:40, XXREAL_1:174;
([#] T1) /\ ([#] T2) = {ppp}
by A206, A207, XXREAL_1:418;
then reconsider FF =
FF as
continuous Function of
I[01],
((TOP-REAL 2) | NE1) by A107, A108, A197, A198, A199, A204, A205, A208, COMPTS_1:20;
A209:
F1 is
one-to-one
by A88, TOPS_2:def 5;
A210:
F19 is
one-to-one
by A92, TOPS_2:def 5;
for
x1,
x2 being
set st
x1 in dom F19 &
x2 in (dom F1) \ (dom F19) holds
F19 . x1 <> F1 . x2
proof
let x1,
x2 be
set ;
( x1 in dom F19 & x2 in (dom F1) \ (dom F19) implies F19 . x1 <> F1 . x2 )
assume that A211:
x1 in dom F19
and A212:
x2 in (dom F1) \ (dom F19)
;
F19 . x1 <> F1 . x2
assume A213:
F19 . x1 = F1 . x2
;
contradiction
A214:
F19 . x1 in LSeg (
(f /. (n + 2)),
(f /. ((n + 2) + 1)))
by A93, A211, FUNCT_2:4;
A215:
x2 in dom F1
by A212, XBOOLE_0:def 5;
A216:
not
x2 in dom F19
by A212, XBOOLE_0:def 5;
F1 . x2 in NE
by A38, A89, A212, FUNCT_2:4;
then
F1 . x2 in NE /\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))))
by A213, A214, XBOOLE_0:def 4;
then
F1 . x2 = f /. (n + 2)
by A38, A111;
hence
contradiction
by A100, A101, A107, A209, A215, A216, FUNCT_1:def 4;
verum
end;
then A217:
FF is
one-to-one
by A209, A210, TOPMETR2:1;
A218:
G " is
being_homeomorphism
by A50, TOPS_2:56;
FF is
being_homeomorphism
by A103, A104, A159, A217, COMPTS_1:17;
then A219:
(G ") * FF is
being_homeomorphism
by A218, TOPS_2:57;
then A220:
(G ") * FF is
continuous
by TOPS_2:def 5;
A221:
dom ((G ") * FF) = [#] I[01]
by A219, TOPS_2:def 5;
A222:
rng ((G ") * FF) = [#] I[01]
by A219, TOPS_2:def 5;
A223:
(G ") * FF is
one-to-one
by A219, TOPS_2:def 5;
then A224:
dom (((G ") * FF) ") = [#] I[01]
by A222, TOPS_2:49;
A225:
rng G =
[#] ((TOP-REAL 2) | H1(n + 1))
by A50, TOPS_2:def 5
.=
rng FF
by A67, A68, A95, A158, TOPREAL3:38
;
A226:
G * ((G ") * FF) =
FF * (G * (G "))
by RELAT_1:36
.=
(id (rng G)) * FF
by A53, A54, TOPS_2:52
.=
FF
by A225, RELAT_1:54
;
A227:
1
/ 2
in dom ((G ") * FF)
by A221, BORSUK_1:43;
then A228:
((G ") * FF) . (1 / 2) in rng ((G ") * FF)
by FUNCT_1:def 3;
A229:
((G ") * FF) . (1 / 2) =
(G ") . (FF . (1 / 2))
by A227, FUNCT_1:12
.=
pp
by A101, A108, FUNCT_4:13
;
A230:
[.pp,1.] c= ((G ") * FF) .: [.(1 / 2),1.]
proof
let a be
object ;
TARSKI:def 3 ( not a in [.pp,1.] or a in ((G ") * FF) .: [.(1 / 2),1.] )
assume
a in [.pp,1.]
;
a in ((G ") * FF) .: [.(1 / 2),1.]
then
a in { l where l is Real : ( pp <= l & l <= 1 ) }
by RCOMP_1:def 1;
then consider l1 being
Real such that A231:
l1 = a
and A232:
pp <= l1
and A233:
l1 <= 1
;
A234:
0 <= pp
by A228, A229, BORSUK_1:43;
set cos =
(((G ") * FF) ") . l1;
l1 in dom (((G ") * FF) ")
by A224, A232, A233, A234, BORSUK_1:43;
then A235:
(((G ") * FF) ") . l1 in rng (((G ") * FF) ")
by FUNCT_1:def 3;
A236:
l1 in rng ((G ") * FF)
by A222, A232, A233, A234, BORSUK_1:43;
(G ") * FF is
onto
by A222, FUNCT_2:def 3;
then A237:
((G ") * FF) . ((((G ") * FF) ") . l1) =
((G ") * FF) . ((((G ") * FF) ") . l1)
by A223, TOPS_2:def 4
.=
l1
by A223, A236, FUNCT_1:35
;
reconsider cos =
(((G ") * FF) ") . l1 as
Real ;
reconsider A3 =
cos,
A4 = 1,
A5 = 1
/ 2 as
Point of
I[01] by A235, BORSUK_1:43;
reconsider A1 =
((G ") * FF) . A3,
A2 =
((G ") * FF) . A4 as
Point of
I[01] ;
reconsider Fhc =
A1,
Fh0 =
A2,
Fh12 =
((G ") * FF) . A5 as
Real ;
A238:
cos <= 1
proof
assume
cos > 1
;
contradiction
then
Fhc > Fh0
by A193, A196, A220, A223, JORDAN5A:16;
hence
contradiction
by A102, A189, A195, A233, A237, BORSUK_1:40, FUNCT_1:13;
verum
end;
cos >= 1
/ 2
then
cos in { l where l is Real : ( 1 / 2 <= l & l <= 1 ) }
by A238;
then
cos in [.(1 / 2),1.]
by RCOMP_1:def 1;
hence
a in ((G ") * FF) .: [.(1 / 2),1.]
by A221, A231, A235, A237, FUNCT_1:def 6;
verum
end;
((G ") * FF) .: [.(1 / 2),1.] c= [.pp,1.]
proof
let a be
object ;
TARSKI:def 3 ( not a in ((G ") * FF) .: [.(1 / 2),1.] or a in [.pp,1.] )
assume
a in ((G ") * FF) .: [.(1 / 2),1.]
;
a in [.pp,1.]
then consider x being
object such that
x in dom ((G ") * FF)
and A239:
x in [.(1 / 2),1.]
and A240:
a = ((G ") * FF) . x
by FUNCT_1:def 6;
x in { l where l is Real : ( 1 / 2 <= l & l <= 1 ) }
by A239, RCOMP_1:def 1;
then consider l1 being
Real such that A241:
l1 = x
and A242:
1
/ 2
<= l1
and A243:
l1 <= 1
;
reconsider ll =
l1,
pol = 1
/ 2 as
Point of
I[01] by A242, A243, BORSUK_1:43;
reconsider A1 =
((G ") * FF) . 1[01],
A2 =
((G ") * FF) . ll,
A3 =
((G ") * FF) . pol as
Point of
I[01] ;
reconsider A4 =
A1,
A5 =
A2,
A6 =
A3 as
Real ;
A244:
A4 >= A5
A5 >= A6
then
A5 in { l where l is Real : ( pp <= l & l <= 1 ) }
by A196, A229, A244, BORSUK_1:def 15;
hence
a in [.pp,1.]
by A240, A241, RCOMP_1:def 1;
verum
end;
then
[.pp,1.] = ((G ") * FF) .: [.(1 / 2),1.]
by A230;
then A245:
G .: [.pp,1.] = LSeg (
(f /. (n + 2)),
(f /. ((n + 2) + 1)))
by A172, A184, A226, RELAT_1:126;
ex
p1,
p2 being
Real st
(
p1 < p2 &
0 <= p1 &
p1 <= 1 &
0 <= p2 &
p2 <= 1 &
LSeg (
f,
j)
= G .: [.p1,p2.] &
G . p1 = f /. j &
G . p2 = f /. (j + 1) )
proof
per cases
( j + 1 <= n + 2 or j + 1 > n + 2 )
;
suppose
j + 1
<= n + 2
;
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = G .: [.p1,p2.] & G . p1 = f /. j & G . p2 = f /. (j + 1) )then consider r1,
r2 being
Real such that A246:
r1 < r2
and A247:
0 <= r1
and A248:
r1 <= 1
and
0 <= r2
and A249:
r2 <= 1
and A250:
LSeg (
f,
j)
= F .: [.r1,r2.]
and A251:
F . r1 = f /. j
and A252:
F . r2 = f /. (j + 1)
by A39, A48, A75, A76, A77;
set f1 =
((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r1;
set f2 =
((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r2;
A253:
(
P[01] (
0,
(1 / 2),
((#) (0,1)),
((0,1) (#))) is
continuous &
P[01] (
0,
(1 / 2),
((#) (0,1)),
((0,1) (#))) is
one-to-one )
by A82, TOPS_2:def 5;
A254:
dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = [#] (Closed-Interval-TSpace (0,(1 / 2)))
by A82, TOPS_2:def 5;
A255:
rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = [#] (Closed-Interval-TSpace (0,1))
by A82, TOPS_2:def 5;
then A256:
P[01] (
0,
(1 / 2),
((#) (0,1)),
((0,1) (#))) is
onto
by FUNCT_2:def 3;
then A257:
((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r1 = ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r1
by A253, TOPS_2:def 4;
A258:
((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r2 = ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r2
by A253, A256, TOPS_2:def 4;
A259:
rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) =
[#] I[01]
by A82, TOPMETR:20, TOPS_2:def 5
.=
the
carrier of
I[01]
;
then A260:
r1 in rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))
by A247, A248, BORSUK_1:43;
A261:
r2 in rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))
by A246, A247, A249, A259, BORSUK_1:43;
A262:
((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r1 in the
carrier of
(Closed-Interval-TSpace (0,(1 / 2)))
by A253, A254, A257, A260, FUNCT_1:32;
A263:
((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r2 in the
carrier of
(Closed-Interval-TSpace (0,(1 / 2)))
by A253, A254, A258, A261, FUNCT_1:32;
A264:
((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r1 in [.0,(1 / 2).]
by A262, TOPMETR:18;
A265:
((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r2 in [.0,(1 / 2).]
by A263, TOPMETR:18;
reconsider f1 =
((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r1,
f2 =
((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r2 as
Real ;
reconsider r19 =
r1,
r29 =
r2 as
Point of
(Closed-Interval-TSpace (0,1)) by A246, A247, A248, A249, BORSUK_1:43, TOPMETR:20;
A266:
(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) " is
being_homeomorphism
by A82, TOPS_2:56;
A267:
f1 = ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r19
;
A268:
f2 = ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r29
;
A269:
(
(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) " is
continuous &
(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) " is
one-to-one )
by A266, TOPS_2:def 5;
then A270:
f1 < f2
by A168, A170, A246, A267, A268, JORDAN5A:15;
A271:
[.0,(1 / 2).] c= [.0,1.]
by XXREAL_1:34;
A272:
r1 = (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . f1
by A253, A257, A260, FUNCT_1:32;
A273:
r2 = (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . f2
by A253, A258, A261, FUNCT_1:32;
A274:
f1 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) }
by A264, RCOMP_1:def 1;
A275:
f2 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) }
by A265, RCOMP_1:def 1;
A276:
ex
ff1 being
Real st
(
ff1 = f1 &
0 <= ff1 &
ff1 <= 1
/ 2 )
by A274;
ex
ff2 being
Real st
(
ff2 = f2 &
0 <= ff2 &
ff2 <= 1
/ 2 )
by A275;
then A277:
(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) .: [.f1,f2.] = [.r1,r2.]
by A82, A105, A166, A270, A272, A273, A276, JORDAN5A:20;
A278:
F1 .: [.f1,f2.] c= FF .: [.f1,f2.]
proof
let a be
object ;
TARSKI:def 3 ( not a in F1 .: [.f1,f2.] or a in FF .: [.f1,f2.] )
assume
a in F1 .: [.f1,f2.]
;
a in FF .: [.f1,f2.]
then consider x being
object such that A279:
x in dom F1
and A280:
x in [.f1,f2.]
and A281:
a = F1 . x
by FUNCT_1:def 6;
x in dom FF
by A279, FUNCT_4:12;
hence
a in FF .: [.f1,f2.]
by A280, A281, A282, FUNCT_1:def 6;
verum
end;
FF .: [.f1,f2.] c= F1 .: [.f1,f2.]
proof
let a be
object ;
TARSKI:def 3 ( not a in FF .: [.f1,f2.] or a in F1 .: [.f1,f2.] )
assume
a in FF .: [.f1,f2.]
;
a in F1 .: [.f1,f2.]
then consider x being
object such that
x in dom FF
and A283:
x in [.f1,f2.]
and A284:
a = FF . x
by FUNCT_1:def 6;
A285:
[.f1,f2.] c= [.0,(1 / 2).]
by A264, A265, XXREAL_2:def 12;
hence
a in F1 .: [.f1,f2.]
by A96, A283, A284, A285, FUNCT_1:def 6;
verum
end; then
F1 .: [.f1,f2.] = FF .: [.f1,f2.]
by A278;
then A286:
F .: [.r1,r2.] = FF .: [.f1,f2.]
by A277, RELAT_1:126;
set e1 =
((G ") * FF) . f1;
set e2 =
((G ") * FF) . f2;
A287:
((G ") * FF) . f1 in the
carrier of
I[01]
by A264, A271, BORSUK_1:40, FUNCT_2:5;
A288:
((G ") * FF) . f2 in the
carrier of
I[01]
by A265, A271, BORSUK_1:40, FUNCT_2:5;
A289:
((G ") * FF) . f1 in { l where l is Real : ( 0 <= l & l <= 1 ) }
by A287, BORSUK_1:40, RCOMP_1:def 1;
A290:
((G ") * FF) . f2 in { l where l is Real : ( 0 <= l & l <= 1 ) }
by A288, BORSUK_1:40, RCOMP_1:def 1;
consider l1 being
Real such that A291:
l1 = ((G ") * FF) . f1
and A292:
0 <= l1
and A293:
l1 <= 1
by A289;
consider l2 being
Real such that A294:
l2 = ((G ") * FF) . f2
and
0 <= l2
and A295:
l2 <= 1
by A290;
reconsider f19 =
f1,
f29 =
f2 as
Point of
I[01] by A264, A265, A271, BORSUK_1:40;
A296:
((G ") * FF) . 0 = 0
by A185, A187, A192, FUNCT_1:13;
A297:
((G ") * FF) . 1
= 1
by A186, A189, A195, FUNCT_1:13;
A298:
l1 = ((G ") * FF) . f19
by A291;
l2 = ((G ") * FF) . f29
by A294;
then A299:
l1 < l2
by A220, A223, A270, A296, A297, A298, JORDAN5A:16;
A300:
f1 < f2
by A168, A170, A246, A267, A268, A269, JORDAN5A:15;
A301:
0 <= f1
by A264, A271, BORSUK_1:40, BORSUK_1:43;
f2 <= 1
by A265, A271, BORSUK_1:40, BORSUK_1:43;
then A302:
G .: [.l1,l2.] =
G .: (((G ") * FF) .: [.f1,f2.])
by A193, A196, A219, A291, A294, A300, A301, JORDAN5A:20, TOPMETR:20
.=
FF .: [.f1,f2.]
by A226, RELAT_1:126
;
A303:
FF . f19 = F . r19
proof
per cases
( f19 = 1 / 2 or f19 <> 1 / 2 )
;
suppose A304:
f19 = 1
/ 2
;
FF . f19 = F . r19then FF . f19 =
F19 . (1 / 2)
by A101, FUNCT_4:13
.=
F9 . 0
by A101, A169, FUNCT_1:12
.=
F . r19
by A77, A80, A105, A253, A255, A257, A304, FUNCT_1:32
;
hence
FF . f19 = F . r19
;
verum end; suppose
f19 <> 1
/ 2
;
FF . f19 = F . r19then FF . f19 =
F1 . f19
by A174, A264, FUNCT_4:11
.=
F . ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . f19)
by A85, A264, FUNCT_1:13
.=
F . r19
by A253, A255, A257, FUNCT_1:32
;
hence
FF . f19 = F . r19
;
verum end; end;
end; A305:
FF . f29 = F . r29
proof
per cases
( f29 = 1 / 2 or f29 <> 1 / 2 )
;
suppose A306:
f29 = 1
/ 2
;
FF . f29 = F . r29then FF . f29 =
F19 . (1 / 2)
by A101, FUNCT_4:13
.=
F9 . 0
by A101, A169, FUNCT_1:12
.=
F . r29
by A77, A80, A105, A253, A255, A258, A306, FUNCT_1:32
;
hence
FF . f29 = F . r29
;
verum end; suppose
f29 <> 1
/ 2
;
FF . f29 = F . r29then FF . f29 =
F1 . f29
by A174, A265, FUNCT_4:11
.=
F . ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . f29)
by A85, A265, FUNCT_1:13
.=
F . r29
by A253, A255, A258, FUNCT_1:32
;
hence
FF . f29 = F . r29
;
verum end; end;
end; A307:
G . l1 = f /. j
by A102, A226, A251, A291, A303, BORSUK_1:40, FUNCT_1:12;
G . l2 = f /. (j + 1)
by A102, A226, A252, A294, A305, BORSUK_1:40, FUNCT_1:12;
hence
ex
p1,
p2 being
Real st
(
p1 < p2 &
0 <= p1 &
p1 <= 1 &
0 <= p2 &
p2 <= 1 &
LSeg (
f,
j)
= G .: [.p1,p2.] &
G . p1 = f /. j &
G . p2 = f /. (j + 1) )
by A250, A286, A292, A293, A295, A299, A302, A307;
verum end; suppose
j + 1
> n + 2
;
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = G .: [.p1,p2.] & G . p1 = f /. j & G . p2 = f /. (j + 1) )then A308:
j + 1
= n + 3
by A41, A49, NAT_1:9;
then
LSeg (
f,
j)
= LSeg (
(f /. (n + 2)),
(f /. ((n + 2) + 1)))
by A36, A42, TOPREAL1:def 3;
hence
ex
p1,
p2 being
Real st
(
p1 < p2 &
0 <= p1 &
p1 <= 1 &
0 <= p2 &
p2 <= 1 &
LSeg (
f,
j)
= G .: [.p1,p2.] &
G . p1 = f /. j &
G . p2 = f /. (j + 1) )
by A52, A64, A70, A71, A245, A308;
verum end; end;
end;
hence
ex
p1,
p2 being
Real st
(
p1 < p2 &
0 <= p1 &
p1 <= 1 &
0 <= p2 &
p2 <= 1 &
LSeg (
f,
j)
= G .: [.p1,p2.] &
G . p1 = f /. j &
G . p2 = f /. (j + 1) )
;
verum
end;
A309:
for n being Nat holds S1[n]
from NAT_1:sch 2(A14, A33);
1 <= h1 + 2
by A12, XXREAL_0:2;
then
ex NE being non empty Subset of (TOP-REAL 2) st
( NE = H1(h1) & ( for j being Nat
for F being Function of I[01],((TOP-REAL 2) | NE) st 1 <= j & j + 1 <= h1 + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (h1 + 2) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) ) )
by A309;
hence
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = Ff .: [.p1,p2.] & Ff . p1 = f /. i & Ff . p2 = f /. (i + 1) )
by A1, A2, A4, A5, A6, A7, A13; verum