let f be FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: 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); :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: 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); :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum
end;
A33: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A34: S1[n] ; :: thesis: S1[n + 1]
assume that
A35: 1 <= (n + 1) + 2 and
A36: (n + 1) + 2 <= len f ; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: 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; :: thesis: 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); :: thesis: ( 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) ; :: thesis: 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
proof
assume pp = 1 ; :: thesis: contradiction
then f /. (n + 2) = f /. ((n + 1) + 2) by A52, A53, A57, A62, FUNCT_1:32;
hence contradiction by A8, A66, A67, A68, PARTFUN2:10; :: thesis: verum
end;
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 ; :: thesis: ( 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) ) :: thesis: ( 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)))) ; :: thesis: 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 :: thesis: not k < n + 1
assume A124: k < n + 1 ; :: thesis: contradiction
A125: 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; :: thesis: 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; :: thesis: verum
end;
assume A149: x = f /. (n + 2) ; :: thesis: 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; :: thesis: 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
proof
let x be set ; :: thesis: ( x in [.0,(1 / 2).] & x <> 1 / 2 implies not x in dom F19 )
assume that
A175: x in [.0,(1 / 2).] and
A176: x <> 1 / 2 ; :: thesis: not x in dom F19
assume x in dom F19 ; :: thesis: contradiction
then x in (dom F1) /\ (dom F19) by A96, A175, XBOOLE_0:def 4;
hence contradiction by A110, A176, TARSKI:def 1; :: thesis: verum
end;
A177: FF .: [.(1 / 2),1.] c= F19 .: [.(1 / 2),1.]
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in FF .: [.(1 / 2),1.] or a in F19 .: [.(1 / 2),1.] )
assume a in FF .: [.(1 / 2),1.] ; :: thesis: 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; :: thesis: verum
end;
F19 .: [.(1 / 2),1.] c= FF .: [.(1 / 2),1.]
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in F19 .: [.(1 / 2),1.] or a in FF .: [.(1 / 2),1.] )
assume a in F19 .: [.(1 / 2),1.] ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: F19 . x1 <> F1 . x2
assume A213: F19 . x1 = F1 . x2 ; :: thesis: 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; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not a in [.pp,1.] or a in ((G ") * FF) .: [.(1 / 2),1.] )
assume a in [.pp,1.] ; :: thesis: 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 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; :: thesis: verum
end;
((G ") * FF) .: [.(1 / 2),1.] c= [.pp,1.]
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ((G ") * FF) .: [.(1 / 2),1.] or a in [.pp,1.] )
assume a in ((G ") * FF) .: [.(1 / 2),1.] ; :: thesis: 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
proof
per cases ( l1 <> 1 / 2 or l1 = 1 / 2 ) ;
suppose l1 = 1 / 2 ; :: thesis: A5 >= A6
hence A5 >= A6 ; :: thesis: verum
end;
end;
end;
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; :: thesis: 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 ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not a in F1 .: [.f1,f2.] or a in FF .: [.f1,f2.] )
assume a in F1 .: [.f1,f2.] ; :: thesis: 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;
A282: now :: thesis: FF . x = F1 . x
per cases ( x <> 1 / 2 or x = 1 / 2 ) ;
suppose x <> 1 / 2 ; :: thesis: FF . x = F1 . x
hence FF . x = F1 . x by A10, A174, A279, FUNCT_4:11; :: thesis: verum
end;
suppose x = 1 / 2 ; :: thesis: FF . x = F1 . x
hence FF . x = F1 . x by A101, A107, A108, FUNCT_4:13; :: thesis: verum
end;
end;
end;
x in dom FF by A279, FUNCT_4:12;
hence a in FF .: [.f1,f2.] by A280, A281, A282, FUNCT_1:def 6; :: thesis: verum
end;
FF .: [.f1,f2.] c= F1 .: [.f1,f2.]
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in FF .: [.f1,f2.] or a in F1 .: [.f1,f2.] )
assume a in FF .: [.f1,f2.] ; :: thesis: 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;
now :: thesis: FF . x = F1 . x
per cases ( x <> 1 / 2 or x = 1 / 2 ) ;
suppose x <> 1 / 2 ; :: thesis: FF . x = F1 . x
hence FF . x = F1 . x by A174, A283, A285, FUNCT_4:11; :: thesis: verum
end;
suppose x = 1 / 2 ; :: thesis: FF . x = F1 . x
hence FF . x = F1 . x by A101, A107, A108, FUNCT_4:13; :: thesis: verum
end;
end;
end;
hence a in F1 .: [.f1,f2.] by A96, A283, A284, A285, FUNCT_1:def 6; :: thesis: 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 ; :: thesis: FF . f19 = F . r19
then 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 ; :: thesis: verum
end;
suppose f19 <> 1 / 2 ; :: thesis: FF . f19 = F . r19
then 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 ; :: thesis: verum
end;
end;
end;
A305: FF . f29 = F . r29
proof
per cases ( f29 = 1 / 2 or f29 <> 1 / 2 ) ;
suppose A306: f29 = 1 / 2 ; :: thesis: FF . f29 = F . r29
then 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 ; :: thesis: verum
end;
suppose f29 <> 1 / 2 ; :: thesis: FF . f29 = F . r29
then 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 ; :: thesis: 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; :: thesis: verum
end;
suppose j + 1 > n + 2 ; :: thesis: 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; :: thesis: 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) ) ; :: thesis: 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; :: thesis: verum