let f be FinSequence of (TOP-REAL 2); :: thesis:
let P be non empty Subset of (TOP-REAL 2); :: thesis:
let Ff be Function of I[01] ,((TOP-REAL 2) | P); :: thesis:
let i be Element of NAT ; :: thesis:
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:
A8: f is one-to-one by A3, TOPREAL1:def 10;
A9: the carrier of (Closed-Interval-TSpace (1 / 2),1) = [.(1 / 2),1.] by TOPMETR:25;
A10: [#] (Closed-Interval-TSpace 0 ,(1 / 2)) = [.0 ,(1 / 2).] by TOPMETR:25;
A11: [#] (Closed-Interval-TSpace (1 / 2),1) = [.(1 / 2),1.] by TOPMETR:25;
A12: len f >= 2 by A3, TOPREAL1:def 10;
deffunc H₁( Element of NAT ) -> Element of K21(the carrier of (TOP-REAL 2)) = L~ (f | ($1 + 2));
defpred S₁[ Element of NAT ] means ( 1 <= $1 + 2 & $1 + 2 <= len f implies ex NE being non empty Subset of (TOP-REAL 2) st
( NE = H₁($1) & ( for j being Element of 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:18;
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:97 ;
A14: S₁[ 0 ]

assume that
A15: 1 <= 0 + 2 and
A16: 0 + 2 <= len f ; :: thesis:
A17: 1 <= len (f | 2) by A15, A16, FINSEQ_1:80;
A18: 2 <= len (f | 2) by A16, FINSEQ_1:80;
then reconsider NE = H₁( 0 ) as non empty Subset of (TOP-REAL 2) by TOPREAL1:29;
take NE ; :: thesis:
thus NE = H₁( 0 ) ; :: thesis:
let j be Element of NAT ; :: thesis:
let F be Function of I[01] ,((TOP-REAL 2) | NE); :: thesis:
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:
j <= (1 + 1) - 1 by A20, XREAL_1:21;
then A24: j = 1 by A19, XXREAL_0:1;
A25: len (f | 2) = 2 by A16, FINSEQ_1:80;
A26: 1 in dom (f | 2) by A17, FINSEQ_3:27;
A27: 2 in dom (f | 2) by A18, FINSEQ_3:27;
A28: (f | 2) /. 1 = (f | 2) . 1 by A26, PARTFUN1:def 8;
A29: (f | 2) /. 2 = (f | 2) . 2 by A27, PARTFUN1:def 8;
A30: (f | 2) /. 1 = f /. 1 by A26, FINSEQ_4:85;
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 10
.= L~ <*((f | 2) /. 1),((f | 2) /. 2)*> by A25, A28, A29, FINSEQ_1:61
.= LSeg ((f | 2) /. 1),((f | 2) /. 2) by SPPOL_2:21
.= LSeg (f /. 1),(f /. 2) by A27, A30, FINSEQ_4:85
.= LSeg f,1 by A31, TOPREAL1:def 5 ;
take 0 ; :: thesis:
take 1 ; :: thesis:
thus ( 0 < 1 & 0 <= 0 & 0 <= 1 & 0 <= 1 & 1 <= 1 & LSeg f,j = F .: [.0 ,1.] & F . 0 = f /. j & F . 1 = f /. (j + 1) ) by A22, A23, A24, A32, BORSUK_1:83, FUNCT_2:45; :: thesis:

end;

A33: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis:
assume A34: S₁[n] ; :: thesis:
assume that
A35: 1 <= (n + 1) + 2 and
A36: (n + 1) + 2 <= len f ; :: thesis:
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 = H₁(n) and
A39: for j being Element of 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:80;
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:27;
then A47: f /. (n + 2) = (f | (n + 3)) /. (n + 2) by FINSEQ_4:85;
reconsider NE1 = H₁(n + 1) as non empty Subset of (TOP-REAL 2) by A40, NAT_1:11, TOPREAL1:29;
take NE1 ; :: thesis:
thus NE1 = H₁(n + 1) ; :: thesis:
let j be Element of NAT ; :: thesis:
let G be Function of I[01] ,((TOP-REAL 2) | NE1); :: thesis:
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:
A53: G is one-to-one by A50, TOPS_2:def 5;
A54: rng G = [#] ((TOP-REAL 2) | H₁(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 10;
set pp = (G " ) . (f /. (n + 2));
A57: (G " ) . (f /. (n + 2)) = (G " ) . (f /. (n + 2)) by A53, A54, TOPS_2:def 4;
A58: n + 2 <= len (f | (n + 2)) by A36, A43, FINSEQ_1:80, XXREAL_0:2;
A59: 1 <= len (f | (n + 2)) by A36, A42, A43, FINSEQ_1:80, XXREAL_0:2;
A60: n + 2 in dom (f | (n + 2)) by A42, A58, FINSEQ_3:27;
A61: 1 in dom (f | (n + 2)) by A59, FINSEQ_3:27;
A62: f /. (n + 2) in rng G by A40, A46, A47, A56, GOBOARD1:16, NAT_1:11;
then A63: (G " ) . (f /. (n + 2)) in dom G by A53, A57, FUNCT_1:54;
A64: f /. (n + 2) = G . ((G " ) . (f /. (n + 2))) by A53, A57, A62, FUNCT_1:54;
reconsider pp = (G " ) . (f /. (n + 2)) as Real by A55, A63, BORSUK_1:83;
A65: (n + 1) + 1 <> (n + 2) + 1 ;
A66: n + 2 <> n + 3 ;
A67: n + 2 in dom f by A42, A45, FINSEQ_3:27;
A68: n + 3 in dom f by A35, A36, FINSEQ_3:27;
A69: 1 <> pp

proof

assume pp = 1 ; :: thesis:
then f /. (n + 2) = f /. ((n + 1) + 2) by A52, A53, A57, A62, FUNCT_1:54;
hence contradiction by A8, A66, A67, A68, PARTFUN2:17; :: thesis:

end;

A70: 0 <= pp by A63, BORSUK_1:86;
pp <= 1 by A63, BORSUK_1:86;
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:85;
A73: (f | (n + 2)) /. 1 = f /. 1 by A61, FINSEQ_4:85;
A74: len (f | (n + 2)) = n + 2 by A36, A43, FINSEQ_1:80, XXREAL_0:2;
f | (n + 2) is being_S-Seq by A3, JORDAN3:37, NAT_1:11;
then NE is_an_arc_of (f | (n + 2)) /. 1,f /. (n + 2) by A38, A72, A74, TOPREAL1:31;
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 2;
A78: (n + 1) + 1 in dom f by A42, A44, FINSEQ_3:27;
(n + 2) + 1 in dom f by A35, A36, FINSEQ_3:27;
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:17, TOPREAL1:15;
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 2;
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:20;
A83: P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ) is being_homeomorphism by TREAL_1:20;
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:25;
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:27, TOPS_2:def 5;
then rng (F * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) = rng F by RELAT_1:47;
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 (#) ))) = H₁(n) by A38, PRE_TOPC:def 10;
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:46;
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:27, TOPS_2:71;
then A89: rng F1 = [#] ((TOP-REAL 2) | NE) by TOPS_2:def 5
.= H₁(n) by A38, PRE_TOPC:def 10 ;
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:27, 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:46;
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:27, TOPS_2:71;
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 10 ;
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:27, TREAL_1:6;
A94: H₁(n + 1) = H₁(n) \/ (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1))) by A67, A68, TOPREAL3:45;
A95: the carrier of ((TOP-REAL 2) | H₁(n + 1)) = [#] ((TOP-REAL 2) | H₁(n + 1))
.= H₁(n + 1) by PRE_TOPC:def 10 ;
dom F1 = the carrier of T1 by A84, A86, RELAT_1:46;
then reconsider g11 = F1 as Function of T1,((TOP-REAL 2) | NE1) by A87, A94, A95, RELSET_1:11, XBOOLE_1:7;
dom F19 = the carrier of T2 by A90, A91, RELAT_1:46;
then reconsider g22 = F19 as Function of T2,((TOP-REAL 2) | NE1) by A93, A94, A95, RELSET_1:11, 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:11, TOPMETR:27;
A104: (TOP-REAL 2) | NE1 is T_2 by TOPMETR:3;
A105: dom (F1 +* F19) = [#] I[01] by A102, BORSUK_1:83;
A106: (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:16
.= 1 by TREAL_1:def 2 ;
A107: (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:16
.= 0 by TREAL_1:def 1 ;
A108: F1 . (1 / 2) = f /. (n + 2) by A77, A100, A106, FUNCT_1:22;
A109: F19 . (1 / 2) = f /. (n + 2) by A80, A101, A107, FUNCT_1:22;
A110: [.0 ,(1 / 2).] /\ [.(1 / 2),1.] = [.(1 / 2),(1 / 2).] by XXREAL_1:143;
then A111: (dom F1) /\ (dom F19) = {(1 / 2)} by A96, A97, XXREAL_1:17;
A112: for x being set holds
( x in H₁(n) /\ (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1))) iff x = f /. (n + 2) )

proof

let x be set ; :: thesis:
thus ( x in H₁(n) /\ (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1))) implies x = f /. (n + 2) ) :: thesis:

proof

assume A113: x in H₁(n) /\ (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1))) ; :: thesis:
then A114: x in LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) by XBOOLE_0:def 4;
x in H₁(n) by A113, XBOOLE_0:def 4;
then x in union { (LSeg (f | (n + 2)),k) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | (n + 2)) ) } by TOPREAL1:def 6;
then consider X being set such that
A115: x in X and
A116: X in { (LSeg (f | (n + 2)),k) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | (n + 2)) ) } by TARSKI:def 4;
consider k being Element of NAT such that
A117: X = LSeg (f | (n + 2)),k and
A118: 1 <= k and
A119: k + 1 <= len (f | (n + 2)) by A116;
A120: len (f | (n + 2)) = n + (1 + 1) by A36, A43, FINSEQ_1:80, XXREAL_0:2;
A121: len (f | (n + 2)) = (n + 1) + 1 by A36, A43, FINSEQ_1:80, XXREAL_0:2;
then A122: k <= n + 1 by A119, XREAL_1:8;
A123: f is s.n.c. by A3, TOPREAL1:def 10;
A124: f is unfolded by A3, TOPREAL1:def 10;

now

assume A125: k < n + 1 ; :: thesis:
A126: 1 <= 1 + k by NAT_1:11;
A127: k + 1 <= len f by A44, A119, A121, XXREAL_0:2;
A128: k + 1 < (n + 1) + 1 by A125, XREAL_1:8;
set p19 = f /. k;
set p29 = f /. (k + 1);
n + 1 <= (n + 1) + 1 by NAT_1:11;
then k <= n + 2 by A125, XXREAL_0:2;
then A129: k in Seg (len (f | (n + 2))) by A118, A120, FINSEQ_1:3;
A130: k + 1 in Seg (len (f | (n + 2))) by A119, A126, FINSEQ_1:3;
A131: k in dom (f | (n + 2)) by A129, FINSEQ_1:def 3;
A132: k + 1 in dom (f | (n + 2)) by A130, FINSEQ_1:def 3;
A133: (f | (n + 2)) /. k = f /. k by A131, FINSEQ_4:85;
A134: (f | (n + 2)) /. (k + 1) = f /. (k + 1) by A132, FINSEQ_4:85;
A135: LSeg f,k = LSeg (f /. k),(f /. (k + 1)) by A118, A127, TOPREAL1:def 5
.= LSeg (f | (n + 2)),k by A118, A119, A133, A134, TOPREAL1:def 5 ;
LSeg f,(n + 2) = LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) by A36, A42, TOPREAL1:def 5;
then LSeg (f | (n + 2)),k misses LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) by A123, A128, A135, TOPREAL1:def 9;
then (LSeg (f | (n + 2)),k) /\ (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1))) = {} by XBOOLE_0:def 7;
hence contradiction by A114, A115, A117, XBOOLE_0:def 4; :: thesis:

end;

then A136: k = n + 1 by A122, XXREAL_0:1;
A137: 1 <= n + 1 by A118, A122, XXREAL_0:2;
A138: (n + 1) + 1 <= len f by A36, A43, XXREAL_0:2;
set p19 = f /. (n + 1);
set p29 = f /. ((n + 1) + 1);
A139: n + 1 <= (n + 1) + 1 by NAT_1:11;
A140: 1 <= 1 + n by NAT_1:11;
A141: 1 <= 1 + (n + 1) by NAT_1:11;
A142: n + 1 in Seg (len (f | (n + 2))) by A120, A139, A140, FINSEQ_1:3;
A143: (n + 1) + 1 in Seg (len (f | (n + 2))) by A120, A141, FINSEQ_1:3;
A144: n + 1 in dom (f | (n + 2)) by A142, FINSEQ_1:def 3;
A145: (n + 1) + 1 in dom (f | (n + 2)) by A143, FINSEQ_1:def 3;
A146: (f | (n + 2)) /. (n + 1) = f /. (n + 1) by A144, FINSEQ_4:85;
A147: (f | (n + 2)) /. ((n + 1) + 1) = f /. ((n + 1) + 1) by A145, FINSEQ_4:85;
A148: LSeg f,(n + 1) = LSeg (f /. (n + 1)),(f /. ((n + 1) + 1)) by A137, A138, TOPREAL1:def 5
.= LSeg (f | (n + 2)),(n + 1) by A120, A140, A146, A147, TOPREAL1:def 5 ;
LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) = LSeg f,((n + 1) + 1) by A36, A42, TOPREAL1:def 5;
then A149: x in (LSeg f,(n + 1)) /\ (LSeg f,((n + 1) + 1)) by A114, A115, A117, A136, A148, 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, A124, TOPREAL1:def 8;
hence x = f /. (n + 2) by A149, TARSKI:def 1; :: thesis:

end;

assume A150: x = f /. (n + 2) ; :: thesis:
then A151: x in LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) by RLTOPSP1:69;
A152: len (f | (n + 2)) = n + 2 by A36, A43, FINSEQ_1:80, XXREAL_0:2;
then A153: dom (f | (n + 2)) = Seg (n + 2) by FINSEQ_1:def 3;
n + 2 in Seg (n + 2) by A42, FINSEQ_1:3;
then A154: x = (f | (n + 2)) /. ((n + 1) + 1) by A150, A153, FINSEQ_4:85;
1 <= n + 1 by NAT_1:11;
then A155: x in LSeg (f | (n + 2)),(n + 1) by A152, A154, TOPREAL1:27;
A156: 1 <= n + 1 by NAT_1:11;
(n + 1) + 1 <= len (f | (n + 2)) by A36, A43, FINSEQ_1:80, XXREAL_0:2;
then LSeg (f | (n + 2)),(n + 1) in { (LSeg (f | (n + 2)),k) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | (n + 2)) ) } by A156;
then x in union { (LSeg (f | (n + 2)),k) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | (n + 2)) ) } by A155, TARSKI:def 4;
then x in H₁(n) by TOPREAL1:def 6;
hence x in H₁(n) /\ (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1))) by A151, XBOOLE_0:def 4; :: thesis:

end;

f /. (n + 2) in rng F19 by A101, A109, FUNCT_1:def 5;
then A157: {(f /. (n + 2))} c= rng F19 by ZFMISC_1:37;
A158: F1 .: ((dom F1) /\ (dom F19)) = Im F1,(1 / 2) by A96, A97, A110, XXREAL_1:17
.= {(f /. (n + 2))} by A100, A108, FUNCT_1:117 ;
then A159: rng (F1 +* F19) = H₁(n) \/ (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1))) by A89, A93, A157, TOPMETR2:3;
then A160: rng (F1 +* F19) = [#] ((TOP-REAL 2) | H₁(n + 1)) by A67, A68, A95, TOPREAL3:45;
rng (F1 +* F19) c= the carrier of ((TOP-REAL 2) | H₁(n + 1)) by A89, A93, A94, A95, A157, A158, TOPMETR2:3;
then reconsider FF = F1 +* F19 as Function of I[01] ,((TOP-REAL 2) | NE1) by A102, BORSUK_1:83, FUNCT_2:4;
A161: rng (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) = [#] (Closed-Interval-TSpace 0 ,1) by A82, TOPS_2:def 5;
A162: 0 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) } ;
A163: 1 / 2 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) } ;
A164: 0 in dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) by A85, A162, RCOMP_1:def 1;
A165: 1 / 2 in dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) by A85, A163, RCOMP_1:def 1;
A166: ( 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;
A167: (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:16
.= 0 by TREAL_1:def 1 ;
A168: ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . 0 = ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . 0 by A161, A166, TOPS_2:def 4
.= 0 by A164, A166, A167, FUNCT_1:54 ;
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:16
.= 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 A161, A166, TOPS_2:def 4
.= 1 / 2 by A106, A165, A166, FUNCT_1:54 ;
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:16
.= 1 by TREAL_1:def 2 ;
A172: LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) = F19 .: [.(1 / 2),1.] by A9, A93, FUNCT_2:45;
A173: FF . (1 / 2) = f /. (n + 2) by A101, A109, FUNCT_4:14;
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:
assume that
A175: x in [.0 ,(1 / 2).] and
A176: x <> 1 / 2 ; :: thesis:
assume x in dom F19 ; :: thesis:
then x in (dom F1) /\ (dom F19) by A96, A175, XBOOLE_0:def 4;
hence contradiction by A111, A176, TARSKI:def 1; :: thesis:

end;

A177: FF .: [.(1 / 2),1.] c= F19 .: [.(1 / 2),1.]

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in FF .: [.(1 / 2),1.] ; :: thesis:
then consider x being set such that
x in dom FF and
A178: x in [.(1 / 2),1.] and
A179: a = FF . x by FUNCT_1:def 12;
FF . x = F19 . x by A97, A178, FUNCT_4:14;
hence a in F19 .: [.(1 / 2),1.] by A97, A178, A179, FUNCT_1:def 12; :: thesis:

end;

F19 .: [.(1 / 2),1.] c= FF .: [.(1 / 2),1.]

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in F19 .: [.(1 / 2),1.] ; :: thesis:
then consider x being set such that
A180: x in dom F19 and
A181: x in [.(1 / 2),1.] and
A182: a = F19 . x by FUNCT_1:def 12;
A183: x in dom FF by A180, FUNCT_4:13;
a = FF . x by A180, A182, FUNCT_4:14;
hence a in FF .: [.(1 / 2),1.] by A181, A183, FUNCT_1:def 12; :: thesis:

end;

then A184: FF .: [.(1 / 2),1.] = F19 .: [.(1 / 2),1.] by A177, XBOOLE_0:def 10;
set GF = (G " ) * FF;
A185: 0 in dom FF by A102, BORSUK_1:83, BORSUK_1:86;
A186: 1 in dom FF by A102, BORSUK_1:83, BORSUK_1:86;
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:12
.= f /. 1 by A76, A164, A167, FUNCT_1:23 ;
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:14
.= f /. ((n + 2) + 1) by A81, A171, A188, FUNCT_1:22 ;
A190: 0 in dom G by A55, BORSUK_1:86;
A191: (G " ) . (f /. 1) = (G " ) . (f /. 1) by A53, A54, TOPS_2:def 4
.= 0 by A51, A53, A190, FUNCT_1:54 ;
then A192: ((G " ) * FF) . 0 = 0 by A185, A187, FUNCT_1:23;
A193: 1 in dom G by A55, BORSUK_1:86;
A194: (G " ) . (f /. ((n + 2) + 1)) = (G " ) . (f /. ((n + 2) + 1)) by A53, A54, TOPS_2:def 4
.= 1 by A52, A53, A193, FUNCT_1:54 ;
then A195: ((G " ) * FF) . 1 = 1 by A186, A189, FUNCT_1:23;
reconsider ppp = 1 / 2 as Point of I[01] by BORSUK_1:86;
TopSpaceMetr RealSpace is T_2 by PCOMPS_1:38;
then A196: I[01] is T_2 by TOPMETR:3, TOPMETR:27, TOPMETR:def 7;
A197: T1 is compact by HEINE:11;
A198: T2 is compact by HEINE:11;
A199: F1 is continuous by A88, TOPS_2:def 5;
A200: F19 is continuous by A92, TOPS_2:def 5;
A201: (TOP-REAL 2) | NE is SubSpace of (TOP-REAL 2) | NE1 by A38, A94, TOPMETR:5;
A202: (TOP-REAL 2) | (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1))) is SubSpace of (TOP-REAL 2) | NE1 by A94, TOPMETR:5;
A203: g11 is continuous by A199, A201, PRE_TOPC:56;
A204: g22 is continuous by A200, A202, PRE_TOPC:56;
A205: [#] T1 = [.0 ,(1 / 2).] by TOPMETR:25;
A206: [#] T2 = [.(1 / 2),1.] by TOPMETR:25;
then A207: ([#] T1) \/ ([#] T2) = [#] I[01] by A205, BORSUK_1:83, XXREAL_1:174;
([#] T1) /\ ([#] T2) = {ppp} by A205, A206, XXREAL_1:418;
then reconsider FF = FF as continuous Function of I[01] ,((TOP-REAL 2) | NE1) by A108, A109, A196, A197, A198, A203, A204, A207, COMPTS_1:29;
A208: F1 is one-to-one by A88, TOPS_2:def 5;
A209: 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:
assume that
A210: x1 in dom F19 and
A211: x2 in (dom F1) \ (dom F19) ; :: thesis:
assume A212: F19 . x1 = F1 . x2 ; :: thesis:
A213: F19 . x1 in LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) by A93, A210, FUNCT_2:6;
A214: x2 in dom F1 by A211, XBOOLE_0:def 5;
A215: not x2 in dom F19 by A211, XBOOLE_0:def 5;
F1 . x2 in NE by A38, A89, A211, FUNCT_2:6;
then F1 . x2 in NE /\ (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1))) by A212, A213, XBOOLE_0:def 4;
then F1 . x2 = f /. (n + 2) by A38, A112;
hence contradiction by A100, A101, A108, A208, A214, A215, FUNCT_1:def 8; :: thesis:

end;

then A216: FF is one-to-one by A208, A209, TOPMETR2:2;
A217: G " is being_homeomorphism by A50, TOPS_2:70;
FF is being_homeomorphism by A103, A104, A105, A160, A216, COMPTS_1:26;
then A218: (G " ) * FF is being_homeomorphism by A217, TOPS_2:71;
then A219: (G " ) * FF is continuous by TOPS_2:def 5;
A220: dom ((G " ) * FF) = [#] I[01] by A218, TOPS_2:def 5;
A221: rng ((G " ) * FF) = [#] I[01] by A218, TOPS_2:def 5;
A222: (G " ) * FF is one-to-one by A218, TOPS_2:def 5;
then A223: dom (((G " ) * FF) " ) = [#] I[01] by A221, TOPS_2:62;
A224: rng G = [#] ((TOP-REAL 2) | H₁(n + 1)) by A50, TOPS_2:def 5
.= rng FF by A67, A68, A95, A159, TOPREAL3:45 ;
A225: G * ((G " ) * FF) = FF * (G * (G " )) by RELAT_1:55
.= (id (rng G)) * FF by A53, A54, TOPS_2:65
.= FF by A224, RELAT_1:80 ;
A226: 1 / 2 in dom ((G " ) * FF) by A220, BORSUK_1:86;
then A227: ((G " ) * FF) . (1 / 2) in rng ((G " ) * FF) by FUNCT_1:def 5;
A228: ((G " ) * FF) . (1 / 2) = (G " ) . (FF . (1 / 2)) by A226, FUNCT_1:22
.= pp by A101, A109, FUNCT_4:14 ;
A229: [.pp,1.] c= ((G " ) * FF) .: [.(1 / 2),1.]

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in [.pp,1.] ; :: thesis:
then a in { l where l is Real : ( pp <= l & l <= 1 ) } by RCOMP_1:def 1;
then consider l1 being Real such that
A230: l1 = a and
A231: pp <= l1 and
A232: l1 <= 1 ;
A233: 0 <= pp by A227, A228, BORSUK_1:86;
set cos = (((G " ) * FF) " ) . l1;
l1 in dom (((G " ) * FF) " ) by A223, A231, A232, A233, BORSUK_1:86;
then A234: (((G " ) * FF) " ) . l1 in rng (((G " ) * FF) " ) by FUNCT_1:def 5;
then A235: (((G " ) * FF) " ) . l1 in [.0 ,1.] by BORSUK_1:83;
A236: l1 in rng ((G " ) * FF) by A221, A231, A232, A233, BORSUK_1:86;
A237: ((G " ) * FF) . ((((G " ) * FF) " ) . l1) = ((G " ) * FF) . ((((G " ) * FF) " ) . l1) by A221, A222, TOPS_2:def 4
.= l1 by A222, A236, FUNCT_1:57 ;
reconsider cos = (((G " ) * FF) " ) . l1 as Real by A235;
reconsider A3 = cos, A4 = 1, A5 = 1 / 2 as Point of I[01] by A234, BORSUK_1:86;
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 by Lm2;
A238: cos <= 1

proof

assume cos > 1 ; :: thesis:
then Fhc > Fh0 by A192, A195, A219, A222, JORDAN5A:17;
hence contradiction by A102, A189, A194, A232, A237, BORSUK_1:83, FUNCT_1:23; :: thesis:

end;

cos >= 1 / 2

proof

assume cos < 1 / 2 ; :: thesis:
then Fhc < Fh12 by A192, A195, A219, A222, JORDAN5A:17;
hence contradiction by A102, A173, A231, A237, BORSUK_1:83, FUNCT_1:23; :: thesis:

end;

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 A220, A230, A234, A237, FUNCT_1:def 12; :: thesis:

end;

((G " ) * FF) .: [.(1 / 2),1.] c= [.pp,1.]

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in ((G " ) * FF) .: [.(1 / 2),1.] ; :: thesis:
then consider x being set such that
x in dom ((G " ) * FF) and
A239: x in [.(1 / 2),1.] and
A240: a = ((G " ) * FF) . x by FUNCT_1:def 12;
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:86;
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 by Lm2;
A244: A4 >= A5

proof

per cases ;

suppose 1 <> l1 ; :: thesis:

then 1 > l1 by A243, XXREAL_0:1;
hence A4 >= A5 by A192, A195, A219, A222, BORSUK_1:def 18, JORDAN5A:17; :: thesis:

end;

suppose 1 = l1 ; :: thesis:

hence A4 >= A5 by BORSUK_1:def 18; :: thesis:

end;

A5 >= A6

proof

per cases ;

suppose l1 <> 1 / 2 ; :: thesis:

then l1 > 1 / 2 by A242, XXREAL_0:1;
hence A5 >= A6 by A192, A195, A219, A222, JORDAN5A:17; :: thesis:

end;

suppose l1 = 1 / 2 ; :: thesis:

hence A5 >= A6 ; :: thesis:

end;

then A5 in { l where l is Real : ( pp <= l & l <= 1 ) } by A195, A228, A244, BORSUK_1:def 18;
hence a in [.pp,1.] by A240, A241, RCOMP_1:def 1; :: thesis:

end;

then [.pp,1.] = ((G " ) * FF) .: [.(1 / 2),1.] by A229, XBOOLE_0:def 10;
then A245: G .: [.pp,1.] = LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) by A172, A184, A225, RELAT_1:159;
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 ;

suppose j + 1 <= n + 2 ; :: thesis:

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 (#) )) " ) . r1 = ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r1 by A253, TOPS_2:def 4;
A257: ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r2 = ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r2 by A253, A255, TOPS_2:def 4;
A258: rng (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) = [#] I[01] by A82, TOPMETR:27, TOPS_2:def 5
.= the carrier of I[01] ;
then A259: r1 in rng (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) by A247, A248, BORSUK_1:86;
A260: r2 in rng (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) by A246, A247, A249, A258, BORSUK_1:86;
A261: ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r1 in the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) by A253, A254, A256, A259, FUNCT_1:54;
A262: ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r2 in the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) by A253, A254, A257, A260, FUNCT_1:54;
A263: ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r1 in [.0 ,(1 / 2).] by A261, TOPMETR:25;
A264: ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r2 in [.0 ,(1 / 2).] by A262, TOPMETR:25;
then 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 by A263;
reconsider r19 = r1, r29 = r2 as Point of (Closed-Interval-TSpace 0 ,1) by A246, A247, A248, A249, BORSUK_1:86, TOPMETR:27;
A265: (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " is being_homeomorphism by A82, TOPS_2:70;
A266: f1 = ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r19 ;
A267: f2 = ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r29 ;
A268: ( (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 A265, TOPS_2:def 5;
then A269: f1 < f2 by A168, A170, A246, A266, A267, JORDAN5A:16;
A270: [.0 ,(1 / 2).] c= [.0 ,1.] by XXREAL_1:34;
A271: r1 = (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) . f1 by A253, A256, A259, FUNCT_1:54;
A272: r2 = (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) . f2 by A253, A257, A260, FUNCT_1:54;
A273: f1 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) } by A263, RCOMP_1:def 1;
A274: f2 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) } by A264, RCOMP_1:def 1;
A275: ex ff1 being Real st
( ff1 = f1 & 0 <= ff1 & ff1 <= 1 / 2 ) by A273;
ex ff2 being Real st
( ff2 = f2 & 0 <= ff2 & ff2 <= 1 / 2 ) by A274;
then A276: (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) .: [.f1,f2.] = [.r1,r2.] by A82, A106, A167, A269, A271, A272, A275, JORDAN5A:21;
A277: F1 .: [.f1,f2.] c= FF .: [.f1,f2.]

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in F1 .: [.f1,f2.] ; :: thesis:
then consider x being set such that
A278: x in dom F1 and
A279: x in [.f1,f2.] and
A280: a = F1 . x by FUNCT_1:def 12;

A281: now

per cases ;

suppose x <> 1 / 2 ; :: thesis:

hence FF . x = F1 . x by A10, A174, A278, FUNCT_4:12; :: thesis:

end;

suppose x = 1 / 2 ; :: thesis:

hence FF . x = F1 . x by A101, A108, A109, FUNCT_4:14; :: thesis:

end;

x in dom FF by A278, FUNCT_4:13;
hence a in FF .: [.f1,f2.] by A279, A280, A281, FUNCT_1:def 12; :: thesis:

end;

FF .: [.f1,f2.] c= F1 .: [.f1,f2.]

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in FF .: [.f1,f2.] ; :: thesis:
then consider x being set such that
x in dom FF and
A282: x in [.f1,f2.] and
A283: a = FF . x by FUNCT_1:def 12;
A284: [.f1,f2.] c= [.0 ,(1 / 2).] by A263, A264, XXREAL_2:def 12;

now

per cases ;

suppose x <> 1 / 2 ; :: thesis:

hence FF . x = F1 . x by A174, A282, A284, FUNCT_4:12; :: thesis:

end;

suppose x = 1 / 2 ; :: thesis:

hence FF . x = F1 . x by A101, A108, A109, FUNCT_4:14; :: thesis:

end;

hence a in F1 .: [.f1,f2.] by A96, A282, A283, A284, FUNCT_1:def 12; :: thesis:

end;

then F1 .: [.f1,f2.] = FF .: [.f1,f2.] by A277, XBOOLE_0:def 10;
then A285: F .: [.r1,r2.] = FF .: [.f1,f2.] by A276, RELAT_1:159;
set e1 = ((G " ) * FF) . f1;
set e2 = ((G " ) * FF) . f2;
A286: ((G " ) * FF) . f1 in the carrier of I[01] by A263, A270, BORSUK_1:83, FUNCT_2:7;
A287: ((G " ) * FF) . f2 in the carrier of I[01] by A264, A270, BORSUK_1:83, FUNCT_2:7;
A288: ((G " ) * FF) . f1 in { l where l is Real : ( 0 <= l & l <= 1 ) } by A286, BORSUK_1:83, RCOMP_1:def 1;
A289: ((G " ) * FF) . f2 in { l where l is Real : ( 0 <= l & l <= 1 ) } by A287, BORSUK_1:83, RCOMP_1:def 1;
consider l1 being Real such that
A290: l1 = ((G " ) * FF) . f1 and
A291: 0 <= l1 and
A292: l1 <= 1 by A288;
consider l2 being Real such that
A293: l2 = ((G " ) * FF) . f2 and
0 <= l2 and
A294: l2 <= 1 by A289;
reconsider f19 = f1, f29 = f2 as Point of I[01] by A263, A264, A270, BORSUK_1:83;
A295: ((G " ) * FF) . 0 = 0 by A185, A187, A191, FUNCT_1:23;
A296: ((G " ) * FF) . 1 = 1 by A186, A189, A194, FUNCT_1:23;
A297: l1 = ((G " ) * FF) . f19 by A290;
l2 = ((G " ) * FF) . f29 by A293;
then A298: l1 < l2 by A219, A222, A269, A295, A296, A297, JORDAN5A:17;
A299: f1 < f2 by A168, A170, A246, A266, A267, A268, JORDAN5A:16;
A300: 0 <= f1 by A263, A270, BORSUK_1:83, BORSUK_1:86;
f2 <= 1 by A264, A270, BORSUK_1:83, BORSUK_1:86;
then A301: G .: [.l1,l2.] = G .: (((G " ) * FF) .: [.f1,f2.]) by A192, A195, A218, A290, A293, A299, A300, JORDAN5A:21, TOPMETR:27
.= FF .: [.f1,f2.] by A225, RELAT_1:159 ;
A302: FF . f19 = F . r19

proof

per cases ;

suppose A303: f19 = 1 / 2 ; :: thesis:

then FF . f19 = F19 . (1 / 2) by A101, FUNCT_4:14
.= F9 . 0 by A101, A169, FUNCT_1:22
.= F . r19 by A77, A80, A106, A253, A255, A256, A303, FUNCT_1:54 ;
hence FF . f19 = F . r19 ; :: thesis:

end;

suppose f19 <> 1 / 2 ; :: thesis:

then FF . f19 = F1 . f19 by A174, A263, FUNCT_4:12
.= F . ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) . f19) by A85, A263, FUNCT_1:23
.= F . r19 by A253, A255, A256, FUNCT_1:54 ;
hence FF . f19 = F . r19 ; :: thesis:

end;

A304: FF . f29 = F . r29

proof

per cases ;

suppose A305: f29 = 1 / 2 ; :: thesis:

then FF . f29 = F19 . (1 / 2) by A101, FUNCT_4:14
.= F9 . 0 by A101, A169, FUNCT_1:22
.= F . r29 by A77, A80, A106, A253, A255, A257, A305, FUNCT_1:54 ;
hence FF . f29 = F . r29 ; :: thesis:

end;

suppose f29 <> 1 / 2 ; :: thesis:

then FF . f29 = F1 . f29 by A174, A264, FUNCT_4:12
.= F . ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) . f29) by A85, A264, FUNCT_1:23
.= F . r29 by A253, A255, A257, FUNCT_1:54 ;
hence FF . f29 = F . r29 ; :: thesis:

end;

A306: G . l1 = f /. j by A102, A225, A251, A290, A302, BORSUK_1:83, FUNCT_1:22;
G . l2 = f /. (j + 1) by A102, A225, A252, A293, A304, BORSUK_1:83, FUNCT_1:22;
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, A285, A291, A292, A294, A298, A301, A306; :: thesis:

end;

suppose j + 1 > n + 2 ; :: thesis:

then A307: 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 5;
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, A307; :: thesis:

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:

end;

A308: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A14, A33);
1 <= h1 + 2 by A12, XXREAL_0:2;
then ex NE being non empty Subset of (TOP-REAL 2) st
( NE = H₁(h1) & ( for j being Element of 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 A308;
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: