:: JORDAN5B semantic presentation begin theorem Th1: :: JORDAN5B:1 for i1 being Nat st 1 <= i1 holds i1 -' 1 < i1 proof let i1 be Nat; ::_thesis: ( 1 <= i1 implies i1 -' 1 < i1 ) assume A1: 1 <= i1 ; ::_thesis: i1 -' 1 < i1 i1 - 1 < i1 - 0 by XREAL_1:15; hence i1 -' 1 < i1 by A1, XREAL_1:233; ::_thesis: verum end; theorem :: JORDAN5B:2 for i, k being Nat st i + 1 <= k holds 1 <= k -' i proof let i, k be Nat; ::_thesis: ( i + 1 <= k implies 1 <= k -' i ) assume i + 1 <= k ; ::_thesis: 1 <= k -' i then (i + 1) -' i <= k -' i by NAT_D:42; hence 1 <= k -' i by NAT_D:34; ::_thesis: verum end; theorem :: JORDAN5B:3 for i, k being Nat st 1 <= i & 1 <= k holds (k -' i) + 1 <= k proof let i, k be Nat; ::_thesis: ( 1 <= i & 1 <= k implies (k -' i) + 1 <= k ) assume that A1: 1 <= i and A2: 1 <= k ; ::_thesis: (k -' i) + 1 <= k k -' i <= k -' 1 by A1, NAT_D:41; then (k -' i) + 1 <= (k -' 1) + 1 by XREAL_1:6; hence (k -' i) + 1 <= k by A2, XREAL_1:235; ::_thesis: verum end; Lm1: for r being real number st 0 <= r & r <= 1 holds ( 0 <= 1 - r & 1 - r <= 1 ) proof let r be real number ; ::_thesis: ( 0 <= r & r <= 1 implies ( 0 <= 1 - r & 1 - r <= 1 ) ) assume that A1: 0 <= r and A2: r <= 1 ; ::_thesis: ( 0 <= 1 - r & 1 - r <= 1 ) A3: 1 - 1 <= 1 - r by A2, XREAL_1:13; 1 - r <= 1 - 0 by A1, XREAL_1:13; hence ( 0 <= 1 - r & 1 - r <= 1 ) by A3; ::_thesis: verum end; theorem :: JORDAN5B:4 for r being real number st r in the carrier of I[01] holds 1 - r in the carrier of I[01] proof let r be real number ; ::_thesis: ( r in the carrier of I[01] implies 1 - r in the carrier of I[01] ) assume A1: r in the carrier of I[01] ; ::_thesis: 1 - r in the carrier of I[01] then A2: 0 <= r by BORSUK_1:43; A3: r <= 1 by A1, BORSUK_1:43; then A4: 0 <= 1 - r by A2, Lm1; 1 - r <= 1 by A2, A3, Lm1; hence 1 - r in the carrier of I[01] by A4, BORSUK_1:43; ::_thesis: verum end; theorem :: JORDAN5B:5 for p, q, p1 being Point of (TOP-REAL 2) st p `2 <> q `2 & p1 in LSeg (p,q) & p1 `2 = p `2 holds p1 = p proof let p, q, p1 be Point of (TOP-REAL 2); ::_thesis: ( p `2 <> q `2 & p1 in LSeg (p,q) & p1 `2 = p `2 implies p1 = p ) assume that A1: p `2 <> q `2 and A2: p1 in LSeg (p,q) ; ::_thesis: ( not p1 `2 = p `2 or p1 = p ) assume A3: p1 `2 = p `2 ; ::_thesis: p1 = p assume A4: p1 <> p ; ::_thesis: contradiction consider l1 being Real such that A5: p1 = ((1 - l1) * p) + (l1 * q) and 0 <= l1 and l1 <= 1 by A2; A6: ((1 - l1) * p) + (l1 * q) = |[((((1 - l1) * p) `1) + ((l1 * q) `1)),((((1 - l1) * p) `2) + ((l1 * q) `2))]| by EUCLID:55; A7: (1 - l1) * p = |[((1 - l1) * (p `1)),((1 - l1) * (p `2))]| by EUCLID:57; A8: l1 * q = |[(l1 * (q `1)),(l1 * (q `2))]| by EUCLID:57; p `2 = (((1 - l1) * p) `2) + ((l1 * q) `2) by A3, A5, A6, EUCLID:52 .= ((1 - l1) * (p `2)) + ((l1 * q) `2) by A7, EUCLID:52 .= ((1 - l1) * (p `2)) + (l1 * (q `2)) by A8, EUCLID:52 ; then (1 - (1 - l1)) * (p `2) = l1 * (q `2) ; then l1 = 0 by A1, XCMPLX_1:5; then p1 = (1 * p) + (0. (TOP-REAL 2)) by A5, EUCLID:29 .= p + (0. (TOP-REAL 2)) by EUCLID:29 .= p by EUCLID:27 ; hence contradiction by A4; ::_thesis: verum end; theorem :: JORDAN5B:6 for p, q, p1 being Point of (TOP-REAL 2) st p `1 <> q `1 & p1 in LSeg (p,q) & p1 `1 = p `1 holds p1 = p proof let p, q, p1 be Point of (TOP-REAL 2); ::_thesis: ( p `1 <> q `1 & p1 in LSeg (p,q) & p1 `1 = p `1 implies p1 = p ) assume that A1: p `1 <> q `1 and A2: p1 in LSeg (p,q) ; ::_thesis: ( not p1 `1 = p `1 or p1 = p ) assume A3: p1 `1 = p `1 ; ::_thesis: p1 = p assume A4: p1 <> p ; ::_thesis: contradiction consider l1 being Real such that A5: p1 = ((1 - l1) * p) + (l1 * q) and 0 <= l1 and l1 <= 1 by A2; A6: ((1 - l1) * p) + (l1 * q) = |[((((1 - l1) * p) `1) + ((l1 * q) `1)),((((1 - l1) * p) `2) + ((l1 * q) `2))]| by EUCLID:55; A7: (1 - l1) * p = |[((1 - l1) * (p `1)),((1 - l1) * (p `2))]| by EUCLID:57; A8: l1 * q = |[(l1 * (q `1)),(l1 * (q `2))]| by EUCLID:57; p `1 = (((1 - l1) * p) `1) + ((l1 * q) `1) by A3, A5, A6, EUCLID:52 .= ((1 - l1) * (p `1)) + ((l1 * q) `1) by A7, EUCLID:52 .= ((1 - l1) * (p `1)) + (l1 * (q `1)) by A8, EUCLID:52 ; then (1 - (1 - l1)) * (p `1) = l1 * (q `1) ; then l1 = 0 by A1, XCMPLX_1:5; then p1 = (1 * p) + (0. (TOP-REAL 2)) by A5, EUCLID:29 .= p + (0. (TOP-REAL 2)) by EUCLID:29 .= p by EUCLID:27 ; hence contradiction by A4; ::_thesis: verum end; Lm2: for P being Point of I[01] holds P is Real proof let P be Point of I[01]; ::_thesis: P is Real P in [.0,1.] by BORSUK_1:40; hence P is Real ; ::_thesis: verum end; theorem Th7: :: JORDAN5B:7 for f being FinSequence of (TOP-REAL 2) for P being non empty Subset of (TOP-REAL 2) for F being Function of I[01],((TOP-REAL 2) | P) for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & P = L~ f & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) holds ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = F .: [.p1,p2.] & F . p1 = f /. i & F . p2 = f /. (i + 1) ) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for P being non empty Subset of (TOP-REAL 2) for F being Function of I[01],((TOP-REAL 2) | P) for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & P = L~ f & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) holds ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = F .: [.p1,p2.] & F . p1 = f /. i & F . p2 = f /. (i + 1) ) let P be non empty Subset of (TOP-REAL 2); ::_thesis: for F being Function of I[01],((TOP-REAL 2) | P) for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & P = L~ f & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) holds ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = F .: [.p1,p2.] & F . p1 = f /. i & F . p2 = f /. (i + 1) ) let Ff be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & P = L~ f & Ff is being_homeomorphism & Ff . 0 = f /. 1 & Ff . 1 = f /. (len f) holds ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = Ff .: [.p1,p2.] & Ff . p1 = f /. i & Ff . p2 = f /. (i + 1) ) let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len f & f is being_S-Seq & P = L~ f & Ff is being_homeomorphism & Ff . 0 = f /. 1 & Ff . 1 = f /. (len f) implies ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = Ff .: [.p1,p2.] & Ff . p1 = f /. i & Ff . p2 = f /. (i + 1) ) ) assume that A1: 1 <= i and A2: i + 1 <= len f and A3: f is being_S-Seq and A4: P = L~ f and A5: Ff is being_homeomorphism and A6: Ff . 0 = f /. 1 and A7: Ff . 1 = f /. (len f) ; ::_thesis: ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = Ff .: [.p1,p2.] & Ff . p1 = f /. i & Ff . p2 = f /. (i + 1) ) A8: f is one-to-one by A3; A9: the carrier of (Closed-Interval-TSpace ((1 / 2),1)) = [.(1 / 2),1.] by TOPMETR:18; A10: [#] (Closed-Interval-TSpace (0,(1 / 2))) = [.0,(1 / 2).] by TOPMETR:18; A11: [#] (Closed-Interval-TSpace ((1 / 2),1)) = [.(1 / 2),1.] by TOPMETR:18; A12: len f >= 2 by A3, TOPREAL1:def_8; deffunc H1( Element of NAT ) -> Element of K19( the carrier of (TOP-REAL 2)) = L~ (f | ($1 + 2)); defpred S1[ Element of NAT ] means ( 1 <= $1 + 2 & $1 + 2 <= len f implies ex NE being non empty Subset of (TOP-REAL 2) st ( NE = H1($1) & ( for j being 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: S1[ 0 ] proof assume that A15: 1 <= 0 + 2 and A16: 0 + 2 <= len f ; ::_thesis: ex NE being non empty Subset of (TOP-REAL 2) st ( NE = H1( 0 ) & ( for j being Element of NAT for F being Function of I[01],((TOP-REAL 2) | NE) st 1 <= j & j + 1 <= 0 + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (0 + 2) holds ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) ) ) A17: 1 <= len (f | 2) by A15, A16, FINSEQ_1:59; A18: 2 <= len (f | 2) by A16, FINSEQ_1:59; then reconsider NE = H1( 0 ) as non empty Subset of (TOP-REAL 2) by TOPREAL1:23; take NE ; ::_thesis: ( NE = H1( 0 ) & ( for j being Element of NAT for F being Function of I[01],((TOP-REAL 2) | NE) st 1 <= j & j + 1 <= 0 + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (0 + 2) holds ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) ) ) thus NE = H1( 0 ) ; ::_thesis: for j being Element of NAT for F being Function of I[01],((TOP-REAL 2) | NE) st 1 <= j & j + 1 <= 0 + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (0 + 2) holds ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) let j be Element of NAT ; ::_thesis: for F being Function of I[01],((TOP-REAL 2) | NE) st 1 <= j & j + 1 <= 0 + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (0 + 2) holds ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) let F be Function of I[01],((TOP-REAL 2) | NE); ::_thesis: ( 1 <= j & j + 1 <= 0 + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (0 + 2) implies ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) ) assume that A19: 1 <= j and A20: j + 1 <= 0 + 2 and A21: F is being_homeomorphism and A22: F . 0 = f /. 1 and A23: F . 1 = f /. (0 + 2) ; ::_thesis: ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) j <= (1 + 1) - 1 by A20, XREAL_1:19; then A24: j = 1 by A19, XXREAL_0:1; A25: len (f | 2) = 2 by A16, FINSEQ_1:59; A26: 1 in dom (f | 2) by A17, FINSEQ_3:25; A27: 2 in dom (f | 2) by A18, FINSEQ_3:25; A28: (f | 2) /. 1 = (f | 2) . 1 by A26, PARTFUN1:def_6; A29: (f | 2) /. 2 = (f | 2) . 2 by A27, PARTFUN1:def_6; A30: (f | 2) /. 1 = f /. 1 by A26, FINSEQ_4:70; A31: 1 + 1 <= len f by A16; A32: rng F = [#] ((TOP-REAL 2) | NE) by A21, TOPS_2:def_5 .= L~ (f | 2) by PRE_TOPC:def_5 .= L~ <*((f | 2) /. 1),((f | 2) /. 2)*> by A25, A28, A29, FINSEQ_1:44 .= LSeg (((f | 2) /. 1),((f | 2) /. 2)) by SPPOL_2:21 .= LSeg ((f /. 1),(f /. 2)) by A27, A30, FINSEQ_4:70 .= LSeg (f,1) by A31, TOPREAL1:def_3 ; take 0 ; ::_thesis: ex p2 being Real st ( 0 < p2 & 0 <= 0 & 0 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.0,p2.] & F . 0 = f /. j & F . p2 = f /. (j + 1) ) take 1 ; ::_thesis: ( 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) ) 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: verum end; A33: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A34: S1[n] ; ::_thesis: S1[n + 1] assume that A35: 1 <= (n + 1) + 2 and A36: (n + 1) + 2 <= len f ; ::_thesis: ex NE being non empty Subset of (TOP-REAL 2) st ( NE = H1(n + 1) & ( for j being Element of NAT for F being Function of I[01],((TOP-REAL 2) | NE) st 1 <= j & j + 1 <= (n + 1) + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. ((n + 1) + 2) holds ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) ) ) A37: 2 <= n + 2 by NAT_1:11; n + 2 <= (n + 2) + 1 by NAT_1:11; then consider NE being non empty Subset of (TOP-REAL 2) such that A38: NE = H1(n) and A39: for j being 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 = H1(n + 1) as non empty Subset of (TOP-REAL 2) by A40, NAT_1:11, TOPREAL1:23; take NE1 ; ::_thesis: ( NE1 = H1(n + 1) & ( for j being Element of NAT for F being Function of I[01],((TOP-REAL 2) | NE1) st 1 <= j & j + 1 <= (n + 1) + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. ((n + 1) + 2) holds ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) ) ) thus NE1 = H1(n + 1) ; ::_thesis: for j being Element of NAT for F being Function of I[01],((TOP-REAL 2) | NE1) st 1 <= j & j + 1 <= (n + 1) + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. ((n + 1) + 2) holds ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) let j be Element of NAT ; ::_thesis: for F being Function of I[01],((TOP-REAL 2) | NE1) st 1 <= j & j + 1 <= (n + 1) + 2 & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. ((n + 1) + 2) holds ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = F .: [.p1,p2.] & F . p1 = f /. j & F . p2 = f /. (j + 1) ) let G be Function of I[01],((TOP-REAL 2) | NE1); ::_thesis: ( 1 <= j & j + 1 <= (n + 1) + 2 & G is being_homeomorphism & G . 0 = f /. 1 & G . 1 = f /. ((n + 1) + 2) implies ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = G .: [.p1,p2.] & G . p1 = f /. j & G . p2 = f /. (j + 1) ) ) assume that A48: 1 <= j and A49: j + 1 <= (n + 1) + 2 and A50: G is being_homeomorphism and A51: G . 0 = f /. 1 and A52: G . 1 = f /. ((n + 1) + 2) ; ::_thesis: ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = G .: [.p1,p2.] & G . p1 = f /. j & G . p2 = f /. (j + 1) ) A53: G is one-to-one by A50, TOPS_2:def_5; A54: rng G = [#] ((TOP-REAL 2) | H1(n + 1)) by A50, TOPS_2:def_5; A55: dom G = [#] I[01] by A50, TOPS_2:def_5; A56: rng G = L~ (f | (n + 3)) by A54, PRE_TOPC:def_5; set pp = (G ") . (f /. (n + 2)); G is onto by A54, FUNCT_2:def_3; then A57: (G ") . (f /. (n + 2)) = (G ") . (f /. (n + 2)) by A53, TOPS_2:def_4; A58: n + 2 <= len (f | (n + 2)) by A36, A43, FINSEQ_1:59, XXREAL_0:2; A59: 1 <= len (f | (n + 2)) by A36, A42, A43, FINSEQ_1:59, XXREAL_0:2; A60: n + 2 in dom (f | (n + 2)) by A42, A58, FINSEQ_3:25; A61: 1 in dom (f | (n + 2)) by A59, FINSEQ_3:25; A62: f /. (n + 2) in rng G by A40, A46, A47, A56, GOBOARD1:1, NAT_1:11; then A63: (G ") . (f /. (n + 2)) in dom G by A53, A57, FUNCT_1:32; A64: f /. (n + 2) = G . ((G ") . (f /. (n + 2))) by A53, A57, A62, FUNCT_1:32; reconsider pp = (G ") . (f /. (n + 2)) as Real 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: contradiction then f /. (n + 2) = f /. ((n + 1) + 2) by A52, A53, A57, A62, FUNCT_1:32; hence contradiction by A8, A66, A67, A68, PARTFUN2:10; ::_thesis: verum end; A70: 0 <= pp by A63, BORSUK_1:43; pp <= 1 by A63, BORSUK_1:43; then A71: pp < 1 by A69, XXREAL_0:1; set pn = f /. (n + 2); set pn1 = f /. ((n + 2) + 1); A72: f /. (n + 2) = (f | (n + 2)) /. (n + 2) by A60, FINSEQ_4:70; A73: (f | (n + 2)) /. 1 = f /. 1 by A61, FINSEQ_4:70; A74: len (f | (n + 2)) = n + 2 by A36, A43, FINSEQ_1:59, XXREAL_0:2; f | (n + 2) is being_S-Seq by A3, JORDAN3:4, NAT_1:11; then NE is_an_arc_of (f | (n + 2)) /. 1,f /. (n + 2) by A38, A72, A74, TOPREAL1:25; then consider F being Function of I[01],((TOP-REAL 2) | NE) such that A75: F is being_homeomorphism and A76: F . 0 = f /. 1 and A77: F . 1 = f /. (n + 2) by A73, TOPREAL1:def_1; A78: (n + 1) + 1 in dom f by A42, A44, FINSEQ_3:25; (n + 2) + 1 in dom f by A35, A36, FINSEQ_3:25; then LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))) is_an_arc_of f /. (n + 2),f /. ((n + 2) + 1) by A8, A65, A78, PARTFUN2:10, TOPREAL1:9; then consider F9 being Function of I[01],((TOP-REAL 2) | (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))))) such that A79: F9 is being_homeomorphism and A80: F9 . 0 = f /. (n + 2) and A81: F9 . 1 = f /. ((n + 2) + 1) by TOPREAL1:def_1; set Ex1 = P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))); set Ex2 = P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))); set F1 = F * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))); set F19 = F9 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))); A82: P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))) is being_homeomorphism by TREAL_1:17; A83: P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))) is being_homeomorphism by TREAL_1:17; A84: dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = [#] (Closed-Interval-TSpace (0,(1 / 2))) by A82, TOPS_2:def_5; then A85: dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = [.0,(1 / 2).] by TOPMETR:18; dom F = [#] I[01] by A75, TOPS_2:def_5; then A86: rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = dom F by A82, TOPMETR:20, TOPS_2:def_5; then rng (F * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) = rng F by RELAT_1:28; then rng (F * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) = [#] ((TOP-REAL 2) | NE) by A75, TOPS_2:def_5; then A87: rng (F * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) = H1(n) by A38, PRE_TOPC:def_5; dom (F * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) = the carrier of (Closed-Interval-TSpace (0,(1 / 2))) by A84, A86, RELAT_1:27; then reconsider F1 = F * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) as Function of (Closed-Interval-TSpace (0,(1 / 2))),((TOP-REAL 2) | NE) by FUNCT_2:def_1; A88: F1 is being_homeomorphism by A75, A82, TOPMETR:20, TOPS_2:57; then A89: rng F1 = [#] ((TOP-REAL 2) | NE) by TOPS_2:def_5 .= H1(n) by A38, PRE_TOPC:def_5 ; A90: dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = [#] (Closed-Interval-TSpace ((1 / 2),1)) by A83, TOPS_2:def_5; dom F9 = [#] I[01] by A79, TOPS_2:def_5; then A91: rng (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = dom F9 by A83, TOPMETR:20, TOPS_2:def_5; then dom (F9 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) = the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by A90, RELAT_1:27; then reconsider F19 = F9 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) as Function of (Closed-Interval-TSpace ((1 / 2),1)),((TOP-REAL 2) | (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))))) by FUNCT_2:def_1; A92: F19 is being_homeomorphism by A79, A83, TOPMETR:20, TOPS_2:57; then A93: rng F19 = [#] ((TOP-REAL 2) | (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))))) by TOPS_2:def_5 .= LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))) by PRE_TOPC:def_5 ; set FF = F1 +* F19; reconsider T1 = Closed-Interval-TSpace (0,(1 / 2)), T2 = Closed-Interval-TSpace ((1 / 2),1) as SubSpace of I[01] by TOPMETR:20, TREAL_1:3; A94: H1(n + 1) = H1(n) \/ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) by A67, A68, TOPREAL3:38; A95: the carrier of ((TOP-REAL 2) | H1(n + 1)) = [#] ((TOP-REAL 2) | H1(n + 1)) .= H1(n + 1) by PRE_TOPC:def_5 ; dom F1 = the carrier of T1 by A84, A86, RELAT_1:27; then reconsider g11 = F1 as Function of T1,((TOP-REAL 2) | NE1) by A87, A94, A95, RELSET_1:4, XBOOLE_1:7; dom F19 = the carrier of T2 by A90, A91, RELAT_1:27; then reconsider g22 = F19 as Function of T2,((TOP-REAL 2) | NE1) by A93, A94, A95, RELSET_1:4, XBOOLE_1:7; A96: [.0,(1 / 2).] = dom F1 by A10, A88, TOPS_2:def_5; A97: [.(1 / 2),1.] = dom F19 by A11, A92, TOPS_2:def_5; A98: 1 / 2 in { l where l is Real : ( 0 <= l & l <= 1 / 2 ) } ; A99: 1 / 2 in { l where l is Real : ( 1 / 2 <= l & l <= 1 ) } ; A100: 1 / 2 in dom F1 by A96, A98, RCOMP_1:def_1; A101: 1 / 2 in dom F19 by A97, A99, RCOMP_1:def_1; A102: dom (F1 +* F19) = [.0,(1 / 2).] \/ [.(1 / 2),1.] by A96, A97, FUNCT_4:def_1 .= [.0,1.] by XXREAL_1:174 ; A103: I[01] is compact by HEINE:4, TOPMETR:20; A104: (TOP-REAL 2) | NE1 is T_2 by TOPMETR:2; A105: 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 H1(n) /\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) iff x = f /. (n + 2) ) proof let x be set ; ::_thesis: ( x in H1(n) /\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) iff x = f /. (n + 2) ) thus ( x in H1(n) /\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) implies x = f /. (n + 2) ) ::_thesis: ( x = f /. (n + 2) implies x in H1(n) /\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) ) proof assume A113: x in H1(n) /\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) ; ::_thesis: x = f /. (n + 2) then A114: x in LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1))) by XBOOLE_0:def_4; x in H1(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:_not_k_<_n_+_1 assume A125: k < n + 1 ; ::_thesis: contradiction 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: verum 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: verum end; assume A150: x = f /. (n + 2) ; ::_thesis: x in H1(n) /\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) 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 H1(n) by TOPREAL1:def_4; hence x in H1(n) /\ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) by A151, XBOOLE_0:def_4; ::_thesis: verum 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) = H1(n) \/ (LSeg ((f /. (n + 2)),(f /. ((n + 2) + 1)))) by A89, A93, A157, TOPMETR2:2; then A160: rng (F1 +* F19) = [#] ((TOP-REAL 2) | H1(n + 1)) by A67, A68, A95, TOPREAL3:38; rng (F1 +* F19) c= the carrier of ((TOP-REAL 2) | H1(n + 1)) by A89, A93, A94, A95, 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: ( x in [.0,(1 / 2).] & x <> 1 / 2 implies not x in dom F19 ) assume that A176: x in [.0,(1 / 2).] and A177: x <> 1 / 2 ; ::_thesis: not x in dom F19 assume x in dom F19 ; ::_thesis: contradiction then x in (dom F1) /\ (dom F19) by A96, A176, XBOOLE_0:def_4; hence contradiction by A111, A177, TARSKI:def_1; ::_thesis: verum end; A178: FF .: [.(1 / 2),1.] c= F19 .: [.(1 / 2),1.] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in FF .: [.(1 / 2),1.] or a in F19 .: [.(1 / 2),1.] ) assume a in FF .: [.(1 / 2),1.] ; ::_thesis: a in F19 .: [.(1 / 2),1.] then consider x being 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: verum end; F19 .: [.(1 / 2),1.] c= FF .: [.(1 / 2),1.] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in F19 .: [.(1 / 2),1.] or a in FF .: [.(1 / 2),1.] ) assume a in F19 .: [.(1 / 2),1.] ; ::_thesis: a in FF .: [.(1 / 2),1.] then consider x being 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: verum 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: ( x1 in dom F19 & x2 in (dom F1) \ (dom F19) implies F19 . x1 <> F1 . x2 ) assume that A212: x1 in dom F19 and A213: x2 in (dom F1) \ (dom F19) ; ::_thesis: F19 . x1 <> F1 . x2 assume A214: F19 . x1 = F1 . x2 ; ::_thesis: contradiction 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: verum 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) | H1(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: ( not a in [.pp,1.] or a in ((G ") * FF) .: [.(1 / 2),1.] ) assume a in [.pp,1.] ; ::_thesis: a in ((G ") * FF) .: [.(1 / 2),1.] then a in { l where l is Real : ( pp <= l & l <= 1 ) } by RCOMP_1:def_1; then consider l1 being Real such that 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: contradiction 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: verum end; cos >= 1 / 2 proof assume cos < 1 / 2 ; ::_thesis: contradiction then Fhc < Fh12 by A194, A197, A221, A224, JORDAN5A:16; hence contradiction by A102, A174, A233, A239, BORSUK_1:40, FUNCT_1:13; ::_thesis: verum 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: verum end; ((G ") * FF) .: [.(1 / 2),1.] c= [.pp,1.] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ((G ") * FF) .: [.(1 / 2),1.] or a in [.pp,1.] ) assume a in ((G ") * FF) .: [.(1 / 2),1.] ; ::_thesis: a in [.pp,1.] then consider x being 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 percases ( 1 <> l1 or 1 = l1 ) ; suppose 1 <> l1 ; ::_thesis: A4 >= A5 then 1 > l1 by A245, XXREAL_0:1; hence A4 >= A5 by A194, A197, A221, A224, BORSUK_1:def_15, JORDAN5A:16; ::_thesis: verum end; suppose 1 = l1 ; ::_thesis: A4 >= A5 hence A4 >= A5 by BORSUK_1:def_15; ::_thesis: verum end; end; end; A5 >= A6 proof percases ( l1 <> 1 / 2 or l1 = 1 / 2 ) ; suppose l1 <> 1 / 2 ; ::_thesis: A5 >= A6 then l1 > 1 / 2 by A244, XXREAL_0:1; hence A5 >= A6 by A194, A197, A221, A224, JORDAN5A:16; ::_thesis: verum end; suppose l1 = 1 / 2 ; ::_thesis: A5 >= A6 hence A5 >= A6 ; ::_thesis: verum end; end; end; then A5 in { l where l is Real : ( pp <= l & l <= 1 ) } by A197, A230, A246, BORSUK_1:def_15; hence a in [.pp,1.] by A242, A243, RCOMP_1:def_1; ::_thesis: verum 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 percases ( j + 1 <= n + 2 or j + 1 > n + 2 ) ; suppose j + 1 <= n + 2 ; ::_thesis: ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = G .: [.p1,p2.] & G . p1 = f /. j & G . p2 = f /. (j + 1) ) then consider r1, r2 being Real such that 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: ( not a in F1 .: [.f1,f2.] or a in FF .: [.f1,f2.] ) assume a in F1 .: [.f1,f2.] ; ::_thesis: a in FF .: [.f1,f2.] then consider x being 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:_FF_._x_=_F1_._x percases ( x <> 1 / 2 or x = 1 / 2 ) ; suppose x <> 1 / 2 ; ::_thesis: FF . x = F1 . x hence FF . x = F1 . x by A10, A175, A281, FUNCT_4:11; ::_thesis: verum end; suppose x = 1 / 2 ; ::_thesis: FF . x = F1 . x hence FF . x = F1 . x by A101, A108, A109, FUNCT_4:13; ::_thesis: verum end; end; 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: verum end; FF .: [.f1,f2.] c= F1 .: [.f1,f2.] proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in FF .: [.f1,f2.] or a in F1 .: [.f1,f2.] ) assume a in FF .: [.f1,f2.] ; ::_thesis: a in F1 .: [.f1,f2.] then consider x being 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:_FF_._x_=_F1_._x percases ( x <> 1 / 2 or x = 1 / 2 ) ; suppose x <> 1 / 2 ; ::_thesis: FF . x = F1 . x hence FF . x = F1 . x by A175, A285, A287, FUNCT_4:11; ::_thesis: verum end; suppose x = 1 / 2 ; ::_thesis: FF . x = F1 . x hence FF . x = F1 . x by A101, A108, A109, FUNCT_4:13; ::_thesis: verum end; end; end; hence a in F1 .: [.f1,f2.] by A96, A285, A286, A287, FUNCT_1:def_6; ::_thesis: verum 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 percases ( f19 = 1 / 2 or f19 <> 1 / 2 ) ; supposeA306: f19 = 1 / 2 ; ::_thesis: FF . f19 = F . r19 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: verum end; suppose f19 <> 1 / 2 ; ::_thesis: FF . f19 = F . r19 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: verum end; end; end; A307: FF . f29 = F . r29 proof percases ( f29 = 1 / 2 or f29 <> 1 / 2 ) ; supposeA308: f29 = 1 / 2 ; ::_thesis: FF . f29 = F . r29 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: verum end; suppose f29 <> 1 / 2 ; ::_thesis: FF . f29 = F . r29 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: verum end; end; 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: verum end; suppose j + 1 > n + 2 ; ::_thesis: ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = G .: [.p1,p2.] & G . p1 = f /. j & G . p2 = f /. (j + 1) ) then 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: verum end; end; end; hence ex p1, p2 being Real st ( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,j) = G .: [.p1,p2.] & G . p1 = f /. j & G . p2 = f /. (j + 1) ) ; ::_thesis: verum end; A311: for n being Element of NAT holds S1[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 = H1(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: verum end; theorem :: JORDAN5B:8 for f being FinSequence of (TOP-REAL 2) for Q, R being non empty Subset of (TOP-REAL 2) for F being Function of I[01],((TOP-REAL 2) | Q) for i being Element of NAT for P being non empty Subset of I[01] st f is being_S-Seq & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & 1 <= i & i + 1 <= len f & F .: P = LSeg (f,i) & Q = L~ f & R = LSeg (f,i) holds ex G being Function of (I[01] | P),((TOP-REAL 2) | R) st ( G = F | P & G is being_homeomorphism ) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q, R being non empty Subset of (TOP-REAL 2) for F being Function of I[01],((TOP-REAL 2) | Q) for i being Element of NAT for P being non empty Subset of I[01] st f is being_S-Seq & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & 1 <= i & i + 1 <= len f & F .: P = LSeg (f,i) & Q = L~ f & R = LSeg (f,i) holds ex G being Function of (I[01] | P),((TOP-REAL 2) | R) st ( G = F | P & G is being_homeomorphism ) let Q, R be non empty Subset of (TOP-REAL 2); ::_thesis: for F being Function of I[01],((TOP-REAL 2) | Q) for i being Element of NAT for P being non empty Subset of I[01] st f is being_S-Seq & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & 1 <= i & i + 1 <= len f & F .: P = LSeg (f,i) & Q = L~ f & R = LSeg (f,i) holds ex G being Function of (I[01] | P),((TOP-REAL 2) | R) st ( G = F | P & G is being_homeomorphism ) let F be Function of I[01],((TOP-REAL 2) | Q); ::_thesis: for i being Element of NAT for P being non empty Subset of I[01] st f is being_S-Seq & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & 1 <= i & i + 1 <= len f & F .: P = LSeg (f,i) & Q = L~ f & R = LSeg (f,i) holds ex G being Function of (I[01] | P),((TOP-REAL 2) | R) st ( G = F | P & G is being_homeomorphism ) let i be Element of NAT ; ::_thesis: for P being non empty Subset of I[01] st f is being_S-Seq & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & 1 <= i & i + 1 <= len f & F .: P = LSeg (f,i) & Q = L~ f & R = LSeg (f,i) holds ex G being Function of (I[01] | P),((TOP-REAL 2) | R) st ( G = F | P & G is being_homeomorphism ) let P be non empty Subset of I[01]; ::_thesis: ( f is being_S-Seq & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & 1 <= i & i + 1 <= len f & F .: P = LSeg (f,i) & Q = L~ f & R = LSeg (f,i) implies ex G being Function of (I[01] | P),((TOP-REAL 2) | R) st ( G = F | P & G is being_homeomorphism ) ) assume that A1: f is being_S-Seq and A2: F is being_homeomorphism and A3: F . 0 = f /. 1 and A4: F . 1 = f /. (len f) and A5: 1 <= i and A6: i + 1 <= len f and A7: F .: P = LSeg (f,i) and A8: Q = L~ f and A9: R = LSeg (f,i) ; ::_thesis: ex G being Function of (I[01] | P),((TOP-REAL 2) | R) st ( G = F | P & G is being_homeomorphism ) consider ppi, pi1 being Real such that A10: ppi < pi1 and A11: 0 <= ppi and ppi <= 1 and 0 <= pi1 and A12: pi1 <= 1 and A13: LSeg (f,i) = F .: [.ppi,pi1.] and F . ppi = f /. i and F . pi1 = f /. (i + 1) by A1, A2, A3, A4, A5, A6, A8, Th7; ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A10; then reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01] by A11, A12, BORSUK_1:40, RCOMP_1:def_1, XXREAL_1:34; A14: the carrier of (I[01] | Poz) = [#] (I[01] | Poz) .= Poz by PRE_TOPC:def_5 ; A15: dom F = [#] I[01] by A2, TOPS_2:def_5 .= [.0,1.] by BORSUK_1:40 ; A16: F is one-to-one by A2, TOPS_2:def_5; then A17: P c= Poz by A7, A13, A15, BORSUK_1:40, FUNCT_1:87; Poz c= P by A7, A13, A15, A16, BORSUK_1:40, FUNCT_1:87; then A18: P = Poz by A17, XBOOLE_0:def_10; set gg = F | P; reconsider gg = F | P as Function of (I[01] | Poz),((TOP-REAL 2) | Q) by A14, A18, FUNCT_2:32; reconsider SEG = LSeg (f,i) as non empty Subset of ((TOP-REAL 2) | Q) by A7, A9; A19: the carrier of (((TOP-REAL 2) | Q) | SEG) = [#] (((TOP-REAL 2) | Q) | SEG) .= SEG by PRE_TOPC:def_5 ; A20: rng gg c= SEG proof let ii be set ; :: according to TARSKI:def_3 ::_thesis: ( not ii in rng gg or ii in SEG ) assume ii in rng gg ; ::_thesis: ii in SEG then consider j being set such that A21: j in dom gg and A22: ii = gg . j by FUNCT_1:def_3; j in (dom F) /\ Poz by A18, A21, RELAT_1:61; then j in dom F by XBOOLE_0:def_4; then F . j in LSeg (f,i) by A13, A14, A21, FUNCT_1:def_6; hence ii in SEG by A14, A18, A21, A22, FUNCT_1:49; ::_thesis: verum end; reconsider SEG = SEG as non empty Subset of ((TOP-REAL 2) | Q) ; A23: ((TOP-REAL 2) | Q) | SEG = (TOP-REAL 2) | R by A9, GOBOARD9:2; reconsider hh9 = gg as Function of (I[01] | Poz),(((TOP-REAL 2) | Q) | SEG) by A19, A20, FUNCT_2:6; A24: F is continuous by A2, TOPS_2:def_5; A25: F is one-to-one by A2, TOPS_2:def_5; gg is continuous by A18, A24, TOPMETR:7; then A26: hh9 is continuous by TOPMETR:6; A27: hh9 is one-to-one by A25, FUNCT_1:52; reconsider hh = hh9 as Function of (I[01] | Poz),((TOP-REAL 2) | R) by A9, GOBOARD9:2; A28: dom hh = [#] (I[01] | Poz) by FUNCT_2:def_1; then A29: dom hh = Poz by PRE_TOPC:def_5; A30: rng hh = hh .: (dom hh) by A28, RELSET_1:22 .= [#] (((TOP-REAL 2) | Q) | SEG) by A7, A13, A15, A16, A19, A29, BORSUK_1:40, FUNCT_1:87, RELAT_1:129 ; reconsider A = Closed-Interval-TSpace (ppi,pi1) as strict SubSpace of I[01] by A10, A11, A12, TOPMETR:20, TREAL_1:3; A31: Poz = [#] A by A10, TOPMETR:18; Closed-Interval-TSpace (ppi,pi1) is compact by A10, HEINE:4; then [#] (Closed-Interval-TSpace (ppi,pi1)) is compact by COMPTS_1:1; then for P being Subset of A st P = Poz holds P is compact by A10, TOPMETR:18; then Poz is compact by A31, COMPTS_1:2; then A32: I[01] | Poz is compact by COMPTS_1:3; (TOP-REAL 2) | R is T_2 by TOPMETR:2; hence ex G being Function of (I[01] | P),((TOP-REAL 2) | R) st ( G = F | P & G is being_homeomorphism ) by A18, A23, A26, A27, A28, A30, A32, COMPTS_1:17; ::_thesis: verum end; begin theorem Th9: :: JORDAN5B:9 for p1, p2, p being Point of (TOP-REAL 2) st p1 <> p2 & p in LSeg (p1,p2) holds LE p,p,p1,p2 proof let p1, p2, p be Point of (TOP-REAL 2); ::_thesis: ( p1 <> p2 & p in LSeg (p1,p2) implies LE p,p,p1,p2 ) assume that A1: p1 <> p2 and A2: p in LSeg (p1,p2) ; ::_thesis: LE p,p,p1,p2 thus LE p,p,p1,p2 ::_thesis: verum proof thus ( p in LSeg (p1,p2) & p in LSeg (p1,p2) ) by A2; :: according to JORDAN3:def_5 ::_thesis: for b1, b2 being Element of REAL holds ( not 0 <= b1 or not b1 <= 1 or not p = ((1 - b1) * p1) + (b1 * p2) or not 0 <= b2 or not b2 <= 1 or not p = ((1 - b2) * p1) + (b2 * p2) or b1 <= b2 ) let r1, r2 be Real; ::_thesis: ( not 0 <= r1 or not r1 <= 1 or not p = ((1 - r1) * p1) + (r1 * p2) or not 0 <= r2 or not r2 <= 1 or not p = ((1 - r2) * p1) + (r2 * p2) or r1 <= r2 ) assume that 0 <= r1 and r1 <= 1 and A3: p = ((1 - r1) * p1) + (r1 * p2) and 0 <= r2 and r2 <= 1 and A4: p = ((1 - r2) * p1) + (r2 * p2) ; ::_thesis: r1 <= r2 thus r1 <= r2 by A1, A3, A4, JORDAN5A:2; ::_thesis: verum end; end; theorem Th10: :: JORDAN5B:10 for p, p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p in LSeg (p1,p2) holds LE p1,p,p1,p2 proof let p, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 <> p2 & p in LSeg (p1,p2) implies LE p1,p,p1,p2 ) assume that A1: p1 <> p2 and A2: p in LSeg (p1,p2) ; ::_thesis: LE p1,p,p1,p2 thus LE p1,p,p1,p2 ::_thesis: verum proof thus ( p1 in LSeg (p1,p2) & p in LSeg (p1,p2) ) by A2, RLTOPSP1:68; :: according to JORDAN3:def_5 ::_thesis: for b1, b2 being Element of REAL holds ( not 0 <= b1 or not b1 <= 1 or not p1 = ((1 - b1) * p1) + (b1 * p2) or not 0 <= b2 or not b2 <= 1 or not p = ((1 - b2) * p1) + (b2 * p2) or b1 <= b2 ) let r1, r2 be Real; ::_thesis: ( not 0 <= r1 or not r1 <= 1 or not p1 = ((1 - r1) * p1) + (r1 * p2) or not 0 <= r2 or not r2 <= 1 or not p = ((1 - r2) * p1) + (r2 * p2) or r1 <= r2 ) assume that 0 <= r1 and r1 <= 1 and A3: p1 = ((1 - r1) * p1) + (r1 * p2) and A4: 0 <= r2 and r2 <= 1 and p = ((1 - r2) * p1) + (r2 * p2) ; ::_thesis: r1 <= r2 0. (TOP-REAL 2) = (((1 - r1) * p1) + (r1 * p2)) + (- p1) by A3, EUCLID:36 .= (((1 - r1) * p1) + (r1 * p2)) - p1 by EUCLID:41 .= ((1 - r1) * p1) + ((r1 * p2) - p1) by EUCLID:45 .= ((1 - r1) * p1) + ((- p1) + (r1 * p2)) by EUCLID:41 .= (((1 - r1) * p1) + (- p1)) + (r1 * p2) by EUCLID:26 .= (((1 - r1) * p1) - p1) + (r1 * p2) by EUCLID:41 ; then - (r1 * p2) = ((((1 - r1) * p1) - p1) + (r1 * p2)) + (- (r1 * p2)) by EUCLID:27 .= ((((1 - r1) * p1) - p1) + (r1 * p2)) - (r1 * p2) by EUCLID:41 .= (((1 - r1) * p1) - p1) + ((r1 * p2) - (r1 * p2)) by EUCLID:45 .= (((1 - r1) * p1) - p1) + (0. (TOP-REAL 2)) by EUCLID:42 .= ((1 - r1) * p1) - p1 by EUCLID:27 .= ((1 - r1) * p1) - (1 * p1) by EUCLID:29 .= ((1 - r1) - 1) * p1 by EUCLID:50 .= (- r1) * p1 .= - (r1 * p1) by EUCLID:40 ; then r1 * p1 = - (- (r1 * p2)) .= r1 * p2 ; hence r1 <= r2 by A1, A4, EUCLID:34; ::_thesis: verum end; end; theorem Th11: :: JORDAN5B:11 for p, p1, p2 being Point of (TOP-REAL 2) st p in LSeg (p1,p2) & p1 <> p2 holds LE p,p2,p1,p2 proof let p, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p in LSeg (p1,p2) & p1 <> p2 implies LE p,p2,p1,p2 ) assume that A1: p in LSeg (p1,p2) and A2: p1 <> p2 ; ::_thesis: LE p,p2,p1,p2 thus LE p,p2,p1,p2 ::_thesis: verum proof thus ( p in LSeg (p1,p2) & p2 in LSeg (p1,p2) ) by A1, RLTOPSP1:68; :: according to JORDAN3:def_5 ::_thesis: for b1, b2 being Element of REAL holds ( not 0 <= b1 or not b1 <= 1 or not p = ((1 - b1) * p1) + (b1 * p2) or not 0 <= b2 or not b2 <= 1 or not p2 = ((1 - b2) * p1) + (b2 * p2) or b1 <= b2 ) let r1, r2 be Real; ::_thesis: ( not 0 <= r1 or not r1 <= 1 or not p = ((1 - r1) * p1) + (r1 * p2) or not 0 <= r2 or not r2 <= 1 or not p2 = ((1 - r2) * p1) + (r2 * p2) or r1 <= r2 ) assume that 0 <= r1 and A3: r1 <= 1 and p = ((1 - r1) * p1) + (r1 * p2) and 0 <= r2 and r2 <= 1 and A4: p2 = ((1 - r2) * p1) + (r2 * p2) ; ::_thesis: r1 <= r2 p2 = 1 * p2 by EUCLID:29 .= (0. (TOP-REAL 2)) + (1 * p2) by EUCLID:27 .= ((1 - 1) * p1) + (1 * p2) by EUCLID:29 ; hence r1 <= r2 by A2, A3, A4, JORDAN5A:2; ::_thesis: verum end; end; theorem :: JORDAN5B:12 for p1, p2, q1, q2, q3 being Point of (TOP-REAL 2) st p1 <> p2 & LE q1,q2,p1,p2 & LE q2,q3,p1,p2 holds LE q1,q3,p1,p2 proof let p1, p2, q1, q2, q3 be Point of (TOP-REAL 2); ::_thesis: ( p1 <> p2 & LE q1,q2,p1,p2 & LE q2,q3,p1,p2 implies LE q1,q3,p1,p2 ) assume that A1: p1 <> p2 and A2: LE q1,q2,p1,p2 and A3: LE q2,q3,p1,p2 ; ::_thesis: LE q1,q3,p1,p2 A4: q1 in LSeg (p1,p2) by A2, JORDAN3:def_5; A5: q2 in LSeg (p1,p2) by A2, JORDAN3:def_5; A6: q3 in LSeg (p1,p2) by A3, JORDAN3:def_5; consider s1 being Real such that A7: q1 = ((1 - s1) * p1) + (s1 * p2) and 0 <= s1 and A8: s1 <= 1 by A4; consider s2 being Real such that A9: q2 = ((1 - s2) * p1) + (s2 * p2) and A10: 0 <= s2 and A11: s2 <= 1 by A5; A12: s1 <= s2 by A2, A7, A8, A9, A10, A11, JORDAN3:def_5; consider s3 being Real such that A13: q3 = ((1 - s3) * p1) + (s3 * p2) and A14: 0 <= s3 and A15: s3 <= 1 by A6; s2 <= s3 by A3, A9, A11, A13, A14, A15, JORDAN3:def_5; then A16: s1 <= s3 by A12, XXREAL_0:2; thus LE q1,q3,p1,p2 ::_thesis: verum proof thus ( q1 in LSeg (p1,p2) & q3 in LSeg (p1,p2) ) by A2, A3, JORDAN3:def_5; :: according to JORDAN3:def_5 ::_thesis: for b1, b2 being Element of REAL holds ( not 0 <= b1 or not b1 <= 1 or not q1 = ((1 - b1) * p1) + (b1 * p2) or not 0 <= b2 or not b2 <= 1 or not q3 = ((1 - b2) * p1) + (b2 * p2) or b1 <= b2 ) let r1, r2 be Real; ::_thesis: ( not 0 <= r1 or not r1 <= 1 or not q1 = ((1 - r1) * p1) + (r1 * p2) or not 0 <= r2 or not r2 <= 1 or not q3 = ((1 - r2) * p1) + (r2 * p2) or r1 <= r2 ) assume that 0 <= r1 and r1 <= 1 and A17: q1 = ((1 - r1) * p1) + (r1 * p2) and 0 <= r2 and r2 <= 1 and A18: q3 = ((1 - r2) * p1) + (r2 * p2) ; ::_thesis: r1 <= r2 s1 = r1 by A1, A7, A17, JORDAN5A:2; hence r1 <= r2 by A1, A13, A16, A18, JORDAN5A:2; ::_thesis: verum end; end; theorem :: JORDAN5B:13 for p, q being Point of (TOP-REAL 2) st p <> q holds LSeg (p,q) = { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } proof let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q implies LSeg (p,q) = { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } ) assume A1: p <> q ; ::_thesis: LSeg (p,q) = { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } thus LSeg (p,q) c= { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } :: according to XBOOLE_0:def_10 ::_thesis: { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } c= LSeg (p,q) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg (p,q) or a in { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } ) assume A2: a in LSeg (p,q) ; ::_thesis: a in { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } then reconsider a9 = a as Point of (TOP-REAL 2) ; A3: LE p,a9,p,q by A1, A2, Th10; LE a9,q,p,q by A1, A2, Th11; hence a in { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } by A3; ::_thesis: verum end; thus { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } c= LSeg (p,q) ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } or a in LSeg (p,q) ) assume a in { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) } ; ::_thesis: a in LSeg (p,q) then ex a9 being Point of (TOP-REAL 2) st ( a9 = a & LE p,a9,p,q & LE a9,q,p,q ) ; hence a in LSeg (p,q) by JORDAN3:30; ::_thesis: verum end; end; theorem :: JORDAN5B:14 for n being Element of NAT for P being Subset of (TOP-REAL n) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds P is_an_arc_of p2,p1 proof let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds P is_an_arc_of p2,p1 let P be Subset of (TOP-REAL n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds P is_an_arc_of p2,p1 let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 implies P is_an_arc_of p2,p1 ) assume A1: P is_an_arc_of p1,p2 ; ::_thesis: P is_an_arc_of p2,p1 then consider f being Function of I[01],((TOP-REAL n) | P) such that A2: f is being_homeomorphism and A3: f . 0 = p1 and A4: f . 1 = p2 by TOPREAL1:def_1; set Ex = L[01] (((0,1) (#)),((#) (0,1))); A5: L[01] (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18; set g = f * (L[01] (((0,1) (#)),((#) (0,1)))); A6: (L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by BORSUK_1:def_14, TREAL_1:5, TREAL_1:9; A7: (L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by BORSUK_1:def_15, TREAL_1:5, TREAL_1:9; dom f = [#] I[01] by A2, TOPS_2:def_5; then rng (L[01] (((0,1) (#)),((#) (0,1)))) = dom f by A5, TOPMETR:20, TOPS_2:def_5; then A8: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = dom (L[01] (((0,1) (#)),((#) (0,1)))) by RELAT_1:27; reconsider P = P as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:1; A9: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = [#] I[01] by A5, A8, TOPMETR:20, TOPS_2:def_5; reconsider g = f * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],((TOP-REAL n) | P) by TOPMETR:20; A10: g is being_homeomorphism by A2, A5, TOPMETR:20, TOPS_2:57; A11: g . 0 = p2 by A4, A7, A9, BORSUK_1:def_14, FUNCT_1:12, TREAL_1:5; g . 1 = p1 by A3, A6, A9, BORSUK_1:def_15, FUNCT_1:12, TREAL_1:5; hence P is_an_arc_of p2,p1 by A10, A11, TOPREAL1:def_1; ::_thesis: verum end; theorem :: JORDAN5B:15 for i being Element of NAT for f being FinSequence of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) st f is being_S-Seq & 1 <= i & i + 1 <= len f & P = LSeg (f,i) holds P is_an_arc_of f /. i,f /. (i + 1) proof let i be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) st f is being_S-Seq & 1 <= i & i + 1 <= len f & P = LSeg (f,i) holds P is_an_arc_of f /. i,f /. (i + 1) let f be FinSequence of (TOP-REAL 2); ::_thesis: for P being Subset of (TOP-REAL 2) st f is being_S-Seq & 1 <= i & i + 1 <= len f & P = LSeg (f,i) holds P is_an_arc_of f /. i,f /. (i + 1) let P be Subset of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq & 1 <= i & i + 1 <= len f & P = LSeg (f,i) implies P is_an_arc_of f /. i,f /. (i + 1) ) assume that A1: f is being_S-Seq and A2: 1 <= i and A3: i + 1 <= len f and A4: P = LSeg (f,i) ; ::_thesis: P is_an_arc_of f /. i,f /. (i + 1) A5: i in dom f by A2, A3, SEQ_4:134; A6: i + 1 in dom f by A2, A3, SEQ_4:134; A7: f is one-to-one by A1; A8: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A2, A3, TOPREAL1:def_3; f /. i <> f /. (i + 1) proof assume f /. i = f /. (i + 1) ; ::_thesis: contradiction then i = i + 1 by A5, A6, A7, PARTFUN2:10; hence contradiction ; ::_thesis: verum end; hence P is_an_arc_of f /. i,f /. (i + 1) by A4, A8, TOPREAL1:9; ::_thesis: verum end; begin theorem :: JORDAN5B:16 for g1 being FinSequence of (TOP-REAL 2) for i being Element of NAT st 1 <= i & i <= len g1 & g1 is being_S-Seq & g1 /. 1 in L~ (mid (g1,i,(len g1))) holds i = 1 proof let g1 be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st 1 <= i & i <= len g1 & g1 is being_S-Seq & g1 /. 1 in L~ (mid (g1,i,(len g1))) holds i = 1 let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len g1 & g1 is being_S-Seq & g1 /. 1 in L~ (mid (g1,i,(len g1))) implies i = 1 ) assume that A1: 1 <= i and A2: i <= len g1 and A3: g1 is being_S-Seq ; ::_thesis: ( not g1 /. 1 in L~ (mid (g1,i,(len g1))) or i = 1 ) assume g1 /. 1 in L~ (mid (g1,i,(len g1))) ; ::_thesis: i = 1 then consider j being Element of NAT such that A4: 1 <= j and A5: j + 1 <= len (mid (g1,i,(len g1))) and A6: g1 /. 1 in LSeg ((mid (g1,i,(len g1))),j) by SPPOL_2:13; A7: j + 1 in dom (mid (g1,i,(len g1))) by A4, A5, SEQ_4:134; A8: mid (g1,i,(len g1)) = g1 /^ (i -' 1) by A2, FINSEQ_6:117; j <= j + 1 by NAT_1:11; then A9: j <= len (g1 /^ (i -' 1)) by A5, A8, XXREAL_0:2; then A10: j in dom (g1 /^ (i -' 1)) by A4, FINSEQ_3:25; i -' 1 <= i by A1, Th1; then A11: i -' 1 <= len g1 by A2, XXREAL_0:2; then A12: j <= (len g1) - (i -' 1) by A9, RFINSEQ:def_1; j <= (i -' 1) + j by NAT_1:11; then A13: 1 <= (i -' 1) + j by A4, XXREAL_0:2; A14: j + (i -' 1) <= len g1 by A12, XREAL_1:19; then A15: (i -' 1) + j in dom g1 by A13, FINSEQ_3:25; A16: (g1 /^ (i -' 1)) /. j = (g1 /^ (i -' 1)) . j by A10, PARTFUN1:def_6 .= g1 . ((i -' 1) + j) by A4, A14, FINSEQ_6:114 .= g1 /. ((i -' 1) + j) by A15, PARTFUN1:def_6 ; A17: 1 <= j + 1 by NAT_1:11; j + 1 <= (i -' 1) + (j + 1) by NAT_1:11; then A18: 1 <= (i -' 1) + (j + 1) by A17, XXREAL_0:2; j + 1 <= len (g1 /^ (i -' 1)) by A2, A5, FINSEQ_6:117; then A19: j + 1 <= (len g1) - (i -' 1) by A11, RFINSEQ:def_1; A20: 1 <= j + 1 by A7, FINSEQ_3:25; A21: (j + 1) + (i -' 1) <= len g1 by A19, XREAL_1:19; then A22: (i -' 1) + (j + 1) in dom g1 by A18, FINSEQ_3:25; j + 1 in dom (g1 /^ (i -' 1)) by A2, A7, FINSEQ_6:117; then A23: (g1 /^ (i -' 1)) /. (j + 1) = (g1 /^ (i -' 1)) . (j + 1) by PARTFUN1:def_6 .= g1 . ((i -' 1) + (j + 1)) by A20, A21, FINSEQ_6:114 .= g1 /. ((i -' 1) + (j + 1)) by A22, PARTFUN1:def_6 ; A24: ((i -' 1) + j) + 1 = (i -' 1) + (j + 1) ; A25: ((i -' 1) + j) + 1 <= len g1 by A21; A26: LSeg ((mid (g1,i,(len g1))),j) = LSeg ((g1 /. ((i -' 1) + j)),(g1 /. ((i -' 1) + (j + 1)))) by A4, A5, A8, A16, A23, TOPREAL1:def_3 .= LSeg (g1,((i -' 1) + j)) by A13, A21, A24, TOPREAL1:def_3 ; A27: 1 + 1 <= len g1 by A3, TOPREAL1:def_8; then g1 /. 1 in LSeg (g1,1) by TOPREAL1:21; then A28: g1 /. 1 in (LSeg (g1,1)) /\ (LSeg (g1,((i -' 1) + j))) by A6, A26, XBOOLE_0:def_4; then A29: LSeg (g1,1) meets LSeg (g1,((i -' 1) + j)) by XBOOLE_0:4; assume i <> 1 ; ::_thesis: contradiction then 1 < i by A1, XXREAL_0:1; then 1 + 1 <= i by NAT_1:13; then 2 -' 1 <= i -' 1 by NAT_D:42; then (2 -' 1) + 1 <= (i -' 1) + j by A4, XREAL_1:7; then A30: (i -' 1) + j >= 2 by XREAL_1:235; A31: ( g1 is s.n.c. & g1 is unfolded & g1 is one-to-one ) by A3; A32: 1 in dom g1 by A27, SEQ_4:134; A33: 1 + 1 in dom g1 by A27, SEQ_4:134; percases ( (i -' 1) + j = 2 or (i -' 1) + j > 2 ) by A30, XXREAL_0:1; suppose (i -' 1) + j = 2 ; ::_thesis: contradiction then g1 /. 1 in {(g1 /. (1 + 1))} by A25, A28, A31, TOPREAL1:def_6; then g1 /. 1 = g1 /. (1 + 1) by TARSKI:def_1; hence contradiction by A31, A32, A33, PARTFUN2:10; ::_thesis: verum end; suppose (i -' 1) + j > 2 ; ::_thesis: contradiction then (i -' 1) + j > 1 + 1 ; hence contradiction by A29, A31, TOPREAL1:def_7; ::_thesis: verum end; end; end; theorem :: JORDAN5B:17 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is being_S-Seq & p = f . (len f) holds L_Cut (f,p) = <*p*> proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is being_S-Seq & p = f . (len f) holds L_Cut (f,p) = <*p*> let p be Point of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq & p = f . (len f) implies L_Cut (f,p) = <*p*> ) assume that A1: f is being_S-Seq and A2: p = f . (len f) ; ::_thesis: L_Cut (f,p) = <*p*> len f >= 2 by A1, TOPREAL1:def_8; then p in L~ f by A2, JORDAN3:1; then A3: p in L~ (Rev f) by SPPOL_2:22; A4: L_Cut (f,p) = L_Cut ((Rev (Rev f)),p) .= Rev (R_Cut ((Rev f),p)) by A1, A3, JORDAN3:22 ; p = (Rev f) . 1 by A2, FINSEQ_5:62; then R_Cut ((Rev f),p) = <*p*> by JORDAN3:def_4; hence L_Cut (f,p) = <*p*> by A4, FINSEQ_5:60; ::_thesis: verum end; theorem :: JORDAN5B:18 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f & p <> f . (len f) & f is being_S-Seq holds Index (p,(L_Cut (f,p))) = 1 proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f & p <> f . (len f) & f is being_S-Seq holds Index (p,(L_Cut (f,p))) = 1 let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & p <> f . (len f) & f is being_S-Seq implies Index (p,(L_Cut (f,p))) = 1 ) assume that A1: p in L~ f and A2: p <> f . (len f) and A3: f is being_S-Seq ; ::_thesis: Index (p,(L_Cut (f,p))) = 1 L_Cut (f,p) is being_S-Seq by A1, A2, A3, JORDAN3:34; then A4: 2 <= len (L_Cut (f,p)) by TOPREAL1:def_8; then 1 <= len (L_Cut (f,p)) by XXREAL_0:2; then 1 in dom (L_Cut (f,p)) by FINSEQ_3:25; then (L_Cut (f,p)) /. 1 = (L_Cut (f,p)) . 1 by PARTFUN1:def_6 .= p by A1, JORDAN3:23 ; hence Index (p,(L_Cut (f,p))) = 1 by A4, JORDAN3:11; ::_thesis: verum end; theorem Th19: :: JORDAN5B:19 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f & f is being_S-Seq & p <> f . (len f) holds p in L~ (L_Cut (f,p)) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f & f is being_S-Seq & p <> f . (len f) holds p in L~ (L_Cut (f,p)) let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & f is being_S-Seq & p <> f . (len f) implies p in L~ (L_Cut (f,p)) ) assume that A1: p in L~ f and A2: f is being_S-Seq ; ::_thesis: ( not p <> f . (len f) or p in L~ (L_Cut (f,p)) ) assume p <> f . (len f) ; ::_thesis: p in L~ (L_Cut (f,p)) then L_Cut (f,p) is being_S-Seq by A1, A2, JORDAN3:34; then A3: len (L_Cut (f,p)) >= 2 by TOPREAL1:def_8; (L_Cut (f,p)) . 1 = p by A1, JORDAN3:23; hence p in L~ (L_Cut (f,p)) by A3, JORDAN3:1; ::_thesis: verum end; theorem :: JORDAN5B:20 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f & f is being_S-Seq & p <> f . 1 holds p in L~ (R_Cut (f,p)) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f & f is being_S-Seq & p <> f . 1 holds p in L~ (R_Cut (f,p)) let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & f is being_S-Seq & p <> f . 1 implies p in L~ (R_Cut (f,p)) ) assume that A1: p in L~ f and A2: f is being_S-Seq ; ::_thesis: ( not p <> f . 1 or p in L~ (R_Cut (f,p)) ) assume p <> f . 1 ; ::_thesis: p in L~ (R_Cut (f,p)) then R_Cut (f,p) is being_S-Seq by A1, A2, JORDAN3:35; then A3: len (R_Cut (f,p)) >= 2 by TOPREAL1:def_8; (R_Cut (f,p)) . (len (R_Cut (f,p))) = p by A1, JORDAN3:24; hence p in L~ (R_Cut (f,p)) by A3, JORDAN3:1; ::_thesis: verum end; theorem Th21: :: JORDAN5B:21 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f & f is one-to-one holds B_Cut (f,p,p) = <*p*> proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f & f is one-to-one holds B_Cut (f,p,p) = <*p*> let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & f is one-to-one implies B_Cut (f,p,p) = <*p*> ) assume that A1: p in L~ f and A2: f is one-to-one ; ::_thesis: B_Cut (f,p,p) = <*p*> A3: Index (p,f) <> (Index (p,f)) + 1 ; A4: Index (p,f) < len f by A1, JORDAN3:8; A5: 1 <= Index (p,f) by A1, JORDAN3:8; A6: (Index (p,f)) + 1 <= len f by A4, NAT_1:13; then A7: Index (p,f) in dom f by A5, SEQ_4:134; A8: (Index (p,f)) + 1 in dom f by A5, A6, SEQ_4:134; p in LSeg (f,(Index (p,f))) by A1, JORDAN3:9; then p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A5, A6, TOPREAL1:def_3; then A9: LE p,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A2, A3, A7, A8, Th9, PARTFUN2:10; (L_Cut (f,p)) . 1 = p by A1, JORDAN3:23; then R_Cut ((L_Cut (f,p)),p) = <*p*> by JORDAN3:def_4; hence B_Cut (f,p,p) = <*p*> by A9, JORDAN3:def_7; ::_thesis: verum end; Lm3: for f being FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & p <> f . (len f) & f is being_S-Seq & not p in L~ (L_Cut (f,q)) holds q in L~ (L_Cut (f,p)) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & p <> f . (len f) & f is being_S-Seq & not p in L~ (L_Cut (f,q)) holds q in L~ (L_Cut (f,p)) let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & q in L~ f & p <> f . (len f) & f is being_S-Seq & not p in L~ (L_Cut (f,q)) implies q in L~ (L_Cut (f,p)) ) assume that A1: p in L~ f and A2: q in L~ f and A3: p <> f . (len f) and A4: f is being_S-Seq ; ::_thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) A5: Index (p,f) < len f by A1, JORDAN3:8; A6: 1 <= Index (p,f) by A1, JORDAN3:8; A7: (Index (p,f)) + 1 <= len f by A5, NAT_1:13; then A8: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A6, TOPREAL1:def_3; A9: Index (p,f) in dom f by A6, A7, SEQ_4:134; A10: (Index (p,f)) + 1 in dom f by A6, A7, SEQ_4:134; A11: f is one-to-one by A4; Index (p,f) < (Index (p,f)) + 1 by NAT_1:13; then A12: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A9, A10, A11, PARTFUN2:10; percases ( Index (p,f) < Index (q,f) or Index (p,f) = Index (q,f) or Index (p,f) > Index (q,f) ) by XXREAL_0:1; suppose Index (p,f) < Index (q,f) ; ::_thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A1, A2, JORDAN3:29; ::_thesis: verum end; supposeA13: Index (p,f) = Index (q,f) ; ::_thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) A14: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A1, A8, JORDAN3:9; q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, A8, A13, JORDAN3:9; then A15: ( LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) or LT q,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) by A12, A14, JORDAN3:28; now__::_thesis:_(_p_in_L~_(L_Cut_(f,q))_or_q_in_L~_(L_Cut_(f,p))_) percases ( LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) or LE q,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) by A15, JORDAN3:def_6; supposeA16: LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ; ::_thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) thus ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) ::_thesis: verum proof percases ( p <> q or p = q ) ; suppose p <> q ; ::_thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A1, A2, A13, A16, JORDAN3:31; ::_thesis: verum end; suppose p = q ; ::_thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A1, A3, A4, Th19; ::_thesis: verum end; end; end; end; supposeA17: LE q,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ; ::_thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) thus ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) ::_thesis: verum proof percases ( p <> q or p = q ) ; suppose p <> q ; ::_thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A1, A2, A13, A17, JORDAN3:31; ::_thesis: verum end; suppose p = q ; ::_thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A1, A3, A4, Th19; ::_thesis: verum end; end; end; end; end; end; hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) ; ::_thesis: verum end; suppose Index (p,f) > Index (q,f) ; ::_thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A1, A2, JORDAN3:29; ::_thesis: verum end; end; end; theorem Th22: :: JORDAN5B:22 for f being FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & q <> f . (len f) & p = f . (len f) & f is being_S-Seq holds p in L~ (L_Cut (f,q)) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & q <> f . (len f) & p = f . (len f) & f is being_S-Seq holds p in L~ (L_Cut (f,q)) let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & q in L~ f & q <> f . (len f) & p = f . (len f) & f is being_S-Seq implies p in L~ (L_Cut (f,q)) ) assume that A1: p in L~ f and A2: q in L~ f and A3: q <> f . (len f) and A4: p = f . (len f) and A5: f is being_S-Seq ; ::_thesis: p in L~ (L_Cut (f,q)) 1 + 1 <= len f by A5, TOPREAL1:def_8; then A6: 1 < len f by XXREAL_0:2; then A7: (Index (p,f)) + 1 = len f by A4, A5, JORDAN3:12; Index (q,f) < len f by A2, JORDAN3:8; then A8: Index (q,f) <= Index (p,f) by A7, NAT_1:13; percases ( Index (q,f) = Index (p,f) or Index (q,f) < Index (p,f) ) by A8, XXREAL_0:1; suppose Index (q,f) = Index (p,f) ; ::_thesis: p in L~ (L_Cut (f,q)) then A9: L_Cut (f,q) = <*q*> ^ (mid (f,(len f),(len f))) by A3, A7, JORDAN3:def_3 .= <*q*> ^ <*(f /. (len f))*> by A6, JORDAN4:15 .= <*q,(f /. (len f))*> by FINSEQ_1:def_9 .= <*q,p*> by A4, A6, FINSEQ_4:15 ; then rng (L_Cut (f,q)) = {p,q} by FINSEQ_2:127; then A10: p in rng (L_Cut (f,q)) by TARSKI:def_2; len (L_Cut (f,q)) = 2 by A9, FINSEQ_1:44; then rng (L_Cut (f,q)) c= L~ (L_Cut (f,q)) by SPPOL_2:18; hence p in L~ (L_Cut (f,q)) by A10; ::_thesis: verum end; suppose Index (q,f) < Index (p,f) ; ::_thesis: p in L~ (L_Cut (f,q)) hence p in L~ (L_Cut (f,q)) by A1, A2, JORDAN3:29; ::_thesis: verum end; end; end; theorem :: JORDAN5B:23 for f being FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st p <> f . (len f) & p in L~ f & q in L~ f & f is being_S-Seq & not p in L~ (L_Cut (f,q)) holds q in L~ (L_Cut (f,p)) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st p <> f . (len f) & p in L~ f & q in L~ f & f is being_S-Seq & not p in L~ (L_Cut (f,q)) holds q in L~ (L_Cut (f,p)) let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> f . (len f) & p in L~ f & q in L~ f & f is being_S-Seq & not p in L~ (L_Cut (f,q)) implies q in L~ (L_Cut (f,p)) ) assume A1: p <> f . (len f) ; ::_thesis: ( not p in L~ f or not q in L~ f or not f is being_S-Seq or p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) assume that A2: p in L~ f and A3: q in L~ f and A4: f is being_S-Seq ; ::_thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) percases ( ( p <> f . (len f) & q = f . (len f) ) or ( p = f . (len f) & q <> f . (len f) ) or ( p <> f . (len f) & q <> f . (len f) ) ) by A1; suppose ( p <> f . (len f) & q = f . (len f) ) ; ::_thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A2, A3, A4, Th22; ::_thesis: verum end; suppose ( p = f . (len f) & q <> f . (len f) ) ; ::_thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A2, A3, A4, Th22; ::_thesis: verum end; suppose ( p <> f . (len f) & q <> f . (len f) ) ; ::_thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A2, A3, A4, Lm3; ::_thesis: verum end; end; end; Lm4: for f being FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) & p <> q holds L~ (B_Cut (f,p,q)) c= L~ f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) & p <> q holds L~ (B_Cut (f,p,q)) c= L~ f let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & q in L~ f & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) & p <> q implies L~ (B_Cut (f,p,q)) c= L~ f ) assume that A1: p in L~ f and A2: q in L~ f and A3: ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) and A4: p <> q ; ::_thesis: L~ (B_Cut (f,p,q)) c= L~ f A5: B_Cut (f,p,q) = R_Cut ((L_Cut (f,p)),q) by A1, A2, A3, JORDAN3:def_7; now__::_thesis:_(_(_Index_(p,f)_<_Index_(q,f)_&_ex_i1_being_Element_of_NAT_st_ (_1_<=_i1_&_i1_+_1_<=_len_(L_Cut_(f,p))_&_q_in_LSeg_((L_Cut_(f,p)),i1)_)_)_or_(_Index_(p,f)_=_Index_(q,f)_&_LE_p,q,f_/._(Index_(p,f)),f_/._((Index_(p,f))_+_1)_&_ex_i1_being_Element_of_NAT_st_ (_1_<=_i1_&_i1_+_1_<=_len_(L_Cut_(f,p))_&_q_in_LSeg_((L_Cut_(f,p)),i1)_)_)_) percases ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) by A3; case Index (p,f) < Index (q,f) ; ::_thesis: ex i1 being Element of NAT st ( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) ) then q in L~ (L_Cut (f,p)) by A1, A2, JORDAN3:29; hence ex i1 being Element of NAT st ( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) ) by SPPOL_2:13; ::_thesis: verum end; case ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ; ::_thesis: ex i1 being Element of NAT st ( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) ) then q in L~ (L_Cut (f,p)) by A1, A2, A4, JORDAN3:31; hence ex i1 being Element of NAT st ( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) ) by SPPOL_2:13; ::_thesis: verum end; end; end; then A6: L~ (B_Cut (f,p,q)) c= L~ (L_Cut (f,p)) by A5, JORDAN3:41, SPPOL_2:17; L~ (L_Cut (f,p)) c= L~ f by A1, JORDAN3:42; hence L~ (B_Cut (f,p,q)) c= L~ f by A6, XBOOLE_1:1; ::_thesis: verum end; theorem :: JORDAN5B:24 for f being FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & f is being_S-Seq holds L~ (B_Cut (f,p,q)) c= L~ f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & f is being_S-Seq holds L~ (B_Cut (f,p,q)) c= L~ f let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & q in L~ f & f is being_S-Seq implies L~ (B_Cut (f,p,q)) c= L~ f ) assume that A1: p in L~ f and A2: q in L~ f and A3: f is being_S-Seq ; ::_thesis: L~ (B_Cut (f,p,q)) c= L~ f A4: f is one-to-one by A3; percases ( p = q or ( p <> q & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) or ( p <> q & not Index (p,f) < Index (q,f) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) ; suppose p = q ; ::_thesis: L~ (B_Cut (f,p,q)) c= L~ f then B_Cut (f,p,q) = <*p*> by A1, A4, Th21; then len (B_Cut (f,p,q)) = 1 by FINSEQ_1:39; then L~ (B_Cut (f,p,q)) = {} by TOPREAL1:22; hence L~ (B_Cut (f,p,q)) c= L~ f by XBOOLE_1:2; ::_thesis: verum end; suppose ( p <> q & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) ; ::_thesis: L~ (B_Cut (f,p,q)) c= L~ f hence L~ (B_Cut (f,p,q)) c= L~ f by A1, A2, Lm4; ::_thesis: verum end; supposethat A5: p <> q and A6: ( not Index (p,f) < Index (q,f) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; ::_thesis: L~ (B_Cut (f,p,q)) c= L~ f A7: B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) by A6, JORDAN3:def_7; A8: ( Index (q,f) < Index (p,f) or ( Index (p,f) = Index (q,f) & not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) by A6, XXREAL_0:1; A9: now__::_thesis:_(_Index_(p,f)_=_Index_(q,f)_&_not_LE_p,q,f_/._(Index_(p,f)),f_/._((Index_(p,f))_+_1)_implies_LE_q,p,f_/._(Index_(q,f)),f_/._((Index_(q,f))_+_1)_) assume that A10: Index (p,f) = Index (q,f) and A11: not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ; ::_thesis: LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) A12: 1 <= Index (p,f) by A1, JORDAN3:8; A13: Index (p,f) < len f by A1, JORDAN3:8; then A14: (Index (p,f)) + 1 <= len f by NAT_1:13; then A15: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A12, TOPREAL1:def_3; then A16: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A1, JORDAN3:9; A17: q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, A10, A15, JORDAN3:9; A18: Index (p,f) in dom f by A12, A13, FINSEQ_3:25; 1 <= (Index (p,f)) + 1 by NAT_1:11; then A19: (Index (p,f)) + 1 in dom f by A14, FINSEQ_3:25; (Index (p,f)) + 0 <> (Index (p,f)) + 1 ; then f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A4, A18, A19, PARTFUN2:10; then LT q,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A11, A16, A17, JORDAN3:28; hence LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) by A10, JORDAN3:def_6; ::_thesis: verum end; then A20: Rev (B_Cut (f,q,p)) = B_Cut (f,p,q) by A1, A2, A7, A8, JORDAN3:def_7; L~ (B_Cut (f,q,p)) c= L~ f by A1, A2, A5, A8, A9, Lm4; hence L~ (B_Cut (f,p,q)) c= L~ f by A20, SPPOL_2:22; ::_thesis: verum end; end; end; theorem :: JORDAN5B:25 for f being non constant standard special_circular_sequence for i, j being Element of NAT st 1 <= i & j <= len (GoB f) & i < j holds (LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f)))))) /\ (LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {} proof let f be non constant standard special_circular_sequence; ::_thesis: for i, j being Element of NAT st 1 <= i & j <= len (GoB f) & i < j holds (LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f)))))) /\ (LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {} let i, j be Element of NAT ; ::_thesis: ( 1 <= i & j <= len (GoB f) & i < j implies (LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f)))))) /\ (LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {} ) assume that A1: 1 <= i and A2: j <= len (GoB f) and A3: i < j ; ::_thesis: (LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f)))))) /\ (LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {} set A = LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f))))); set B = LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f))))); assume (LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f)))))) /\ (LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f)))))) <> {} ; ::_thesis: contradiction then LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f))))) meets LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f))))) by XBOOLE_0:def_7; then consider x being set such that A4: x in LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f))))) and A5: x in LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f))))) by XBOOLE_0:3; reconsider x1 = x as Point of (TOP-REAL 2) by A4; A6: 1 <= width (GoB f) by GOBOARD7:33; A7: i <= len (GoB f) by A2, A3, XXREAL_0:2; ((GoB f) * (1,(width (GoB f)))) `1 <= ((GoB f) * (i,(width (GoB f)))) `1 proof percases ( i = 1 or i > 1 ) by A1, XXREAL_0:1; suppose i = 1 ; ::_thesis: ((GoB f) * (1,(width (GoB f)))) `1 <= ((GoB f) * (i,(width (GoB f)))) `1 hence ((GoB f) * (1,(width (GoB f)))) `1 <= ((GoB f) * (i,(width (GoB f)))) `1 ; ::_thesis: verum end; suppose i > 1 ; ::_thesis: ((GoB f) * (1,(width (GoB f)))) `1 <= ((GoB f) * (i,(width (GoB f)))) `1 hence ((GoB f) * (1,(width (GoB f)))) `1 <= ((GoB f) * (i,(width (GoB f)))) `1 by A6, A7, GOBOARD5:3; ::_thesis: verum end; end; end; then A8: x1 `1 <= ((GoB f) * (i,(width (GoB f)))) `1 by A4, TOPREAL1:3; A9: ((GoB f) * (j,(width (GoB f)))) `1 > ((GoB f) * (i,(width (GoB f)))) `1 by A1, A2, A3, A6, GOBOARD5:3; A10: 1 <= j by A1, A3, XXREAL_0:2; ((GoB f) * (j,(width (GoB f)))) `1 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `1 proof percases ( j < len (GoB f) or j = len (GoB f) ) by A2, XXREAL_0:1; suppose j < len (GoB f) ; ::_thesis: ((GoB f) * (j,(width (GoB f)))) `1 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `1 hence ((GoB f) * (j,(width (GoB f)))) `1 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `1 by A6, A10, GOBOARD5:3; ::_thesis: verum end; suppose j = len (GoB f) ; ::_thesis: ((GoB f) * (j,(width (GoB f)))) `1 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `1 hence ((GoB f) * (j,(width (GoB f)))) `1 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `1 ; ::_thesis: verum end; end; end; then x1 `1 >= ((GoB f) * (j,(width (GoB f)))) `1 by A5, TOPREAL1:3; hence contradiction by A8, A9, XXREAL_0:2; ::_thesis: verum end; theorem :: JORDAN5B:26 for f being non constant standard special_circular_sequence for i, j being Element of NAT st 1 <= i & j <= width (GoB f) & i < j holds (LSeg (((GoB f) * ((len (GoB f)),1)),((GoB f) * ((len (GoB f)),i)))) /\ (LSeg (((GoB f) * ((len (GoB f)),j)),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {} proof let f be non constant standard special_circular_sequence; ::_thesis: for i, j being Element of NAT st 1 <= i & j <= width (GoB f) & i < j holds (LSeg (((GoB f) * ((len (GoB f)),1)),((GoB f) * ((len (GoB f)),i)))) /\ (LSeg (((GoB f) * ((len (GoB f)),j)),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {} let i, j be Element of NAT ; ::_thesis: ( 1 <= i & j <= width (GoB f) & i < j implies (LSeg (((GoB f) * ((len (GoB f)),1)),((GoB f) * ((len (GoB f)),i)))) /\ (LSeg (((GoB f) * ((len (GoB f)),j)),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {} ) assume that A1: 1 <= i and A2: j <= width (GoB f) and A3: i < j ; ::_thesis: (LSeg (((GoB f) * ((len (GoB f)),1)),((GoB f) * ((len (GoB f)),i)))) /\ (LSeg (((GoB f) * ((len (GoB f)),j)),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {} set A = LSeg (((GoB f) * ((len (GoB f)),1)),((GoB f) * ((len (GoB f)),i))); set B = LSeg (((GoB f) * ((len (GoB f)),j)),((GoB f) * ((len (GoB f)),(width (GoB f))))); assume (LSeg (((GoB f) * ((len (GoB f)),1)),((GoB f) * ((len (GoB f)),i)))) /\ (LSeg (((GoB f) * ((len (GoB f)),j)),((GoB f) * ((len (GoB f)),(width (GoB f)))))) <> {} ; ::_thesis: contradiction then LSeg (((GoB f) * ((len (GoB f)),1)),((GoB f) * ((len (GoB f)),i))) meets LSeg (((GoB f) * ((len (GoB f)),j)),((GoB f) * ((len (GoB f)),(width (GoB f))))) by XBOOLE_0:def_7; then consider x being set such that A4: x in LSeg (((GoB f) * ((len (GoB f)),1)),((GoB f) * ((len (GoB f)),i))) and A5: x in LSeg (((GoB f) * ((len (GoB f)),j)),((GoB f) * ((len (GoB f)),(width (GoB f))))) by XBOOLE_0:3; reconsider x1 = x as Point of (TOP-REAL 2) by A4; A6: 1 <= len (GoB f) by GOBOARD7:32; A7: i <= width (GoB f) by A2, A3, XXREAL_0:2; ((GoB f) * ((len (GoB f)),1)) `2 <= ((GoB f) * ((len (GoB f)),i)) `2 proof percases ( i = 1 or i > 1 ) by A1, XXREAL_0:1; suppose i = 1 ; ::_thesis: ((GoB f) * ((len (GoB f)),1)) `2 <= ((GoB f) * ((len (GoB f)),i)) `2 hence ((GoB f) * ((len (GoB f)),1)) `2 <= ((GoB f) * ((len (GoB f)),i)) `2 ; ::_thesis: verum end; suppose i > 1 ; ::_thesis: ((GoB f) * ((len (GoB f)),1)) `2 <= ((GoB f) * ((len (GoB f)),i)) `2 hence ((GoB f) * ((len (GoB f)),1)) `2 <= ((GoB f) * ((len (GoB f)),i)) `2 by A6, A7, GOBOARD5:4; ::_thesis: verum end; end; end; then A8: x1 `2 <= ((GoB f) * ((len (GoB f)),i)) `2 by A4, TOPREAL1:4; A9: ((GoB f) * ((len (GoB f)),j)) `2 > ((GoB f) * ((len (GoB f)),i)) `2 by A1, A2, A3, A6, GOBOARD5:4; A10: 1 <= j by A1, A3, XXREAL_0:2; ((GoB f) * ((len (GoB f)),j)) `2 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `2 proof percases ( j < width (GoB f) or j = width (GoB f) ) by A2, XXREAL_0:1; suppose j < width (GoB f) ; ::_thesis: ((GoB f) * ((len (GoB f)),j)) `2 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `2 hence ((GoB f) * ((len (GoB f)),j)) `2 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `2 by A6, A10, GOBOARD5:4; ::_thesis: verum end; suppose j = width (GoB f) ; ::_thesis: ((GoB f) * ((len (GoB f)),j)) `2 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `2 hence ((GoB f) * ((len (GoB f)),j)) `2 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `2 ; ::_thesis: verum end; end; end; then x1 `2 >= ((GoB f) * ((len (GoB f)),j)) `2 by A5, TOPREAL1:4; hence contradiction by A8, A9, XXREAL_0:2; ::_thesis: verum end; theorem Th27: :: JORDAN5B:27 for f being FinSequence of (TOP-REAL 2) st f is being_S-Seq holds L_Cut (f,(f /. 1)) = f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq implies L_Cut (f,(f /. 1)) = f ) assume A1: f is being_S-Seq ; ::_thesis: L_Cut (f,(f /. 1)) = f then A2: 1 + 1 <= len f by TOPREAL1:def_8; then 1 <= len f by XXREAL_0:2; then A3: 1 in dom f by FINSEQ_3:25; A4: 1 + 1 in dom f by A2, FINSEQ_3:25; A5: 1 < len f by A2, NAT_1:13; A6: f is one-to-one by A1; A7: f /. 1 = f . 1 by A3, PARTFUN1:def_6; A8: Index ((f /. 1),f) = 1 by A2, JORDAN3:11; f /. 1 <> f /. (1 + 1) by A3, A4, A6, PARTFUN2:10; then f /. 1 <> f . (1 + 1) by A4, PARTFUN1:def_6; hence L_Cut (f,(f /. 1)) = <*(f /. 1)*> ^ (mid (f,((Index ((f /. 1),f)) + 1),(len f))) by A8, JORDAN3:def_3 .= mid (f,1,(len f)) by A3, A5, A7, A8, FINSEQ_6:126 .= f by A2, FINSEQ_6:120, XXREAL_0:2 ; ::_thesis: verum end; theorem :: JORDAN5B:28 for f being FinSequence of (TOP-REAL 2) st f is being_S-Seq holds R_Cut (f,(f /. (len f))) = f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq implies R_Cut (f,(f /. (len f))) = f ) assume A1: f is being_S-Seq ; ::_thesis: R_Cut (f,(f /. (len f))) = f then A2: 2 <= len f by TOPREAL1:def_8; then A3: f /. (len f) in L~ f by JORDAN3:1; A4: f /. (len f) = (Rev f) /. 1 by A2, CARD_1:27, FINSEQ_5:65; thus R_Cut (f,(f /. (len f))) = Rev (Rev (R_Cut (f,(f /. (len f))))) .= Rev (L_Cut ((Rev f),(f /. (len f)))) by A1, A3, JORDAN3:22 .= Rev (Rev f) by A1, A4, Th27 .= f ; ::_thesis: verum end; theorem :: JORDAN5B:29 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f holds p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) ) assume A1: p in L~ f ; ::_thesis: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) then A2: Index (p,f) < len f by JORDAN3:8; A3: 1 <= Index (p,f) by A1, JORDAN3:8; A4: (Index (p,f)) + 1 <= len f by A2, NAT_1:13; p in LSeg (f,(Index (p,f))) by A1, JORDAN3:9; hence p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, A4, TOPREAL1:def_3; ::_thesis: verum end; theorem :: JORDAN5B:30 for f being FinSequence of (TOP-REAL 2) for i being Element of NAT st f is unfolded & f is s.n.c. & f is one-to-one & len f >= 2 & f /. 1 in LSeg (f,i) holds i = 1 proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st f is unfolded & f is s.n.c. & f is one-to-one & len f >= 2 & f /. 1 in LSeg (f,i) holds i = 1 let i be Element of NAT ; ::_thesis: ( f is unfolded & f is s.n.c. & f is one-to-one & len f >= 2 & f /. 1 in LSeg (f,i) implies i = 1 ) assume that A1: ( f is unfolded & f is s.n.c. & f is one-to-one ) and A2: 2 <= len f ; ::_thesis: ( not f /. 1 in LSeg (f,i) or i = 1 ) 1 <= len f by A2, XXREAL_0:2; then A3: 1 in dom f by FINSEQ_3:25; A4: 2 in dom f by A2, FINSEQ_3:25; assume A5: f /. 1 in LSeg (f,i) ; ::_thesis: i = 1 assume A6: i <> 1 ; ::_thesis: contradiction percases ( i > 1 or i < 1 ) by A6, XXREAL_0:1; supposeA7: i > 1 ; ::_thesis: contradiction 1 + 1 <= len f by A2; then f /. 1 in LSeg (f,1) by TOPREAL1:21; then A8: f /. 1 in (LSeg (f,1)) /\ (LSeg (f,i)) by A5, XBOOLE_0:def_4; then A9: LSeg (f,1) meets LSeg (f,i) by XBOOLE_0:4; now__::_thesis:_contradiction percases ( i = 2 or i > 2 or i < 2 ) by XXREAL_0:1; supposeA10: i = 2 ; ::_thesis: contradiction then A11: 1 + 2 <= len f by A5, TOPREAL1:def_3; 1 + 1 = 2 ; then f /. 1 in {(f /. 2)} by A1, A8, A10, A11, TOPREAL1:def_6; then f /. 1 = f /. 2 by TARSKI:def_1; hence contradiction by A1, A3, A4, PARTFUN2:10; ::_thesis: verum end; suppose i > 2 ; ::_thesis: contradiction then 1 + 1 < i ; hence contradiction by A1, A9, TOPREAL1:def_7; ::_thesis: verum end; suppose i < 2 ; ::_thesis: contradiction then i < 1 + 1 ; hence contradiction by A7, NAT_1:13; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; suppose i < 1 ; ::_thesis: contradiction hence contradiction by A5, TOPREAL1:def_3; ::_thesis: verum end; end; end; theorem :: JORDAN5B:31 for f being non constant standard special_circular_sequence for j being Element of NAT for P being Subset of (TOP-REAL 2) st 1 <= j & j <= width (GoB f) & P = LSeg (((GoB f) * (1,j)),((GoB f) * ((len (GoB f)),j))) holds P is_S-P_arc_joining (GoB f) * (1,j),(GoB f) * ((len (GoB f)),j) proof let f be non constant standard special_circular_sequence; ::_thesis: for j being Element of NAT for P being Subset of (TOP-REAL 2) st 1 <= j & j <= width (GoB f) & P = LSeg (((GoB f) * (1,j)),((GoB f) * ((len (GoB f)),j))) holds P is_S-P_arc_joining (GoB f) * (1,j),(GoB f) * ((len (GoB f)),j) let j be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL 2) st 1 <= j & j <= width (GoB f) & P = LSeg (((GoB f) * (1,j)),((GoB f) * ((len (GoB f)),j))) holds P is_S-P_arc_joining (GoB f) * (1,j),(GoB f) * ((len (GoB f)),j) let P be Subset of (TOP-REAL 2); ::_thesis: ( 1 <= j & j <= width (GoB f) & P = LSeg (((GoB f) * (1,j)),((GoB f) * ((len (GoB f)),j))) implies P is_S-P_arc_joining (GoB f) * (1,j),(GoB f) * ((len (GoB f)),j) ) assume that A1: 1 <= j and A2: j <= width (GoB f) and A3: P = LSeg (((GoB f) * (1,j)),((GoB f) * ((len (GoB f)),j))) ; ::_thesis: P is_S-P_arc_joining (GoB f) * (1,j),(GoB f) * ((len (GoB f)),j) set p = (GoB f) * (1,j); set q = (GoB f) * ((len (GoB f)),j); 1 <= len (GoB f) by GOBOARD7:32; then A4: ((GoB f) * (1,j)) `2 = ((GoB f) * ((len (GoB f)),j)) `2 by A1, A2, GOBOARD5:1; A5: ((GoB f) * (1,j)) `1 <> ((GoB f) * ((len (GoB f)),j)) `1 proof assume A6: ((GoB f) * (1,j)) `1 = ((GoB f) * ((len (GoB f)),j)) `1 ; ::_thesis: contradiction A7: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def_2; A8: 1 <= len (GoB f) by GOBOARD7:32; then A9: [1,j] in Indices (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) by A1, A2, A7, MATRIX_1:36; A10: [(len (GoB f)),j] in Indices (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) by A1, A2, A7, A8, MATRIX_1:36; (GoB f) * (1,j) = (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) * (1,j) by GOBOARD2:def_2 .= |[((Incr (X_axis f)) . 1),((Incr (Y_axis f)) . j)]| by A9, GOBOARD2:def_1 ; then A11: ((GoB f) * (1,j)) `1 = (Incr (X_axis f)) . 1 by EUCLID:52; A12: (GoB f) * ((len (GoB f)),j) = (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) * ((len (GoB f)),j) by GOBOARD2:def_2 .= |[((Incr (X_axis f)) . (len (GoB f))),((Incr (Y_axis f)) . j)]| by A10, GOBOARD2:def_1 ; A13: len (Incr (X_axis f)) = len (GoB f) by A7, GOBOARD2:def_1; A14: 1 <= len (GoB f) by GOBOARD7:32; A15: 1 <= len (Incr (X_axis f)) by A13, GOBOARD7:32; A16: len (GoB f) in dom (Incr (X_axis f)) by A13, A14, FINSEQ_3:25; 1 in dom (Incr (X_axis f)) by A15, FINSEQ_3:25; then len (GoB f) = 1 by A6, A11, A12, A16, EUCLID:52, SEQ_4:138; hence contradiction by GOBOARD7:32; ::_thesis: verum end; reconsider gg = <*((GoB f) * (1,j)),((GoB f) * ((len (GoB f)),j))*> as FinSequence of the carrier of (TOP-REAL 2) ; A17: len gg = 2 by FINSEQ_1:44; take gg ; :: according to TOPREAL4:def_1 ::_thesis: ( gg is being_S-Seq & P = L~ gg & (GoB f) * (1,j) = gg /. 1 & (GoB f) * ((len (GoB f)),j) = gg /. (len gg) ) thus gg is being_S-Seq by A4, A5, SPPOL_2:43; ::_thesis: ( P = L~ gg & (GoB f) * (1,j) = gg /. 1 & (GoB f) * ((len (GoB f)),j) = gg /. (len gg) ) thus P = L~ gg by A3, SPPOL_2:21; ::_thesis: ( (GoB f) * (1,j) = gg /. 1 & (GoB f) * ((len (GoB f)),j) = gg /. (len gg) ) thus ( (GoB f) * (1,j) = gg /. 1 & (GoB f) * ((len (GoB f)),j) = gg /. (len gg) ) by A17, FINSEQ_4:17; ::_thesis: verum end; theorem :: JORDAN5B:32 for f being non constant standard special_circular_sequence for j being Element of NAT for P being Subset of (TOP-REAL 2) st 1 <= j & j <= len (GoB f) & P = LSeg (((GoB f) * (j,1)),((GoB f) * (j,(width (GoB f))))) holds P is_S-P_arc_joining (GoB f) * (j,1),(GoB f) * (j,(width (GoB f))) proof let f be non constant standard special_circular_sequence; ::_thesis: for j being Element of NAT for P being Subset of (TOP-REAL 2) st 1 <= j & j <= len (GoB f) & P = LSeg (((GoB f) * (j,1)),((GoB f) * (j,(width (GoB f))))) holds P is_S-P_arc_joining (GoB f) * (j,1),(GoB f) * (j,(width (GoB f))) let j be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL 2) st 1 <= j & j <= len (GoB f) & P = LSeg (((GoB f) * (j,1)),((GoB f) * (j,(width (GoB f))))) holds P is_S-P_arc_joining (GoB f) * (j,1),(GoB f) * (j,(width (GoB f))) let P be Subset of (TOP-REAL 2); ::_thesis: ( 1 <= j & j <= len (GoB f) & P = LSeg (((GoB f) * (j,1)),((GoB f) * (j,(width (GoB f))))) implies P is_S-P_arc_joining (GoB f) * (j,1),(GoB f) * (j,(width (GoB f))) ) assume that A1: 1 <= j and A2: j <= len (GoB f) and A3: P = LSeg (((GoB f) * (j,1)),((GoB f) * (j,(width (GoB f))))) ; ::_thesis: P is_S-P_arc_joining (GoB f) * (j,1),(GoB f) * (j,(width (GoB f))) set p = (GoB f) * (j,1); set q = (GoB f) * (j,(width (GoB f))); 1 <= width (GoB f) by GOBOARD7:33; then A4: ((GoB f) * (j,1)) `1 = ((GoB f) * (j,(width (GoB f)))) `1 by A1, A2, GOBOARD5:2; A5: ((GoB f) * (j,1)) `2 <> ((GoB f) * (j,(width (GoB f)))) `2 proof assume A6: ((GoB f) * (j,1)) `2 = ((GoB f) * (j,(width (GoB f)))) `2 ; ::_thesis: contradiction A7: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def_2; A8: 1 <= width (GoB f) by GOBOARD7:33; then A9: [j,1] in Indices (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) by A1, A2, A7, MATRIX_1:36; A10: [j,(width (GoB f))] in Indices (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) by A1, A2, A7, A8, MATRIX_1:36; (GoB f) * (j,1) = (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) * (j,1) by GOBOARD2:def_2 .= |[((Incr (X_axis f)) . j),((Incr (Y_axis f)) . 1)]| by A9, GOBOARD2:def_1 ; then A11: ((GoB f) * (j,1)) `2 = (Incr (Y_axis f)) . 1 by EUCLID:52; A12: (GoB f) * (j,(width (GoB f))) = (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) * (j,(width (GoB f))) by GOBOARD2:def_2 .= |[((Incr (X_axis f)) . j),((Incr (Y_axis f)) . (width (GoB f)))]| by A10, GOBOARD2:def_1 ; A13: len (Incr (Y_axis f)) = width (GoB f) by A7, GOBOARD2:def_1; A14: 1 <= width (GoB f) by GOBOARD7:33; A15: 1 <= len (Incr (Y_axis f)) by A13, GOBOARD7:33; A16: width (GoB f) in dom (Incr (Y_axis f)) by A13, A14, FINSEQ_3:25; 1 in dom (Incr (Y_axis f)) by A15, FINSEQ_3:25; then width (GoB f) = 1 by A6, A11, A12, A16, EUCLID:52, SEQ_4:138; hence contradiction by GOBOARD7:33; ::_thesis: verum end; reconsider gg = <*((GoB f) * (j,1)),((GoB f) * (j,(width (GoB f))))*> as FinSequence of the carrier of (TOP-REAL 2) ; A17: len gg = 2 by FINSEQ_1:44; take gg ; :: according to TOPREAL4:def_1 ::_thesis: ( gg is being_S-Seq & P = L~ gg & (GoB f) * (j,1) = gg /. 1 & (GoB f) * (j,(width (GoB f))) = gg /. (len gg) ) thus gg is being_S-Seq by A4, A5, SPPOL_2:43; ::_thesis: ( P = L~ gg & (GoB f) * (j,1) = gg /. 1 & (GoB f) * (j,(width (GoB f))) = gg /. (len gg) ) thus P = L~ gg by A3, SPPOL_2:21; ::_thesis: ( (GoB f) * (j,1) = gg /. 1 & (GoB f) * (j,(width (GoB f))) = gg /. (len gg) ) thus ( (GoB f) * (j,1) = gg /. 1 & (GoB f) * (j,(width (GoB f))) = gg /. (len gg) ) by A17, FINSEQ_4:17; ::_thesis: verum end; theorem :: JORDAN5B:33 for f being FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) & p <> q holds L~ (B_Cut (f,p,q)) c= L~ f by Lm4;