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