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 A1: ( 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) ) ; :: thesis:
then A2: f is one-to-one by TOPREAL1:def 10;
A3: ( the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) = [.0 ,(1 / 2).] & the carrier of (Closed-Interval-TSpace (1 / 2),1) = [.(1 / 2),1.] ) by TOPMETR:25;
A4: ( [#] (Closed-Interval-TSpace 0 ,(1 / 2)) = [.0 ,(1 / 2).] & [#] (Closed-Interval-TSpace (1 / 2),1) = [.(1 / 2),1.] ) by TOPMETR:25;
A5: len f >= 2 by A1, 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 A5, INT_1:18;
A6: 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 ;
A7: S₁[ 0 ]

proof

assume A8: ( 1 <= 0 + 2 & 0 + 2 <= len f ) ; :: thesis:
then A9: ( 1 <= len (f | 2) & 2 <= len (f | 2) ) by 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 A10: ( 1 <= j & j + 1 <= 0 + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (0 + 2) ) ; :: thesis:
then j <= (1 + 1) - 1 by XREAL_1:21;
then A11: j = 1 by A10, XXREAL_0:1;
A12: len (f | 2) = 2 by A8, FINSEQ_1:80;
A13: ( 1 in dom (f | 2) & 2 in dom (f | 2) ) by A9, FINSEQ_3:27;
then A14: ( (f | 2) /. 1 = (f | 2) . 1 & (f | 2) /. 2 = (f | 2) . 2 ) by PARTFUN1:def 8;
A15: (f | 2) /. 1 = f /. 1 by A13, FINSEQ_4:85;
A16: 1 + 1 <= len f by A8;
A17: rng F = [#] ((TOP-REAL 2) | NE) by A10, TOPS_2:def 5
.= L~ (f | 2) by PRE_TOPC:def 10
.= L~ <*((f | 2) /. 1),((f | 2) /. 2)*> by A12, A14, FINSEQ_1:61
.= LSeg ((f | 2) /. 1),((f | 2) /. 2) by SPPOL_2:21
.= LSeg (f /. 1),(f /. 2) by A13, A15, FINSEQ_4:85
.= LSeg f,1 by A16, 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 A10, A11, A17, BORSUK_1:83, FUNCT_2:45; :: thesis:

end;

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

proof

let n be Element of NAT ; :: thesis:
assume A19: S₁[n] ; :: thesis:
assume A20: ( 1 <= (n + 1) + 2 & (n + 1) + 2 <= len f ) ; :: thesis:
A21: 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
A22: ( NE = H₁(n) & ( 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 A19, A20, A21, XXREAL_0:2;
A23: len (f | ((n + 1) + 2)) = (n + 1) + 2 by A20, FINSEQ_1:80;
A24: (n + 1) + 2 = (n + 2) + 1 ;
A25: ( 1 <= (n + 1) + 1 & (n + 1) + 1 <= (n + 2) + 1 & (n + 2) + 1 <= len f ) by A20, NAT_1:11;
then A26: ( 1 <= (n + 1) + 1 & (n + 1) + 1 <= len f ) by XXREAL_0:2;
A27: ( 1 <= n + 2 & n + 2 <= len f ) by A25, XXREAL_0:2;
A28: n + 2 in dom (f | (n + 3)) by A23, A25, FINSEQ_3:27;
then A29: 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 A23, 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 A30: ( 1 <= j & j + 1 <= (n + 1) + 2 & G is being_homeomorphism & G . 0 = f /. 1 & G . 1 = f /. ((n + 1) + 2) ) ; :: thesis:
then A31: ( G is one-to-one & rng G = [#] ((TOP-REAL 2) | H₁(n + 1)) & dom G = [#] I[01] ) by TOPS_2:def 5;
then A32: rng G = L~ (f | (n + 3)) by PRE_TOPC:def 10;
set pp = (G " ) . (f /. (n + 2));
A33: (G " ) . (f /. (n + 2)) = (G " ) . (f /. (n + 2)) by A31, TOPS_2:def 4;
( n + 2 <= len (f | (n + 2)) & 1 <= len (f | (n + 2)) ) by A25, FINSEQ_1:80, XXREAL_0:2;
then A34: ( n + 2 in dom (f | (n + 2)) & 1 in dom (f | (n + 2)) ) by A25, FINSEQ_3:27;
A35: f /. (n + 2) in rng G by A23, A28, A29, A32, GOBOARD1:16, NAT_1:11;
then A36: ( (G " ) . (f /. (n + 2)) in dom G & f /. (n + 2) = G . ((G " ) . (f /. (n + 2))) ) by A31, A33, FUNCT_1:54;
then reconsider pp = (G " ) . (f /. (n + 2)) as Real by A31, BORSUK_1:83;
A37: (n + 1) + 1 <> (n + 2) + 1 ;
A38: n + 2 <> n + 3 ;
A39: ( n + 2 in dom f & n + 3 in dom f ) by A20, A27, FINSEQ_3:27;
A40: 1 <> pp

proof

assume pp = 1 ; :: thesis:
then f /. (n + 2) = f /. ((n + 1) + 2) by A30, A31, A33, A35, FUNCT_1:54;
hence contradiction by A2, A38, A39, PARTFUN2:17; :: thesis:

end;

A41: ( 0 <= pp & pp <= 1 ) by A36, BORSUK_1:86;
then A42: pp < 1 by A40, XXREAL_0:1;
set pn = f /. (n + 2);
set pn1 = f /. ((n + 2) + 1);
2 <= n + 2 by NAT_1:11;
then A43: ( f /. (n + 2) = (f | (n + 2)) /. (n + 2) & (f | (n + 2)) /. 1 = f /. 1 & len (f | (n + 2)) = n + 2 & f | (n + 2) is being_S-Seq ) by A1, A27, A34, FINSEQ_1:80, FINSEQ_4:85, JORDAN3:37;
then NE is_an_arc_of (f | (n + 2)) /. 1,f /. (n + 2) by A22, TOPREAL1:31;
then consider F being Function of I[01] ,((TOP-REAL 2) | NE) such that
A44: ( F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (n + 2) ) by A43, TOPREAL1:def 2;
( (n + 1) + 1 in dom f & (n + 2) + 1 in dom f ) by A20, A26, FINSEQ_3:27;
then LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) is_an_arc_of f /. (n + 2),f /. ((n + 2) + 1) by A2, A37, PARTFUN2:17, TOPREAL1:15;
then consider F' being Function of I[01] ,((TOP-REAL 2) | (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)))) such that
A45: ( F' is being_homeomorphism & F' . 0 = f /. (n + 2) & F' . 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 F1' = F' * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ));
A46: ( P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ) is being_homeomorphism & P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ) is being_homeomorphism ) by TREAL_1:20;
then A47: dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) = [#] (Closed-Interval-TSpace 0 ,(1 / 2)) by TOPS_2:def 5;
then A48: dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) = [.0 ,(1 / 2).] by TOPMETR:25;
dom F = [#] I[01] by A44, TOPS_2:def 5;
then A49: rng (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) = dom F by A46, 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 A50: rng (F * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) = [#] ((TOP-REAL 2) | NE) by A44, TOPS_2:def 5;
then A51: rng (F * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) = H₁(n) by A22, PRE_TOPC:def 10;
( dom (F * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) = the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) & rng (F * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) = the carrier of ((TOP-REAL 2) | NE) ) by A47, A49, A50, 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;
A52: F1 is being_homeomorphism by A44, A46, TOPMETR:27, TOPS_2:71;
then A53: rng F1 = [#] ((TOP-REAL 2) | NE) by TOPS_2:def 5
.= H₁(n) by A22, PRE_TOPC:def 10 ;
A54: dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) = [#] (Closed-Interval-TSpace (1 / 2),1) by A46, TOPS_2:def 5;
dom F' = [#] I[01] by A45, TOPS_2:def 5;
then A55: rng (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) = dom F' by A46, TOPMETR:27, TOPS_2:def 5;
then rng (F' * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) = rng F' by RELAT_1:47;
then rng (F' * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) = [#] ((TOP-REAL 2) | (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)))) by A45, TOPS_2:def 5;
then ( dom (F' * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) = the carrier of (Closed-Interval-TSpace (1 / 2),1) & rng (F' * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) = the carrier of ((TOP-REAL 2) | (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)))) ) by A54, A55, RELAT_1:46;
then reconsider F1' = F' * (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;
A56: F1' is being_homeomorphism by A45, A46, TOPMETR:27, TOPS_2:71;
then A57: rng F1' = [#] ((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 +* F1';
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;
A58: H₁(n + 1) = H₁(n) \/ (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1))) by A39, TOPREAL3:45;
A59: the carrier of ((TOP-REAL 2) | H₁(n + 1)) = [#] ((TOP-REAL 2) | H₁(n + 1))
.= H₁(n + 1) by PRE_TOPC:def 10 ;
then ( dom F1 = the carrier of T1 & rng F1 c= the carrier of ((TOP-REAL 2) | NE1) ) by A47, A49, A51, A58, RELAT_1:46, XBOOLE_1:7;
then reconsider g11 = F1 as Function of T1,((TOP-REAL 2) | NE1) by RELSET_1:11;
( dom F1' = the carrier of T2 & rng F1' c= the carrier of ((TOP-REAL 2) | NE1) ) by A54, A55, A57, A58, A59, RELAT_1:46, XBOOLE_1:7;
then reconsider g22 = F1' as Function of T2,((TOP-REAL 2) | NE1) by RELSET_1:11;
A60: ( [.0 ,(1 / 2).] = dom F1 & [.(1 / 2),1.] = dom F1' ) by A4, A52, A56, TOPS_2:def 5;
( 1 / 2 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) } & 1 / 2 in { l where l is Real : ( 1 / 2 <= l & l <= 1 ) } ) ;
then A61: ( 1 / 2 in dom F1 & 1 / 2 in dom F1' ) by A60, RCOMP_1:def 1;
A62: dom (F1 +* F1') = [.0 ,(1 / 2).] \/ [.(1 / 2),1.] by A60, FUNCT_4:def 1
.= [.0 ,1.] by XXREAL_1:174 ;
A63: I[01] is compact by HEINE:11, TOPMETR:27;
A64: (TOP-REAL 2) | NE1 is T_2 by TOPMETR:3;
A65: dom (F1 +* F1') = [#] I[01] by A62, BORSUK_1:83;
A66: (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 ;
A67: (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 ;
A68: F1 . (1 / 2) = f /. (n + 2) by A44, A61, A66, FUNCT_1:22;
A69: F1' . (1 / 2) = f /. (n + 2) by A45, A61, A67, FUNCT_1:22;
A70: [.0 ,(1 / 2).] /\ [.(1 / 2),1.] = [.(1 / 2),(1 / 2).] by XXREAL_1:143;
then A71: (dom F1) /\ (dom F1') = {(1 / 2)} by A60, XXREAL_1:17;
A72: 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 x in H₁(n) /\ (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1))) ; :: thesis:
then A73: ( x in LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) & x in H₁(n) ) by 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
A74: x in X and
A75: 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
A76: X = LSeg (f | (n + 2)),k and
A77: ( 1 <= k & k + 1 <= len (f | (n + 2)) ) by A75;
A78: len (f | (n + 2)) = n + (1 + 1) by A25, FINSEQ_1:80, XXREAL_0:2;
A79: len (f | (n + 2)) = (n + 1) + 1 by A25, FINSEQ_1:80, XXREAL_0:2;
then A80: k <= n + 1 by A77, XREAL_1:8;
A81: f is s.n.c. by A1, TOPREAL1:def 10;
A82: f is unfolded by A1, TOPREAL1:def 10;

now

assume A83: k < n + 1 ; :: thesis:
A84: ( 1 <= 1 + k & k + 1 <= n + (1 + 1) ) by A26, A77, FINSEQ_1:80, NAT_1:11;
A85: k + 1 <= len f by A26, A77, A79, XXREAL_0:2;
A86: k + 1 < (n + 1) + 1 by A83, XREAL_1:8;
set p1' = f /. k;
set p2' = f /. (k + 1);
( n + 1 <= (n + 1) + 1 & (n + 1) + 1 = n + (1 + 1) ) by NAT_1:11;
then k <= n + 2 by A83, XXREAL_0:2;
then ( k in Seg (len (f | (n + 2))) & k + 1 in Seg (len (f | (n + 2))) ) by A77, A78, A84, FINSEQ_1:3;
then A87: ( k in dom (f | (n + 2)) & k + 1 in dom (f | (n + 2)) ) by FINSEQ_1:def 3;
then A88: (f | (n + 2)) /. k = f /. k by FINSEQ_4:85;
A89: (f | (n + 2)) /. (k + 1) = f /. (k + 1) by A87, FINSEQ_4:85;
A90: LSeg f,k = LSeg (f /. k),(f /. (k + 1)) by A77, A85, TOPREAL1:def 5
.= LSeg (f | (n + 2)),k by A77, A88, A89, TOPREAL1:def 5 ;
LSeg f,(n + 2) = LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) by A25, TOPREAL1:def 5;
then LSeg (f | (n + 2)),k misses LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) by A81, A86, A90, 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 A73, A74, A76, XBOOLE_0:def 4; :: thesis:

end;

then A91: k = n + 1 by A80, XXREAL_0:1;
A92: ( 1 <= n + 1 & 1 <= (n + 1) + 1 & (n + 1) + 1 <= len f ) by A25, A77, A80, XXREAL_0:2;
set p1' = f /. (n + 1);
set p2' = f /. ((n + 1) + 1);
A93: ( n + 1 <= (n + 1) + 1 & (n + 1) + 1 = n + (1 + 1) & 1 <= 1 + n & 1 <= 1 + (n + 1) ) by NAT_1:11;
then ( n + 1 in Seg (len (f | (n + 2))) & (n + 1) + 1 in Seg (len (f | (n + 2))) ) by A78, FINSEQ_1:3;
then A94: ( n + 1 in dom (f | (n + 2)) & (n + 1) + 1 in dom (f | (n + 2)) ) by FINSEQ_1:def 3;
then A95: (f | (n + 2)) /. (n + 1) = f /. (n + 1) by FINSEQ_4:85;
A96: (f | (n + 2)) /. ((n + 1) + 1) = f /. ((n + 1) + 1) by A94, FINSEQ_4:85;
A97: LSeg f,(n + 1) = LSeg (f /. (n + 1)),(f /. ((n + 1) + 1)) by A92, TOPREAL1:def 5
.= LSeg (f | (n + 2)),(n + 1) by A78, A93, A95, A96, TOPREAL1:def 5 ;
LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) = LSeg f,((n + 1) + 1) by A25, TOPREAL1:def 5;
then A98: x in (LSeg f,(n + 1)) /\ (LSeg f,((n + 1) + 1)) by A73, A74, A76, A91, A97, 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 A20, A82, TOPREAL1:def 8;
hence x = f /. (n + 2) by A98, TARSKI:def 1; :: thesis:

end;

assume A99: x = f /. (n + 2) ; :: thesis:
then A100: x in LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) by RLTOPSP1:69;
A101: len (f | (n + 2)) = n + 2 by A25, FINSEQ_1:80, XXREAL_0:2;
then ( dom (f | (n + 2)) = Seg (n + 2) & n + 2 in Seg (n + 2) ) by A25, FINSEQ_1:3, FINSEQ_1:def 3;
then A102: x = (f | (n + 2)) /. ((n + 1) + 1) by A99, FINSEQ_4:85;
1 <= n + 1 by NAT_1:11;
then A103: x in LSeg (f | (n + 2)),(n + 1) by A101, A102, TOPREAL1:27;
( 1 <= 1 + n & (n + 1) + 1 <= n + (1 + 1) & n + 2 <= len f ) by A25, NAT_1:11, XXREAL_0:2;
then ( 1 <= n + 1 & (n + 1) + 1 <= len (f | (n + 2)) ) by FINSEQ_1:80;
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)) ) } ;
then x in union { (LSeg (f | (n + 2)),k) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | (n + 2)) ) } by A103, 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 A100, XBOOLE_0:def 4; :: thesis:

end;

f /. (n + 2) in rng F1' by A61, A69, FUNCT_1:def 5;
then A104: {(f /. (n + 2))} c= rng F1' by ZFMISC_1:37;
A105: F1 .: ((dom F1) /\ (dom F1')) = Im F1,(1 / 2) by A60, A70, XXREAL_1:17
.= {(f /. (n + 2))} by A61, A68, FUNCT_1:117 ;
then A106: rng (F1 +* F1') = H₁(n) \/ (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1))) by A53, A57, A104, TOPMETR2:3;
then A107: rng (F1 +* F1') = [#] ((TOP-REAL 2) | H₁(n + 1)) by A39, A59, TOPREAL3:45;
( dom (F1 +* F1') = the carrier of I[01] & rng (F1 +* F1') c= the carrier of ((TOP-REAL 2) | H₁(n + 1)) ) by A53, A57, A58, A59, A62, A104, A105, BORSUK_1:83, TOPMETR2:3;
then reconsider FF = F1 +* F1' as Function of I[01] ,((TOP-REAL 2) | NE1) by FUNCT_2:4;
A108: rng (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) = [#] (Closed-Interval-TSpace 0 ,1) by A46, TOPS_2:def 5;
( 0 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) } & 1 / 2 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) } ) ;
then A109: ( 0 in dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) & 1 / 2 in dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) & 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 A46, A48, RCOMP_1:def 1, TOPS_2:def 5;
A110: (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 ;
A111: ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . 0 = ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . 0 by A108, A109, TOPS_2:def 4
.= 0 by A109, A110, FUNCT_1:54 ;
A112: (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 ;
A113: ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . 1 = ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . 1 by A108, A109, TOPS_2:def 4
.= 1 / 2 by A66, A109, FUNCT_1:54 ;
A114: (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 ;
A115: LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) = F1' .: [.(1 / 2),1.] by A3, A57, FUNCT_2:45;
A116: FF . (1 / 2) = f /. (n + 2) by A61, A69, FUNCT_4:14;
A117: for x being set st x in [.0 ,(1 / 2).] & x <> 1 / 2 holds
not x in dom F1'

proof

let x be set ; :: thesis:
assume A118: ( x in [.0 ,(1 / 2).] & x <> 1 / 2 ) ; :: thesis:
assume x in dom F1' ; :: thesis:
then x in (dom F1) /\ (dom F1') by A60, A118, XBOOLE_0:def 4;
hence contradiction by A71, A118, TARSKI:def 1; :: thesis:

end;

A119: FF .: [.(1 / 2),1.] = F1' .: [.(1 / 2),1.]

proof

thus FF .: [.(1 / 2),1.] c= F1' .: [.(1 / 2),1.] :: according to XBOOLE_0:def 10 :: thesis:

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
A120: ( x in dom FF & x in [.(1 / 2),1.] & a = FF . x ) by FUNCT_1:def 12;
FF . x = F1' . x by A60, A120, FUNCT_4:14;
hence a in F1' .: [.(1 / 2),1.] by A60, A120, FUNCT_1:def 12; :: thesis:

end;

thus F1' .: [.(1 / 2),1.] c= FF .: [.(1 / 2),1.] :: thesis:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in F1' .: [.(1 / 2),1.] ; :: thesis:
then consider x being set such that
A121: ( x in dom F1' & x in [.(1 / 2),1.] & a = F1' . x ) by FUNCT_1:def 12;
A122: x in dom FF by A121, FUNCT_4:13;
a = FF . x by A121, FUNCT_4:14;
hence a in FF .: [.(1 / 2),1.] by A121, A122, FUNCT_1:def 12; :: thesis:

end;

set GF = (G " ) * FF;
A123: ( 0 in dom FF & 1 in dom FF ) by A62, 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 A124: FF . 0 = F1 . 0 by A117, FUNCT_4:12
.= f /. 1 by A44, A109, A110, FUNCT_1:23 ;
1 in { l where l is Real : ( 1 / 2 <= l & l <= 1 ) } ;
then A125: 1 in dom F1' by A60, RCOMP_1:def 1;
then A126: FF . 1 = F1' . 1 by FUNCT_4:14
.= f /. ((n + 2) + 1) by A45, A114, A125, FUNCT_1:22 ;
A127: ( 0 in dom G & f /. 1 = G . 0 ) by A30, A31, BORSUK_1:86;
A128: (G " ) . (f /. 1) = (G " ) . (f /. 1) by A31, TOPS_2:def 4
.= 0 by A31, A127, FUNCT_1:54 ;
then A129: ((G " ) * FF) . 0 = 0 by A123, A124, FUNCT_1:23;
A130: ( 1 in dom G & f /. ((n + 2) + 1) = G . 1 ) by A30, A31, BORSUK_1:86;
A131: (G " ) . (f /. ((n + 2) + 1)) = (G " ) . (f /. ((n + 2) + 1)) by A31, TOPS_2:def 4
.= 1 by A31, A130, FUNCT_1:54 ;
then A132: ((G " ) * FF) . 1 = 1 by A123, A126, 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 A133: I[01] is T_2 by TOPMETR:3, TOPMETR:27, TOPMETR:def 7;
A134: ( T1 is compact & T2 is compact ) by HEINE:11;
( F1 is continuous & F1' is continuous & (TOP-REAL 2) | NE is SubSpace of (TOP-REAL 2) | NE1 & (TOP-REAL 2) | (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1))) is SubSpace of (TOP-REAL 2) | NE1 ) by A22, A52, A56, A58, TOPMETR:5, TOPS_2:def 5;
then A135: ( g11 is continuous & g22 is continuous ) by PRE_TOPC:56;
A136: [#] T1 = [.0 ,(1 / 2).] by TOPMETR:25;
A137: [#] T2 = [.(1 / 2),1.] by TOPMETR:25;
then A138: ([#] T1) \/ ([#] T2) = [#] I[01] by A136, BORSUK_1:83, XXREAL_1:174;
([#] T1) /\ ([#] T2) = {ppp} by A136, A137, XXREAL_1:418;
then reconsider FF = FF as continuous Function of I[01] ,((TOP-REAL 2) | NE1) by A68, A69, A133, A134, A135, A138, COMPTS_1:29;
A139: ( F1 is one-to-one & F1' is one-to-one ) by A52, A56, TOPS_2:def 5;
for x1, x2 being set st x1 in dom F1' & x2 in (dom F1) \ (dom F1') holds
F1' . x1 <> F1 . x2

proof

let x1, x2 be set ; :: thesis:
assume A140: ( x1 in dom F1' & x2 in (dom F1) \ (dom F1') ) ; :: thesis:
assume A141: F1' . x1 = F1 . x2 ; :: thesis:
A142: F1' . x1 in LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) by A57, A140, FUNCT_2:6;
A143: ( x2 in dom F1 & not x2 in dom F1' ) by A140, XBOOLE_0:def 5;
F1 . x2 in NE by A22, A53, A140, FUNCT_2:6;
then F1 . x2 in NE /\ (LSeg (f /. (n + 2)),(f /. ((n + 2) + 1))) by A141, A142, XBOOLE_0:def 4;
then F1 . x2 = f /. (n + 2) by A22, A72;
hence contradiction by A61, A68, A139, A143, FUNCT_1:def 8; :: thesis:

end;

then FF is one-to-one by A139, TOPMETR2:2;
then ( G " is being_homeomorphism & FF is being_homeomorphism ) by A30, A63, A64, A65, A107, COMPTS_1:26, TOPS_2:70;
then A144: (G " ) * FF is being_homeomorphism by TOPS_2:71;
then A145: (G " ) * FF is continuous by TOPS_2:def 5;
A146: ( dom ((G " ) * FF) = [#] I[01] & rng ((G " ) * FF) = [#] I[01] & (G " ) * FF is one-to-one ) by A144, TOPS_2:def 5;
then A147: ( dom (((G " ) * FF) " ) = [#] I[01] & rng (((G " ) * FF) " ) = [#] I[01] ) by TOPS_2:62;
A148: rng G = [#] ((TOP-REAL 2) | H₁(n + 1)) by A30, TOPS_2:def 5
.= rng FF by A39, A59, A106, TOPREAL3:45 ;
A149: G * ((G " ) * FF) = FF

proof

G * ((G " ) * FF) = FF * (G * (G " )) by RELAT_1:55
.= (id (rng G)) * FF by A31, TOPS_2:65
.= FF by A148, RELAT_1:80 ;
hence G * ((G " ) * FF) = FF ; :: thesis:

end;

A150: 1 / 2 in dom ((G " ) * FF) by A146, BORSUK_1:86;
then A151: ((G " ) * FF) . (1 / 2) in rng ((G " ) * FF) by FUNCT_1:def 5;
A152: ((G " ) * FF) . (1 / 2) = (G " ) . (FF . (1 / 2)) by A150, FUNCT_1:22
.= pp by A61, A69, FUNCT_4:14 ;
[.pp,1.] = ((G " ) * FF) .: [.(1 / 2),1.]

proof

thus [.pp,1.] c= ((G " ) * FF) .: [.(1 / 2),1.] :: according to XBOOLE_0:def 10 :: thesis:

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
A153: ( l1 = a & pp <= l1 & l1 <= 1 ) ;
A154: 0 <= pp by A151, A152, BORSUK_1:86;
set cos = (((G " ) * FF) " ) . l1;
l1 in dom (((G " ) * FF) " ) by A147, A153, A154, BORSUK_1:86;
then A155: (((G " ) * FF) " ) . l1 in rng (((G " ) * FF) " ) by FUNCT_1:def 5;
then A156: (((G " ) * FF) " ) . l1 in [.0 ,1.] by BORSUK_1:83;
A157: l1 in rng ((G " ) * FF) by A146, A153, A154, BORSUK_1:86;
A158: ((G " ) * FF) . ((((G " ) * FF) " ) . l1) = ((G " ) * FF) . ((((G " ) * FF) " ) . l1) by A146, TOPS_2:def 4
.= l1 by A146, A157, FUNCT_1:57 ;
reconsider cos = (((G " ) * FF) " ) . l1 as Real by A156;
reconsider A3 = cos, A4 = 1, A5 = 1 / 2 as Point of I[01] by A155, 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;
A159: cos <= 1

proof

assume cos > 1 ; :: thesis:
then Fhc > Fh0 by A129, A132, A145, A146, JORDAN5A:17;
hence contradiction by A62, A126, A131, A153, A158, BORSUK_1:83, FUNCT_1:23; :: thesis:

end;

cos >= 1 / 2

proof

assume cos < 1 / 2 ; :: thesis:
then Fhc < Fh12 by A129, A132, A145, A146, JORDAN5A:17;
hence contradiction by A62, A116, A153, A158, BORSUK_1:83, FUNCT_1:23; :: thesis:

end;

then cos in { l where l is Real : ( 1 / 2 <= l & l <= 1 ) } by A159;
then cos in [.(1 / 2),1.] by RCOMP_1:def 1;
hence a in ((G " ) * FF) .: [.(1 / 2),1.] by A146, A153, A155, A158, FUNCT_1:def 12; :: thesis:

end;

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

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
A160: ( x in dom ((G " ) * FF) & x in [.(1 / 2),1.] & a = ((G " ) * FF) . x ) by FUNCT_1:def 12;
x in { l where l is Real : ( 1 / 2 <= l & l <= 1 ) } by A160, RCOMP_1:def 1;
then consider l1 being Real such that
A161: ( l1 = x & 1 / 2 <= l1 & l1 <= 1 ) ;
reconsider ll = l1, pol = 1 / 2 as Point of I[01] by A161, 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;
A162: A4 >= A5

proof

per cases ;

suppose 1 <> l1 ; :: thesis:

then 1 > l1 by A161, XXREAL_0:1;
hence A4 >= A5 by A129, A132, A145, A146, 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 A161, XXREAL_0:1;
hence A5 >= A6 by A129, A132, A145, A146, 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 A132, A152, A162, BORSUK_1:def 18;
hence a in [.pp,1.] by A160, A161, RCOMP_1:def 1; :: thesis:

end;

then A163: G .: [.pp,1.] = LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) by A115, A119, A149, 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
A164: ( r1 < r2 & 0 <= r1 & r1 <= 1 & 0 <= r2 & r2 <= 1 & LSeg f,j = F .: [.r1,r2.] & F . r1 = f /. j & F . r2 = f /. (j + 1) ) by A22, A30, A44;
set f1 = ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r1;
set f2 = ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r2;
A165: ( P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ) is continuous & P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ) is one-to-one & dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) = [#] (Closed-Interval-TSpace 0 ,(1 / 2)) & rng (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) = [#] (Closed-Interval-TSpace 0 ,1) ) by A46, TOPS_2:def 5;
then A166: ( ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r1 = ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r1 & ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r2 = ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r2 ) by TOPS_2:def 4;
rng (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) = [#] I[01] by A46, TOPMETR:27, TOPS_2:def 5
.= the carrier of I[01] ;
then A167: ( r1 in rng (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) & r2 in rng (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) ) by A164, BORSUK_1:86;
then ( ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r1 in the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) & ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r2 in the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) ) by A165, A166, FUNCT_1:54;
then A168: ( ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r1 in [.0 ,(1 / 2).] & ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r2 in [.0 ,(1 / 2).] ) by 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 ;
reconsider r1' = r1, r2' = r2 as Point of (Closed-Interval-TSpace 0 ,1) by A164, BORSUK_1:86, TOPMETR:27;
(P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " is being_homeomorphism by A46, TOPS_2:70;
then A169: ( f1 = ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r1' & f2 = ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . r2' & ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . 0 = 0 & ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) " ) . 1 = 1 / 2 & (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 A111, A113, TOPS_2:def 5;
then A170: f1 < f2 by A164, JORDAN5A:16;
A171: [.0 ,(1 / 2).] c= [.0 ,1.] by XXREAL_1:34;
A172: ( r1 = (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) . f1 & r2 = (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) . f2 ) by A165, A166, A167, FUNCT_1:54;
A173: ( f1 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) } & f2 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) } ) by A168, RCOMP_1:def 1;
then consider ff1 being Real such that
A174: ( ff1 = f1 & 0 <= ff1 & ff1 <= 1 / 2 ) ;
consider ff2 being Real such that
A175: ( ff2 = f2 & 0 <= ff2 & ff2 <= 1 / 2 ) by A173;
A176: (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) .: [.f1,f2.] = [.r1,r2.] by A46, A66, A110, A170, A172, A174, A175, JORDAN5A:21;
F1 .: [.f1,f2.] = FF .: [.f1,f2.]

proof

thus F1 .: [.f1,f2.] c= FF .: [.f1,f2.] :: according to XBOOLE_0:def 10 :: thesis:

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
A177: ( x in dom F1 & x in [.f1,f2.] & a = F1 . x ) by FUNCT_1:def 12;

now

per cases ;

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

hence FF . x = F1 . x by A4, A117, A177, FUNCT_4:12; :: thesis:

end;

suppose x = 1 / 2 ; :: thesis:

hence FF . x = F1 . x by A61, A68, A69, FUNCT_4:14; :: thesis:

end;

then ( x in dom FF & x in [.f1,f2.] & a = FF . x ) by A177, FUNCT_4:13;
hence a in FF .: [.f1,f2.] by FUNCT_1:def 12; :: thesis:

end;

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

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
A178: ( x in dom FF & x in [.f1,f2.] & a = FF . x ) by FUNCT_1:def 12;
A179: [.f1,f2.] c= [.0 ,(1 / 2).] by A168, XXREAL_2:def 12;

now

per cases ;

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

hence FF . x = F1 . x by A117, A178, A179, FUNCT_4:12; :: thesis:

end;

suppose x = 1 / 2 ; :: thesis:

hence FF . x = F1 . x by A61, A68, A69, FUNCT_4:14; :: thesis:

end;

hence a in F1 .: [.f1,f2.] by A60, A178, A179, FUNCT_1:def 12; :: thesis:

end;

then A180: F .: [.r1,r2.] = FF .: [.f1,f2.] by A176, RELAT_1:159;
set e1 = ((G " ) * FF) . f1;
set e2 = ((G " ) * FF) . f2;
( ((G " ) * FF) . f1 in the carrier of I[01] & ((G " ) * FF) . f2 in the carrier of I[01] ) by A168, A171, BORSUK_1:83, FUNCT_2:7;
then A181: ( ((G " ) * FF) . f1 in { l where l is Real : ( 0 <= l & l <= 1 ) } & ((G " ) * FF) . f2 in { l where l is Real : ( 0 <= l & l <= 1 ) } ) by BORSUK_1:83, RCOMP_1:def 1;
then consider l1 being Real such that
A182: ( l1 = ((G " ) * FF) . f1 & 0 <= l1 & l1 <= 1 ) ;
consider l2 being Real such that
A183: ( l2 = ((G " ) * FF) . f2 & 0 <= l2 & l2 <= 1 ) by A181;
reconsider f1' = f1, f2' = f2 as Point of I[01] by A168, A171, BORSUK_1:83;
( ((G " ) * FF) . 0 = 0 & ((G " ) * FF) . 1 = 1 & l1 = ((G " ) * FF) . f1' & l2 = ((G " ) * FF) . f2' ) by A123, A124, A126, A128, A131, A182, A183, FUNCT_1:23;
then A184: ( l1 < l2 & 0 <= l1 & l1 <= 1 & 0 <= l2 & l2 <= 1 ) by A145, A146, A170, A182, A183, JORDAN5A:17;
A185: ( (G " ) * FF is one-to-one & (G " ) * FF is continuous & f1 < f2 & l1 = ((G " ) * FF) . f1 & l2 = ((G " ) * FF) . f2 ) by A144, A164, A169, A182, A183, JORDAN5A:16, TOPS_2:def 5;
( 0 <= f1 & f2 <= 1 ) by A168, A171, BORSUK_1:83, BORSUK_1:86;
then A186: G .: [.l1,l2.] = G .: (((G " ) * FF) .: [.f1,f2.]) by A129, A132, A144, A185, JORDAN5A:21, TOPMETR:27
.= FF .: [.f1,f2.] by A149, RELAT_1:159 ;
A187: FF . f1' = F . r1'

proof

per cases ;

suppose A188: f1' = 1 / 2 ; :: thesis:

then FF . f1' = F1' . (1 / 2) by A61, FUNCT_4:14
.= F' . 0 by A61, A112, FUNCT_1:22
.= F . r1' by A44, A45, A66, A165, A166, A188, FUNCT_1:54 ;
hence FF . f1' = F . r1' ; :: thesis:

end;

suppose f1' <> 1 / 2 ; :: thesis:

then FF . f1' = F1 . f1' by A117, A168, FUNCT_4:12
.= F . ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) . f1') by A48, A168, FUNCT_1:23
.= F . r1' by A165, A166, FUNCT_1:54 ;
hence FF . f1' = F . r1' ; :: thesis:

end;

A189: FF . f2' = F . r2'

proof

per cases ;

suppose A190: f2' = 1 / 2 ; :: thesis:

then FF . f2' = F1' . (1 / 2) by A61, FUNCT_4:14
.= F' . 0 by A61, A112, FUNCT_1:22
.= F . r2' by A44, A45, A66, A165, A166, A190, FUNCT_1:54 ;
hence FF . f2' = F . r2' ; :: thesis:

end;

suppose f2' <> 1 / 2 ; :: thesis:

then FF . f2' = F1 . f2' by A117, A168, FUNCT_4:12
.= F . ((P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) . f2') by A48, A168, FUNCT_1:23
.= F . r2' by A165, A166, FUNCT_1:54 ;
hence FF . f2' = F . r2' ; :: thesis:

end;

A191: G . l1 = f /. j by A62, A149, A164, A182, A187, BORSUK_1:83, FUNCT_1:22;
G . l2 = f /. (j + 1) by A62, A149, A164, A183, A189, 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 A164, A180, A184, A186, A191; :: thesis:

end;

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

then A192: j + 1 = n + 3 by A24, A30, NAT_1:9;
then LSeg f,j = LSeg (f /. (n + 2)),(f /. ((n + 2) + 1)) by A25, 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 A30, A36, A41, A42, A163, A192; :: 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;

A193: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A7, A18);
( 1 <= h1 + 2 & h1 + 2 <= len f ) by A5, XXREAL_0:2;
then consider NE being non empty Subset of (TOP-REAL 2) such that
A194: ( 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 A193;
thus 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, A6, A194; :: thesis: