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;
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 H₁( Element of NAT ) -> Element of K19( 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: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: 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:59;
A18: 2 <= len (f | 2) by A16, FINSEQ_1:59;
then reconsider NE = H₁( 0 ) as non empty Subset of (TOP-REAL 2) by TOPREAL1:23;
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: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:
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:40, RELSET_1:22; :: 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: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 = H₁(n + 1) as non empty Subset of (TOP-REAL 2) by A40, NAT_1:11, TOPREAL1:23;
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 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 by A55, A63, BORSUK_1:40;
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:
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:

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) (#))))) = H₁(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
.= H₁(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: H₁(n + 1) = H₁(n) \/ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) by A67, A68, TOPREAL3:38;
A95: the carrier of ((TOP-REAL 2) | H₁(n + 1)) = [#] ((TOP-REAL 2) | H₁(n + 1))
.= H₁(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: dom (F1 +* F19) = [#] I[01] by A102, BORSUK_1:40;
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:13
.= 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:13
.= 0 by TREAL_1:def 1 ;
A108: F1 . (1 / 2) = f /. (n + 2) by A77, A100, A106, FUNCT_1:12;
A109: F19 . (1 / 2) = f /. (n + 2) by A80, A101, A107, FUNCT_1:12;
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 4;
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:59, XXREAL_0:2;
A121: len (f | (n + 2)) = (n + 1) + 1 by A36, A43, FINSEQ_1:59, XXREAL_0:2;
then A122: k <= n + 1 by A119, XREAL_1:6;
A123: f is s.n.c. by A3;
A124: f is unfolded by A3;

now :: thesis:

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:6;
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:1;
A130: k + 1 in Seg (len (f | (n + 2))) by A119, A126, FINSEQ_1:1;
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:70;
A134: (f | (n + 2)) /. (k + 1) = f /. (k + 1) by A132, FINSEQ_4:70;
A135: LSeg (f,k) = LSeg ((f /. k),(f /. (k + 1))) by A118, A127, TOPREAL1:def 3
.= LSeg ((f | (n + 2)),k) by A118, A119, A133, A134, 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 A123, A128, A135, TOPREAL1:def 7;
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:1;
A143: (n + 1) + 1 in Seg (len (f | (n + 2))) by A120, A141, FINSEQ_1:1;
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:70;
A147: (f | (n + 2)) /. ((n + 1) + 1) = f /. ((n + 1) + 1) by A145, FINSEQ_4:70;
A148: LSeg (f,(n + 1)) = LSeg ((f /. (n + 1)),(f /. ((n + 1) + 1))) by A137, A138, TOPREAL1:def 3
.= LSeg ((f | (n + 2)),(n + 1)) by A120, A140, A146, A147, TOPREAL1:def 3 ;
LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))) = LSeg (f,((n + 1) + 1)) by A36, A42, TOPREAL1:def 3;
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 6;
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:68;
A152: len (f | (n + 2)) = n + 2 by A36, A43, FINSEQ_1:59, 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:1;
then A154: x = (f | (n + 2)) /. ((n + 1) + 1) by A150, A153, FINSEQ_4:70;
1 <= n + 1 by NAT_1:11;
then A155: x in LSeg ((f | (n + 2)),(n + 1)) by A152, A154, TOPREAL1:21;
A156: 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 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 4;
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 3;
then A157: {(f /. (n + 2))} c= rng F19 by ZFMISC_1:31;
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:59 ;
then A159: rng (F1 +* F19) = H₁(n) \/ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) by A89, A93, A157, TOPMETR2:2;
then A160: rng (F1 +* F19) = [#] ((TOP-REAL 2) | H₁(n + 1)) by A67, A68, A95, TOPREAL3:38;
rng (F1 +* F19) c= the carrier of ((TOP-REAL 2) | H₁(n + 1)) by A89, A93, A94, A95, A157, A158, TOPMETR2:2;
then reconsider FF = F1 +* F19 as Function of I[01],((TOP-REAL 2) | NE1) by A102, BORSUK_1:40, FUNCT_2:2;
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:13
.= 0 by TREAL_1:def 1 ;
A168: P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))) is onto by A161, FUNCT_2:def 3;
then A169: ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . 0 = ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . 0 by A166, TOPS_2:def 4
.= 0 by A164, A166, A167, FUNCT_1:32 ;
A170: (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 ;
A171: ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . 1 = ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . 1 by A168, A166, TOPS_2:def 4
.= 1 / 2 by A106, A165, A166, FUNCT_1:32 ;
A172: (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 ;
A173: LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))) = F19 .: [.(1 / 2),1.] by A9, A93, RELSET_1:22;
A174: FF . (1 / 2) = f /. (n + 2) by A101, A109, FUNCT_4:13;
A175: 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
A176: x in [.0,(1 / 2).] and
A177: x <> 1 / 2 ; :: thesis:
assume x in dom F19 ; :: thesis:
then x in (dom F1) /\ (dom F19) by A96, A176, XBOOLE_0:def 4;
hence contradiction by A111, A177, TARSKI:def 1; :: thesis:

end;

A178: 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
A179: x in [.(1 / 2),1.] and
A180: a = FF . x by FUNCT_1:def 6;
FF . x = F19 . x by A97, A179, FUNCT_4:13;
hence a in F19 .: [.(1 / 2),1.] by A97, A179, A180, FUNCT_1:def 6; :: 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
A181: x in dom F19 and
A182: x in [.(1 / 2),1.] and
A183: a = F19 . x by FUNCT_1:def 6;
A184: x in dom FF by A181, FUNCT_4:12;
a = FF . x by A181, A183, FUNCT_4:13;
hence a in FF .: [.(1 / 2),1.] by A182, A184, FUNCT_1:def 6; :: thesis:

end;

then A185: FF .: [.(1 / 2),1.] = F19 .: [.(1 / 2),1.] by A178, XBOOLE_0:def 10;
set GF = (G ") * FF;
A186: 0 in dom FF by A102, BORSUK_1:40, BORSUK_1:43;
A187: 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 A188: FF . 0 = F1 . 0 by A175, FUNCT_4:11
.= f /. 1 by A76, A164, A167, FUNCT_1:13 ;
1 in { l where l is Real : ( 1 / 2 <= l & l <= 1 ) } ;
then A189: 1 in dom F19 by A97, RCOMP_1:def 1;
then A190: FF . 1 = F19 . 1 by FUNCT_4:13
.= f /. ((n + 2) + 1) by A81, A172, A189, FUNCT_1:12 ;
A191: 0 in dom G by A55, BORSUK_1:43;
A192: G is onto by A54, FUNCT_2:def 3;
then A193: (G ") . (f /. 1) = (G ") . (f /. 1) by A53, TOPS_2:def 4
.= 0 by A51, A53, A191, FUNCT_1:32 ;
then A194: ((G ") * FF) . 0 = 0 by A186, A188, FUNCT_1:13;
A195: 1 in dom G by A55, BORSUK_1:43;
A196: (G ") . (f /. ((n + 2) + 1)) = (G ") . (f /. ((n + 2) + 1)) by A192, A53, TOPS_2:def 4
.= 1 by A52, A53, A195, FUNCT_1:32 ;
then A197: ((G ") * FF) . 1 = 1 by A187, A190, 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 A198: I[01] is T_2 by TOPMETR:2, TOPMETR:20, TOPMETR:def 6;
A199: T1 is compact by HEINE:4;
A200: T2 is compact by HEINE:4;
A201: F1 is continuous by A88, TOPS_2:def 5;
A202: F19 is continuous by A92, TOPS_2:def 5;
A203: (TOP-REAL 2) | NE is SubSpace of (TOP-REAL 2) | NE1 by A38, A94, TOPMETR:4;
A204: (TOP-REAL 2) | (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) is SubSpace of (TOP-REAL 2) | NE1 by A94, TOPMETR:4;
A205: g11 is continuous by A201, A203, PRE_TOPC:26;
A206: g22 is continuous by A202, A204, PRE_TOPC:26;
A207: [#] T1 = [.0,(1 / 2).] by TOPMETR:18;
A208: [#] T2 = [.(1 / 2),1.] by TOPMETR:18;
then A209: ([#] T1) \/ ([#] T2) = [#] I[01] by A207, BORSUK_1:40, XXREAL_1:174;
([#] T1) /\ ([#] T2) = {ppp} by A207, A208, XXREAL_1:418;
then reconsider FF = FF as continuous Function of I[01],((TOP-REAL 2) | NE1) by A108, A109, A198, A199, A200, A205, A206, A209, COMPTS_1:20;
A210: F1 is one-to-one by A88, TOPS_2:def 5;
A211: 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
A212: x1 in dom F19 and
A213: x2 in (dom F1) \ (dom F19) ; :: thesis:
assume A214: F19 . x1 = F1 . x2 ; :: thesis:
A215: F19 . x1 in LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))) by A93, A212, FUNCT_2:4;
A216: x2 in dom F1 by A213, XBOOLE_0:def 5;
A217: not x2 in dom F19 by A213, XBOOLE_0:def 5;
F1 . x2 in NE by A38, A89, A213, FUNCT_2:4;
then F1 . x2 in NE /\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) by A214, A215, XBOOLE_0:def 4;
then F1 . x2 = f /. (n + 2) by A38, A112;
hence contradiction by A100, A101, A108, A210, A216, A217, FUNCT_1:def 4; :: thesis:

end;

then A218: FF is one-to-one by A210, A211, TOPMETR2:1;
A219: G " is being_homeomorphism by A50, TOPS_2:56;
FF is being_homeomorphism by A103, A104, A105, A160, A218, COMPTS_1:17;
then A220: (G ") * FF is being_homeomorphism by A219, TOPS_2:57;
then A221: (G ") * FF is continuous by TOPS_2:def 5;
A222: dom ((G ") * FF) = [#] I[01] by A220, TOPS_2:def 5;
A223: rng ((G ") * FF) = [#] I[01] by A220, TOPS_2:def 5;
A224: (G ") * FF is one-to-one by A220, TOPS_2:def 5;
then A225: dom (((G ") * FF) ") = [#] I[01] by A223, TOPS_2:49;
A226: rng G = [#] ((TOP-REAL 2) | H₁(n + 1)) by A50, TOPS_2:def 5
.= rng FF by A67, A68, A95, A159, TOPREAL3:38 ;
A227: G * ((G ") * FF) = FF * (G * (G ")) by RELAT_1:36
.= (id (rng G)) * FF by A53, A54, TOPS_2:52
.= FF by A226, RELAT_1:54 ;
A228: 1 / 2 in dom ((G ") * FF) by A222, BORSUK_1:43;
then A229: ((G ") * FF) . (1 / 2) in rng ((G ") * FF) by FUNCT_1:def 3;
A230: ((G ") * FF) . (1 / 2) = (G ") . (FF . (1 / 2)) by A228, FUNCT_1:12
.= pp by A101, A109, FUNCT_4:13 ;
A231: [.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
A232: l1 = a and
A233: pp <= l1 and
A234: l1 <= 1 ;
A235: 0 <= pp by A229, A230, BORSUK_1:43;
set cos = (((G ") * FF) ") . l1;
l1 in dom (((G ") * FF) ") by A225, A233, A234, A235, BORSUK_1:43;
then A236: (((G ") * FF) ") . l1 in rng (((G ") * FF) ") by FUNCT_1:def 3;
then A237: (((G ") * FF) ") . l1 in [.0,1.] by BORSUK_1:40;
A238: l1 in rng ((G ") * FF) by A223, A233, A234, A235, BORSUK_1:43;
(G ") * FF is onto by A223, FUNCT_2:def 3;
then A239: ((G ") * FF) . ((((G ") * FF) ") . l1) = ((G ") * FF) . ((((G ") * FF) ") . l1) by A224, TOPS_2:def 4
.= l1 by A224, A238, FUNCT_1:35 ;
reconsider cos = (((G ") * FF) ") . l1 as Real by A237;
reconsider A3 = cos, A4 = 1, A5 = 1 / 2 as Point of I[01] by A236, 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 by Lm2;
A240: cos <= 1

proof

assume cos > 1 ; :: thesis:
then Fhc > Fh0 by A194, A197, A221, A224, JORDAN5A:16;
hence contradiction by A102, A190, A196, A234, A239, BORSUK_1:40, FUNCT_1:13; :: thesis:

end;

cos >= 1 / 2

proof

assume cos < 1 / 2 ; :: thesis:
then Fhc < Fh12 by A194, A197, A221, A224, JORDAN5A:16;
hence contradiction by A102, A174, A233, A239, BORSUK_1:40, FUNCT_1:13; :: thesis:

end;

then cos in { l where l is Real : ( 1 / 2 <= l & l <= 1 ) } by A240;
then cos in [.(1 / 2),1.] by RCOMP_1:def 1;
hence a in ((G ") * FF) .: [.(1 / 2),1.] by A222, A232, A236, A239, FUNCT_1:def 6; :: 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
A241: x in [.(1 / 2),1.] and
A242: a = ((G ") * FF) . x by FUNCT_1:def 6;
x in { l where l is Real : ( 1 / 2 <= l & l <= 1 ) } by A241, RCOMP_1:def 1;
then consider l1 being Real such that
A243: l1 = x and
A244: 1 / 2 <= l1 and
A245: l1 <= 1 ;
reconsider ll = l1, pol = 1 / 2 as Point of I[01] by A244, A245, 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 by Lm2;
A246: A4 >= A5

proof

per cases ;

suppose 1 <> l1 ; :: thesis:

then 1 > l1 by A245, XXREAL_0:1;
hence A4 >= A5 by A194, A197, A221, A224, BORSUK_1:def 15, JORDAN5A:16; :: thesis:

end;

suppose 1 = l1 ; :: thesis:

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

end;

A5 >= A6

proof

per cases ;

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

then l1 > 1 / 2 by A244, XXREAL_0:1;
hence A5 >= A6 by A194, A197, A221, A224, JORDAN5A:16; :: 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 A197, A230, A246, BORSUK_1:def 15;
hence a in [.pp,1.] by A242, A243, RCOMP_1:def 1; :: thesis:

end;

then [.pp,1.] = ((G ") * FF) .: [.(1 / 2),1.] by A231, XBOOLE_0:def 10;
then A247: G .: [.pp,1.] = LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))) by A173, A185, A227, 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 ;

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

then consider r1, r2 being Real such that
A248: r1 < r2 and
A249: 0 <= r1 and
A250: r1 <= 1 and
0 <= r2 and
A251: r2 <= 1 and
A252: LSeg (f,j) = F .: [.r1,r2.] and
A253: F . r1 = f /. j and
A254: 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;
A255: ( 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;
A256: dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = [#] (Closed-Interval-TSpace (0,(1 / 2))) by A82, TOPS_2:def 5;
A257: rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = [#] (Closed-Interval-TSpace (0,1)) by A82, TOPS_2:def 5;
then A258: P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))) is onto by FUNCT_2:def 3;
then A259: ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r1 = ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r1 by A255, TOPS_2:def 4;
A260: ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r2 = ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r2 by A255, A258, TOPS_2:def 4;
A261: 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 A262: r1 in rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) by A249, A250, BORSUK_1:43;
A263: r2 in rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) by A248, A249, A251, A261, BORSUK_1:43;
A264: ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r1 in the carrier of (Closed-Interval-TSpace (0,(1 / 2))) by A255, A256, A259, A262, FUNCT_1:32;
A265: ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r2 in the carrier of (Closed-Interval-TSpace (0,(1 / 2))) by A255, A256, A260, A263, FUNCT_1:32;
A266: ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r1 in [.0,(1 / 2).] by A264, TOPMETR:18;
A267: ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r2 in [.0,(1 / 2).] by A265, TOPMETR:18;
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 A266;
reconsider r19 = r1, r29 = r2 as Point of (Closed-Interval-TSpace (0,1)) by A248, A249, A250, A251, BORSUK_1:43, TOPMETR:20;
A268: (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) " is being_homeomorphism by A82, TOPS_2:56;
A269: f1 = ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r19 ;
A270: f2 = ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r29 ;
A271: ( (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 A268, TOPS_2:def 5;
then A272: f1 < f2 by A169, A171, A248, A269, A270, JORDAN5A:15;
A273: [.0,(1 / 2).] c= [.0,1.] by XXREAL_1:34;
A274: r1 = (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . f1 by A255, A259, A262, FUNCT_1:32;
A275: r2 = (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . f2 by A255, A260, A263, FUNCT_1:32;
A276: f1 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) } by A266, RCOMP_1:def 1;
A277: f2 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) } by A267, RCOMP_1:def 1;
A278: ex ff1 being Real st
( ff1 = f1 & 0 <= ff1 & ff1 <= 1 / 2 ) by A276;
ex ff2 being Real st
( ff2 = f2 & 0 <= ff2 & ff2 <= 1 / 2 ) by A277;
then A279: (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) .: [.f1,f2.] = [.r1,r2.] by A82, A106, A167, A272, A274, A275, A278, JORDAN5A:20;
A280: 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
A281: x in dom F1 and
A282: x in [.f1,f2.] and
A283: a = F1 . x by FUNCT_1:def 6;

A284: now :: thesis:

per cases ;

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

hence FF . x = F1 . x by A10, A175, A281, FUNCT_4:11; :: thesis:

end;

suppose x = 1 / 2 ; :: thesis:

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

end;

x in dom FF by A281, FUNCT_4:12;
hence a in FF .: [.f1,f2.] by A282, A283, A284, FUNCT_1:def 6; :: 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
A285: x in [.f1,f2.] and
A286: a = FF . x by FUNCT_1:def 6;
A287: [.f1,f2.] c= [.0,(1 / 2).] by A266, A267, XXREAL_2:def 12;

now :: thesis:

per cases ;

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

hence FF . x = F1 . x by A175, A285, A287, FUNCT_4:11; :: thesis:

end;

suppose x = 1 / 2 ; :: thesis:

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

end;

hence a in F1 .: [.f1,f2.] by A96, A285, A286, A287, FUNCT_1:def 6; :: thesis:

end;

then F1 .: [.f1,f2.] = FF .: [.f1,f2.] by A280, XBOOLE_0:def 10;
then A288: F .: [.r1,r2.] = FF .: [.f1,f2.] by A279, RELAT_1:126;
set e1 = ((G ") * FF) . f1;
set e2 = ((G ") * FF) . f2;
A289: ((G ") * FF) . f1 in the carrier of I[01] by A266, A273, BORSUK_1:40, FUNCT_2:5;
A290: ((G ") * FF) . f2 in the carrier of I[01] by A267, A273, BORSUK_1:40, FUNCT_2:5;
A291: ((G ") * FF) . f1 in { l where l is Real : ( 0 <= l & l <= 1 ) } by A289, BORSUK_1:40, RCOMP_1:def 1;
A292: ((G ") * FF) . f2 in { l where l is Real : ( 0 <= l & l <= 1 ) } by A290, BORSUK_1:40, RCOMP_1:def 1;
consider l1 being Real such that
A293: l1 = ((G ") * FF) . f1 and
A294: 0 <= l1 and
A295: l1 <= 1 by A291;
consider l2 being Real such that
A296: l2 = ((G ") * FF) . f2 and
0 <= l2 and
A297: l2 <= 1 by A292;
reconsider f19 = f1, f29 = f2 as Point of I[01] by A266, A267, A273, BORSUK_1:40;
A298: ((G ") * FF) . 0 = 0 by A186, A188, A193, FUNCT_1:13;
A299: ((G ") * FF) . 1 = 1 by A187, A190, A196, FUNCT_1:13;
A300: l1 = ((G ") * FF) . f19 by A293;
l2 = ((G ") * FF) . f29 by A296;
then A301: l1 < l2 by A221, A224, A272, A298, A299, A300, JORDAN5A:16;
A302: f1 < f2 by A169, A171, A248, A269, A270, A271, JORDAN5A:15;
A303: 0 <= f1 by A266, A273, BORSUK_1:40, BORSUK_1:43;
f2 <= 1 by A267, A273, BORSUK_1:40, BORSUK_1:43;
then A304: G .: [.l1,l2.] = G .: (((G ") * FF) .: [.f1,f2.]) by A194, A197, A220, A293, A296, A302, A303, JORDAN5A:20, TOPMETR:20
.= FF .: [.f1,f2.] by A227, RELAT_1:126 ;
A305: FF . f19 = F . r19

proof

per cases ;

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

then FF . f19 = F19 . (1 / 2) by A101, FUNCT_4:13
.= F9 . 0 by A101, A170, FUNCT_1:12
.= F . r19 by A77, A80, A106, A255, A257, A259, A306, FUNCT_1:32 ;
hence FF . f19 = F . r19 ; :: thesis:

end;

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

then FF . f19 = F1 . f19 by A175, A266, FUNCT_4:11
.= F . ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . f19) by A85, A266, FUNCT_1:13
.= F . r19 by A255, A257, A259, FUNCT_1:32 ;
hence FF . f19 = F . r19 ; :: thesis:

end;

A307: FF . f29 = F . r29

proof

per cases ;

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

then FF . f29 = F19 . (1 / 2) by A101, FUNCT_4:13
.= F9 . 0 by A101, A170, FUNCT_1:12
.= F . r29 by A77, A80, A106, A255, A257, A260, A308, FUNCT_1:32 ;
hence FF . f29 = F . r29 ; :: thesis:

end;

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

then FF . f29 = F1 . f29 by A175, A267, FUNCT_4:11
.= F . ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . f29) by A85, A267, FUNCT_1:13
.= F . r29 by A255, A257, A260, FUNCT_1:32 ;
hence FF . f29 = F . r29 ; :: thesis:

end;

A309: G . l1 = f /. j by A102, A227, A253, A293, A305, BORSUK_1:40, FUNCT_1:12;
G . l2 = f /. (j + 1) by A102, A227, A254, A296, A307, 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 A252, A288, A294, A295, A297, A301, A304, A309; :: thesis:

end;

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

then A310: 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, A247, A310; :: 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;

A311: 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 A311;
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: