:: SPRECT_3 semantic presentation
begin
theorem :: SPRECT_3:1
for D being non empty set
for f being non empty FinSequence of D
for g being FinSequence of D holds (g ^ f) /. (len (g ^ f)) = f /. (len f)
proof
let D be non empty set ; ::_thesis: for f being non empty FinSequence of D
for g being FinSequence of D holds (g ^ f) /. (len (g ^ f)) = f /. (len f)
let f be non empty FinSequence of D; ::_thesis: for g being FinSequence of D holds (g ^ f) /. (len (g ^ f)) = f /. (len f)
let g be FinSequence of D; ::_thesis: (g ^ f) /. (len (g ^ f)) = f /. (len f)
A1: len f >= 1 by NAT_1:14;
len (g ^ f) = (len g) + (len f) by FINSEQ_1:22;
hence (g ^ f) /. (len (g ^ f)) = f /. (len f) by A1, SEQ_4:136; ::_thesis: verum
end;
theorem Th2: :: SPRECT_3:2
for a, b, c, d being set holds Indices ((a,b) ][ (c,d)) = {[1,1],[1,2],[2,1],[2,2]}
proof
let a, b, c, d be set ; ::_thesis: Indices ((a,b) ][ (c,d)) = {[1,1],[1,2],[2,1],[2,2]}
thus Indices ((a,b) ][ (c,d)) = [:(Seg 2),(Seg 2):] by MATRIX_2:3
.= [:{1},(Seg 2):] \/ [:{2},(Seg 2):] by FINSEQ_1:2, ZFMISC_1:109
.= [:{1},(Seg 2):] \/ {[2,1],[2,2]} by FINSEQ_1:2, ZFMISC_1:30
.= {[1,1],[1,2]} \/ {[2,1],[2,2]} by FINSEQ_1:2, ZFMISC_1:30
.= {[1,1],[1,2],[2,1],[2,2]} by ENUMSET1:5 ; ::_thesis: verum
end;
begin
theorem Th3: :: SPRECT_3:3
for n being Element of NAT
for p, q being Point of (TOP-REAL n)
for r being Real st 0 < r & p = ((1 - r) * p) + (r * q) holds
p = q
proof
let n be Element of NAT ; ::_thesis: for p, q being Point of (TOP-REAL n)
for r being Real st 0 < r & p = ((1 - r) * p) + (r * q) holds
p = q
let p, q be Point of (TOP-REAL n); ::_thesis: for r being Real st 0 < r & p = ((1 - r) * p) + (r * q) holds
p = q
let r be Real; ::_thesis: ( 0 < r & p = ((1 - r) * p) + (r * q) implies p = q )
assume that
A1: 0 < r and
A2: p = ((1 - r) * p) + (r * q) ; ::_thesis: p = q
A3: ((1 - r) * p) + (r * p) = ((1 - r) + r) * p by EUCLID:33
.= p by EUCLID:29 ;
r * p = (r * p) + (0. (TOP-REAL n)) by EUCLID:27
.= (r * p) + (((1 - r) * p) + (- ((1 - r) * p))) by EUCLID:36
.= ((r * q) + ((1 - r) * p)) + (- ((1 - r) * p)) by A2, A3, EUCLID:26
.= (r * q) + (((1 - r) * p) + (- ((1 - r) * p))) by EUCLID:26
.= (r * q) + (0. (TOP-REAL n)) by EUCLID:36
.= r * q by EUCLID:27 ;
hence p = q by A1, EUCLID:34; ::_thesis: verum
end;
theorem Th4: :: SPRECT_3:4
for n being Element of NAT
for p, q being Point of (TOP-REAL n)
for r being Real st r < 1 & p = ((1 - r) * q) + (r * p) holds
p = q
proof
let n be Element of NAT ; ::_thesis: for p, q being Point of (TOP-REAL n)
for r being Real st r < 1 & p = ((1 - r) * q) + (r * p) holds
p = q
let p, q be Point of (TOP-REAL n); ::_thesis: for r being Real st r < 1 & p = ((1 - r) * q) + (r * p) holds
p = q
let r be Real; ::_thesis: ( r < 1 & p = ((1 - r) * q) + (r * p) implies p = q )
assume that
A1: r < 1 and
A2: p = ((1 - r) * q) + (r * p) ; ::_thesis: p = q
set s = 1 - r;
r + 0 < 1 by A1;
then A3: 0 < 1 - r by XREAL_1:20;
p = ((1 - (1 - r)) * p) + ((1 - r) * q) by A2;
hence p = q by A3, Th3; ::_thesis: verum
end;
theorem :: SPRECT_3:5
for n being Element of NAT
for p, q being Point of (TOP-REAL n) st p = (1 / 2) * (p + q) holds
p = q
proof
let n be Element of NAT ; ::_thesis: for p, q being Point of (TOP-REAL n) st p = (1 / 2) * (p + q) holds
p = q
let p, q be Point of (TOP-REAL n); ::_thesis: ( p = (1 / 2) * (p + q) implies p = q )
assume p = (1 / 2) * (p + q) ; ::_thesis: p = q
then p = ((1 - (1 / 2)) * p) + ((1 / 2) * q) by EUCLID:32;
hence p = q by Th3; ::_thesis: verum
end;
theorem Th6: :: SPRECT_3:6
for n being Element of NAT
for p, q, r being Point of (TOP-REAL n) st q in LSeg (p,r) & r in LSeg (p,q) holds
q = r
proof
let n be Element of NAT ; ::_thesis: for p, q, r being Point of (TOP-REAL n) st q in LSeg (p,r) & r in LSeg (p,q) holds
q = r
let p, q, r be Point of (TOP-REAL n); ::_thesis: ( q in LSeg (p,r) & r in LSeg (p,q) implies q = r )
assume q in LSeg (p,r) ; ::_thesis: ( not r in LSeg (p,q) or q = r )
then consider r1 being Real such that
A1: q = ((1 - r1) * p) + (r1 * r) and
A2: 0 <= r1 and
A3: r1 <= 1 ;
assume r in LSeg (p,q) ; ::_thesis: q = r
then consider r2 being Real such that
A4: r = ((1 - r2) * p) + (r2 * q) and
0 <= r2 and
A5: r2 <= 1 ;
A6: r1 * r2 <= 1 by A2, A3, A5, XREAL_1:160;
A7: (1 - r2) + (r2 * (1 - r1)) = 1 - (r2 * r1) ;
A8: r = ((1 - r2) * p) + ((r2 * ((1 - r1) * p)) + (r2 * (r1 * r))) by A1, A4, EUCLID:32
.= (((1 - r2) * p) + (r2 * ((1 - r1) * p))) + (r2 * (r1 * r)) by EUCLID:26
.= (((1 - r2) * p) + ((r2 * (1 - r1)) * p)) + (r2 * (r1 * r)) by EUCLID:30
.= ((1 - (r2 * r1)) * p) + (r2 * (r1 * r)) by A7, EUCLID:33
.= ((1 - (r2 * r1)) * p) + ((r2 * r1) * r) by EUCLID:30 ;
A9: (1 - r1) + (r1 * (1 - r2)) = 1 - (r1 * r2) ;
A10: q = ((1 - r1) * p) + ((r1 * ((1 - r2) * p)) + (r1 * (r2 * q))) by A1, A4, EUCLID:32
.= (((1 - r1) * p) + (r1 * ((1 - r2) * p))) + (r1 * (r2 * q)) by EUCLID:26
.= (((1 - r1) * p) + ((r1 * (1 - r2)) * p)) + (r1 * (r2 * q)) by EUCLID:30
.= ((1 - (r1 * r2)) * p) + (r1 * (r2 * q)) by A9, EUCLID:33
.= ((1 - (r1 * r2)) * p) + ((r1 * r2) * q) by EUCLID:30 ;
percases ( r1 * r2 = 1 or r1 * r2 < 1 ) by A6, XXREAL_0:1;
supposeA11: r1 * r2 = 1 ; ::_thesis: q = r
then ( 1 <= r1 or 1 <= r2 ) by A2, XREAL_1:162;
then ( 1 * r1 = 1 or 1 * r2 = 1 ) by A3, A5, XXREAL_0:1;
hence q = (0 * p) + r by A1, A11, EUCLID:29
.= (0. (TOP-REAL n)) + r by EUCLID:29
.= r by EUCLID:27 ;
::_thesis: verum
end;
supposeA12: r1 * r2 < 1 ; ::_thesis: q = r
hence q = p by A10, Th4
.= r by A8, A12, Th4 ;
::_thesis: verum
end;
end;
end;
begin
theorem Th7: :: SPRECT_3:7
for A being non empty Subset of (TOP-REAL 2)
for p being Element of (Euclid 2)
for r being Real st A = Ball (p,r) holds
A is connected
proof
let A be non empty Subset of (TOP-REAL 2); ::_thesis: for p being Element of (Euclid 2)
for r being Real st A = Ball (p,r) holds
A is connected
let p be Element of (Euclid 2); ::_thesis: for r being Real st A = Ball (p,r) holds
A is connected
let r be Real; ::_thesis: ( A = Ball (p,r) implies A is connected )
assume A1: A = Ball (p,r) ; ::_thesis: A is connected
A is convex
proof
let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def_1 ::_thesis: ( not w1 in A or not w2 in A or LSeg (w1,w2) c= A )
assume that
A2: w1 in A and
A3: w2 in A ; ::_thesis: LSeg (w1,w2) c= A
thus LSeg (w1,w2) c= A by A1, A2, A3, TOPREAL3:21; ::_thesis: verum
end;
hence A is connected ; ::_thesis: verum
end;
theorem Th8: :: SPRECT_3:8
for A, B being Subset of (TOP-REAL 2) st A is open & B is_a_component_of A holds
B is open
proof
let A, B be Subset of (TOP-REAL 2); ::_thesis: ( A is open & B is_a_component_of A implies B is open )
assume that
A1: A is open and
A2: B is_a_component_of A ; ::_thesis: B is open
A3: B c= A by A2, SPRECT_1:5;
A4: TopStruct(# the U1 of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8;
then reconsider C = B, D = A as Subset of (TopSpaceMetr (Euclid 2)) ;
A5: D is open by A1, A4, PRE_TOPC:30;
for p being Point of (Euclid 2) st p in C holds
ex r being real number st
( r > 0 & Ball (p,r) c= C )
proof
let p be Point of (Euclid 2); ::_thesis: ( p in C implies ex r being real number st
( r > 0 & Ball (p,r) c= C ) )
assume A6: p in C ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= C )
then consider r being real number such that
A7: r > 0 and
A8: Ball (p,r) c= D by A3, A5, TOPMETR:15;
reconsider r = r as Real by XREAL_0:def_1;
take r ; ::_thesis: ( r > 0 & Ball (p,r) c= C )
thus r > 0 by A7; ::_thesis: Ball (p,r) c= C
reconsider E = Ball (p,r) as Subset of (TOP-REAL 2) by A4, TOPMETR:12;
A9: p in E by A7, GOBOARD6:1;
then A10: E is connected by Th7;
B meets E by A6, A9, XBOOLE_0:3;
hence Ball (p,r) c= C by A2, A8, A10, GOBOARD9:4; ::_thesis: verum
end;
then C is open by TOPMETR:15;
hence B is open by A4, PRE_TOPC:30; ::_thesis: verum
end;
theorem :: SPRECT_3:9
for p, q, r, s being Point of (TOP-REAL 2) st LSeg (p,q) is horizontal & LSeg (r,s) is horizontal & LSeg (p,q) meets LSeg (r,s) holds
p `2 = r `2
proof
let p, q, r, s be Point of (TOP-REAL 2); ::_thesis: ( LSeg (p,q) is horizontal & LSeg (r,s) is horizontal & LSeg (p,q) meets LSeg (r,s) implies p `2 = r `2 )
assume that
A1: LSeg (p,q) is horizontal and
A2: LSeg (r,s) is horizontal ; ::_thesis: ( not LSeg (p,q) meets LSeg (r,s) or p `2 = r `2 )
assume LSeg (p,q) meets LSeg (r,s) ; ::_thesis: p `2 = r `2
then (LSeg (p,q)) /\ (LSeg (r,s)) <> {} by XBOOLE_0:def_7;
then consider x being Point of (TOP-REAL 2) such that
A3: x in (LSeg (p,q)) /\ (LSeg (r,s)) by SUBSET_1:4;
A4: x in LSeg (r,s) by A3, XBOOLE_0:def_4;
x in LSeg (p,q) by A3, XBOOLE_0:def_4;
hence p `2 = x `2 by A1, SPPOL_1:40
.= r `2 by A2, A4, SPPOL_1:40 ;
::_thesis: verum
end;
theorem :: SPRECT_3:10
for p, q, r being Point of (TOP-REAL 2) st LSeg (p,q) is vertical & LSeg (q,r) is horizontal holds
(LSeg (p,q)) /\ (LSeg (q,r)) = {q}
proof
let p, q, r be Point of (TOP-REAL 2); ::_thesis: ( LSeg (p,q) is vertical & LSeg (q,r) is horizontal implies (LSeg (p,q)) /\ (LSeg (q,r)) = {q} )
assume that
A1: LSeg (p,q) is vertical and
A2: LSeg (q,r) is horizontal ; ::_thesis: (LSeg (p,q)) /\ (LSeg (q,r)) = {q}
for x being set holds
( x in (LSeg (p,q)) /\ (LSeg (q,r)) iff x = q )
proof
let x be set ; ::_thesis: ( x in (LSeg (p,q)) /\ (LSeg (q,r)) iff x = q )
thus ( x in (LSeg (p,q)) /\ (LSeg (q,r)) implies x = q ) ::_thesis: ( x = q implies x in (LSeg (p,q)) /\ (LSeg (q,r)) )
proof
assume A3: x in (LSeg (p,q)) /\ (LSeg (q,r)) ; ::_thesis: x = q
then reconsider x = x as Point of (TOP-REAL 2) ;
x in LSeg (q,r) by A3, XBOOLE_0:def_4;
then A4: x `2 = q `2 by A2, SPPOL_1:40;
x in LSeg (p,q) by A3, XBOOLE_0:def_4;
then x `1 = q `1 by A1, SPPOL_1:41;
hence x = q by A4, TOPREAL3:6; ::_thesis: verum
end;
assume A5: x = q ; ::_thesis: x in (LSeg (p,q)) /\ (LSeg (q,r))
then A6: x in LSeg (q,r) by RLTOPSP1:68;
x in LSeg (p,q) by A5, RLTOPSP1:68;
hence x in (LSeg (p,q)) /\ (LSeg (q,r)) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg (p,q)) /\ (LSeg (q,r)) = {q} by TARSKI:def_1; ::_thesis: verum
end;
theorem :: SPRECT_3:11
for p, q, r, s being Point of (TOP-REAL 2) st LSeg (p,q) is horizontal & LSeg (s,r) is vertical & r in LSeg (p,q) holds
(LSeg (p,q)) /\ (LSeg (s,r)) = {r}
proof
let p, q, r, s be Point of (TOP-REAL 2); ::_thesis: ( LSeg (p,q) is horizontal & LSeg (s,r) is vertical & r in LSeg (p,q) implies (LSeg (p,q)) /\ (LSeg (s,r)) = {r} )
assume that
A1: LSeg (p,q) is horizontal and
A2: LSeg (s,r) is vertical and
A3: r in LSeg (p,q) ; ::_thesis: (LSeg (p,q)) /\ (LSeg (s,r)) = {r}
for x being set holds
( x in (LSeg (p,q)) /\ (LSeg (s,r)) iff x = r )
proof
let x be set ; ::_thesis: ( x in (LSeg (p,q)) /\ (LSeg (s,r)) iff x = r )
thus ( x in (LSeg (p,q)) /\ (LSeg (s,r)) implies x = r ) ::_thesis: ( x = r implies x in (LSeg (p,q)) /\ (LSeg (s,r)) )
proof
assume A4: x in (LSeg (p,q)) /\ (LSeg (s,r)) ; ::_thesis: x = r
then reconsider x = x as Point of (TOP-REAL 2) ;
x in LSeg (p,q) by A4, XBOOLE_0:def_4;
then A5: x `2 = p `2 by A1, SPPOL_1:40;
x in LSeg (s,r) by A4, XBOOLE_0:def_4;
then A6: x `1 = r `1 by A2, SPPOL_1:41;
p `2 = r `2 by A1, A3, SPPOL_1:40;
hence x = r by A5, A6, TOPREAL3:6; ::_thesis: verum
end;
assume A7: x = r ; ::_thesis: x in (LSeg (p,q)) /\ (LSeg (s,r))
then x in LSeg (s,r) by RLTOPSP1:68;
hence x in (LSeg (p,q)) /\ (LSeg (s,r)) by A3, A7, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg (p,q)) /\ (LSeg (s,r)) = {r} by TARSKI:def_1; ::_thesis: verum
end;
begin
theorem :: SPRECT_3:12
for j, k, i being Element of NAT
for G being Go-board st 1 <= j & j <= k & k <= width G & 1 <= i & i <= len G holds
(G * (i,j)) `2 <= (G * (i,k)) `2
proof
let j, k, i be Element of NAT ; ::_thesis: for G being Go-board st 1 <= j & j <= k & k <= width G & 1 <= i & i <= len G holds
(G * (i,j)) `2 <= (G * (i,k)) `2
let G be Go-board; ::_thesis: ( 1 <= j & j <= k & k <= width G & 1 <= i & i <= len G implies (G * (i,j)) `2 <= (G * (i,k)) `2 )
assume that
A1: 1 <= j and
A2: j <= k and
A3: k <= width G and
A4: 1 <= i and
A5: i <= len G ; ::_thesis: (G * (i,j)) `2 <= (G * (i,k)) `2
percases ( j < k or j = k ) by A2, XXREAL_0:1;
suppose j < k ; ::_thesis: (G * (i,j)) `2 <= (G * (i,k)) `2
hence (G * (i,j)) `2 <= (G * (i,k)) `2 by A1, A3, A4, A5, GOBOARD5:4; ::_thesis: verum
end;
suppose j = k ; ::_thesis: (G * (i,j)) `2 <= (G * (i,k)) `2
hence (G * (i,j)) `2 <= (G * (i,k)) `2 ; ::_thesis: verum
end;
end;
end;
theorem :: SPRECT_3:13
for j, i, k being Element of NAT
for G being Go-board st 1 <= j & j <= width G & 1 <= i & i <= k & k <= len G holds
(G * (i,j)) `1 <= (G * (k,j)) `1
proof
let j, i, k be Element of NAT ; ::_thesis: for G being Go-board st 1 <= j & j <= width G & 1 <= i & i <= k & k <= len G holds
(G * (i,j)) `1 <= (G * (k,j)) `1
let G be Go-board; ::_thesis: ( 1 <= j & j <= width G & 1 <= i & i <= k & k <= len G implies (G * (i,j)) `1 <= (G * (k,j)) `1 )
assume that
A1: 1 <= j and
A2: j <= width G and
A3: 1 <= i and
A4: i <= k and
A5: k <= len G ; ::_thesis: (G * (i,j)) `1 <= (G * (k,j)) `1
percases ( i < k or i = k ) by A4, XXREAL_0:1;
suppose i < k ; ::_thesis: (G * (i,j)) `1 <= (G * (k,j)) `1
hence (G * (i,j)) `1 <= (G * (k,j)) `1 by A1, A2, A3, A5, GOBOARD5:3; ::_thesis: verum
end;
suppose i = k ; ::_thesis: (G * (i,j)) `1 <= (G * (k,j)) `1
hence (G * (i,j)) `1 <= (G * (k,j)) `1 ; ::_thesis: verum
end;
end;
end;
theorem Th14: :: SPRECT_3:14
for C being Subset of (TOP-REAL 2) holds LSeg ((NW-corner C),(NE-corner C)) c= L~ (SpStSeq C)
proof
let C be Subset of (TOP-REAL 2); ::_thesis: LSeg ((NW-corner C),(NE-corner C)) c= L~ (SpStSeq C)
A1: (LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) c= ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) \/ ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) by XBOOLE_1:7;
LSeg ((NW-corner C),(NE-corner C)) c= (LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) by XBOOLE_1:7;
then LSeg ((NW-corner C),(NE-corner C)) c= ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) \/ ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) by A1, XBOOLE_1:1;
hence LSeg ((NW-corner C),(NE-corner C)) c= L~ (SpStSeq C) by SPRECT_1:41; ::_thesis: verum
end;
theorem Th15: :: SPRECT_3:15
for C being non empty compact Subset of (TOP-REAL 2) holds N-min C in LSeg ((NW-corner C),(NE-corner C))
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: N-min C in LSeg ((NW-corner C),(NE-corner C))
A1: N-most C c= LSeg ((NW-corner C),(NE-corner C)) by XBOOLE_1:17;
N-min C in N-most C by PSCOMP_1:42;
hence N-min C in LSeg ((NW-corner C),(NE-corner C)) by A1; ::_thesis: verum
end;
registration
let C be Subset of (TOP-REAL 2);
cluster LSeg ((NW-corner C),(NE-corner C)) -> horizontal ;
coherence
LSeg ((NW-corner C),(NE-corner C)) is horizontal
proof
(NW-corner C) `2 = N-bound C by EUCLID:52
.= (NE-corner C) `2 by EUCLID:52 ;
hence LSeg ((NW-corner C),(NE-corner C)) is horizontal by SPPOL_1:15; ::_thesis: verum
end;
end;
theorem :: SPRECT_3:16
for g being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st g /. 1 <> p & ( (g /. 1) `1 = p `1 or (g /. 1) `2 = p `2 ) & g is being_S-Seq & (LSeg (p,(g /. 1))) /\ (L~ g) = {(g /. 1)} holds
<*p*> ^ g is being_S-Seq
proof
let g be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st g /. 1 <> p & ( (g /. 1) `1 = p `1 or (g /. 1) `2 = p `2 ) & g is being_S-Seq & (LSeg (p,(g /. 1))) /\ (L~ g) = {(g /. 1)} holds
<*p*> ^ g is being_S-Seq
let p be Point of (TOP-REAL 2); ::_thesis: ( g /. 1 <> p & ( (g /. 1) `1 = p `1 or (g /. 1) `2 = p `2 ) & g is being_S-Seq & (LSeg (p,(g /. 1))) /\ (L~ g) = {(g /. 1)} implies <*p*> ^ g is being_S-Seq )
assume that
A1: g /. 1 <> p and
A2: ( (g /. 1) `1 = p `1 or (g /. 1) `2 = p `2 ) and
A3: g is being_S-Seq and
A4: (LSeg (p,(g /. 1))) /\ (L~ g) = {(g /. 1)} ; ::_thesis: <*p*> ^ g is being_S-Seq
set f = <*p,(g /. 1)*>;
A5: <*p,(g /. 1)*> is being_S-Seq by A1, A2, SPPOL_2:43;
reconsider g9 = g as S-Sequence_in_R2 by A3;
A6: 1 in dom g9 by FINSEQ_5:6;
A7: len <*p,(g /. 1)*> = 1 + 1 by FINSEQ_1:44;
then (len <*p,(g /. 1)*>) -' 1 = 1 by NAT_D:34;
then A8: mid (<*p,(g /. 1)*>,1,((len <*p,(g /. 1)*>) -' 1)) = <*(<*p,(g /. 1)*> /. 1)*> by A7, JORDAN4:15
.= <*p*> by FINSEQ_4:17 ;
A9: (L~ <*p,(g /. 1)*>) /\ (L~ g) = {(g /. 1)} by A4, SPPOL_2:21
.= {(g . 1)} by A6, PARTFUN1:def_6 ;
<*p,(g /. 1)*> . (len <*p,(g /. 1)*>) = g /. 1 by A7, FINSEQ_1:44
.= g . 1 by A6, PARTFUN1:def_6 ;
hence <*p*> ^ g is being_S-Seq by A3, A5, A9, A8, JORDAN3:45; ::_thesis: verum
end;
theorem :: SPRECT_3:17
for j being Element of NAT
for f being S-Sequence_in_R2
for p being Point of (TOP-REAL 2) st 1 < j & j <= len f & p in L~ (mid (f,1,j)) holds
LE p,f /. j, L~ f,f /. 1,f /. (len f)
proof
let j be Element of NAT ; ::_thesis: for f being S-Sequence_in_R2
for p being Point of (TOP-REAL 2) st 1 < j & j <= len f & p in L~ (mid (f,1,j)) holds
LE p,f /. j, L~ f,f /. 1,f /. (len f)
let f be S-Sequence_in_R2; ::_thesis: for p being Point of (TOP-REAL 2) st 1 < j & j <= len f & p in L~ (mid (f,1,j)) holds
LE p,f /. j, L~ f,f /. 1,f /. (len f)
let p be Point of (TOP-REAL 2); ::_thesis: ( 1 < j & j <= len f & p in L~ (mid (f,1,j)) implies LE p,f /. j, L~ f,f /. 1,f /. (len f) )
assume that
A1: 1 < j and
A2: j <= len f and
A3: p in L~ (mid (f,1,j)) ; ::_thesis: LE p,f /. j, L~ f,f /. 1,f /. (len f)
consider i being Element of NAT such that
A4: 1 <= i and
A5: i + 1 <= len (mid (f,1,j)) and
A6: p in LSeg ((mid (f,1,j)),i) by A3, SPPOL_2:13;
A7: (j -' 1) + 1 = j by A1, XREAL_1:235;
then A8: i + 1 <= j by A1, A2, A5, JORDAN4:8;
then i < (j -' 1) + 1 by A7, NAT_1:13;
then A9: LSeg ((mid (f,1,j)),i) = LSeg (f,((i + 1) -' 1)) by A1, A2, A4, JORDAN4:19;
1 <= i + 1 by NAT_1:11;
then A10: LE f /. (i + 1),f /. j, L~ f,f /. 1,f /. (len f) by A2, A8, JORDAN5C:24;
A11: i = (i + 1) -' 1 by NAT_D:34;
i + 1 <= len f by A2, A8, XXREAL_0:2;
then LE p,f /. (i + 1), L~ f,f /. 1,f /. (len f) by A4, A6, A11, A9, JORDAN5C:26;
hence LE p,f /. j, L~ f,f /. 1,f /. (len f) by A10, JORDAN5C:13; ::_thesis: verum
end;
theorem :: SPRECT_3:18
for i, j being Element of NAT
for h being FinSequence of (TOP-REAL 2) st i in dom h & j in dom h holds
L~ (mid (h,i,j)) c= L~ h
proof
let i, j be Element of NAT ; ::_thesis: for h being FinSequence of (TOP-REAL 2) st i in dom h & j in dom h holds
L~ (mid (h,i,j)) c= L~ h
let h be FinSequence of (TOP-REAL 2); ::_thesis: ( i in dom h & j in dom h implies L~ (mid (h,i,j)) c= L~ h )
assume that
A1: i in dom h and
A2: j in dom h ; ::_thesis: L~ (mid (h,i,j)) c= L~ h
A3: i <= len h by A1, FINSEQ_3:25;
A4: j <= len h by A2, FINSEQ_3:25;
A5: 1 <= j by A2, FINSEQ_3:25;
1 <= i by A1, FINSEQ_3:25;
hence L~ (mid (h,i,j)) c= L~ h by A3, A5, A4, JORDAN4:35; ::_thesis: verum
end;
theorem :: SPRECT_3:19
for i, j being Element of NAT st 1 <= i & i < j holds
for f being FinSequence of (TOP-REAL 2) st j <= len f holds
L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j)))
proof
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i < j implies for f being FinSequence of (TOP-REAL 2) st j <= len f holds
L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j))) )
assume that
A1: 1 <= i and
A2: i < j ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st j <= len f holds
L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j)))
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( j <= len f implies L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j))) )
assume A3: j <= len f ; ::_thesis: L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j)))
set A = { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } ;
set B = { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } ;
A4: { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } = { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))}
proof
thus { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } c= { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} :: according to XBOOLE_0:def_10 ::_thesis: { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} c= { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } or e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} )
assume e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))}
then consider k being Element of NAT such that
A5: e = LSeg (f,k) and
A6: i <= k and
A7: k < j ;
( i = k or i < k ) by A6, XXREAL_0:1;
then ( i = k or i + 1 <= k ) by NAT_1:13;
then ( e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } or e in {(LSeg (f,i))} ) by A5, A7, TARSKI:def_1;
hence e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} by XBOOLE_0:def_3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} or e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } )
assume A8: e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) }
percases ( e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } or e in {(LSeg (f,i))} ) by A8, XBOOLE_0:def_3;
suppose e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) }
then consider k being Element of NAT such that
A9: e = LSeg (f,k) and
A10: i + 1 <= k and
A11: k < j ;
i < k by A10, NAT_1:13;
hence e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } by A9, A11; ::_thesis: verum
end;
suppose e in {(LSeg (f,i))} ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) }
then e = LSeg (f,i) by TARSKI:def_1;
hence e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } by A2; ::_thesis: verum
end;
end;
end;
A12: 1 <= i + 1 by NAT_1:11;
A13: i + 1 <= j by A2, NAT_1:13;
thus L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } by A1, A2, A3, SPRECT_2:14
.= (union { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } ) \/ (union {(LSeg (f,i))}) by A4, ZFMISC_1:78
.= (union { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } ) \/ (LSeg (f,i)) by ZFMISC_1:25
.= (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j))) by A3, A12, A13, SPRECT_2:14 ; ::_thesis: verum
end;
theorem :: SPRECT_3:20
for i, j being Element of NAT
for f being FinSequence of (TOP-REAL 2) st 1 <= i & i < j & j <= len f holds
L~ (mid (f,i,j)) = (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1)))
proof
let i, j be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st 1 <= i & i < j & j <= len f holds
L~ (mid (f,i,j)) = (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1)))
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( 1 <= i & i < j & j <= len f implies L~ (mid (f,i,j)) = (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1))) )
assume that
A1: 1 <= i and
A2: i < j and
A3: j <= len f ; ::_thesis: L~ (mid (f,i,j)) = (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1)))
j -' 1 <= j by NAT_D:35;
then A4: j -' 1 <= len f by A3, XXREAL_0:2;
set A = { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } ;
set B = { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } ;
A5: i <= j -' 1 by A2, NAT_D:49;
A6: { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } = { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))}
proof
thus { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } c= { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} :: according to XBOOLE_0:def_10 ::_thesis: { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} c= { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } or e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} )
assume e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))}
then consider k being Element of NAT such that
A7: e = LSeg (f,k) and
A8: i <= k and
A9: k < j ;
k <= j -' 1 by A9, NAT_D:49;
then ( j -' 1 = k or k < j -' 1 ) by XXREAL_0:1;
then ( e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } or e in {(LSeg (f,(j -' 1)))} ) by A7, A8, TARSKI:def_1;
hence e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} by XBOOLE_0:def_3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} or e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } )
A10: j -' 1 <= j by NAT_D:35;
assume A11: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) }
percases ( e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } or e in {(LSeg (f,(j -' 1)))} ) by A11, XBOOLE_0:def_3;
suppose e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) }
then consider k being Element of NAT such that
A12: e = LSeg (f,k) and
A13: i <= k and
A14: k < j -' 1 ;
k < j by A10, A14, XXREAL_0:2;
hence e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } by A12, A13; ::_thesis: verum
end;
supposeA15: e in {(LSeg (f,(j -' 1)))} ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) }
1 <= j -' 1 by A1, A5, XXREAL_0:2;
then A16: j -' 1 < j by NAT_D:51;
e = LSeg (f,(j -' 1)) by A15, TARSKI:def_1;
hence e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } by A5, A16; ::_thesis: verum
end;
end;
end;
thus L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } by A1, A2, A3, SPRECT_2:14
.= (union { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } ) \/ (union {(LSeg (f,(j -' 1)))}) by A6, ZFMISC_1:78
.= (union { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } ) \/ (LSeg (f,(j -' 1))) by ZFMISC_1:25
.= (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1))) by A1, A5, A4, SPRECT_2:14 ; ::_thesis: verum
end;
theorem :: SPRECT_3:21
for f, g being FinSequence of (TOP-REAL 2) st f is being_S-Seq & g is being_S-Seq & ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) & L~ f misses L~ g & (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ f) = {(f /. (len f))} & (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ g) = {(g /. 1)} holds
f ^ g is being_S-Seq
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq & g is being_S-Seq & ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) & L~ f misses L~ g & (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ f) = {(f /. (len f))} & (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ g) = {(g /. 1)} implies f ^ g is being_S-Seq )
assume that
A1: f is being_S-Seq and
A2: g is being_S-Seq and
A3: ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) and
A4: L~ f misses L~ g and
A5: (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ f) = {(f /. (len f))} and
A6: (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ g) = {(g /. 1)} ; ::_thesis: f ^ g is being_S-Seq
A7: len g >= 2 by A2, TOPREAL1:def_8;
then A8: len g >= 1 by XXREAL_0:2;
then 1 in dom g by FINSEQ_3:25;
then A9: g /. 1 in L~ g by A7, GOBOARD1:1;
set h = <*(f /. (len f))*> ^ g;
A10: len f >= 2 by A1, TOPREAL1:def_8;
then 1 <= len f by XXREAL_0:2;
then A11: len f in dom f by FINSEQ_3:25;
then A12: f . (len f) = f /. (len f) by PARTFUN1:def_6
.= (<*(f /. (len f))*> ^ g) . 1 by FINSEQ_1:41 ;
A13: len (<*(f /. (len f))*> ^ g) = (len <*(f /. (len f))*>) + (len g) by FINSEQ_1:22
.= (len g) + 1 by FINSEQ_1:39 ;
then len (<*(f /. (len f))*> ^ g) >= 1 + 1 by A8, XREAL_1:6;
then A14: mid ((<*(f /. (len f))*> ^ g),2,(len (<*(f /. (len f))*> ^ g))) = ((<*(f /. (len f))*> ^ g) /^ ((1 + 1) -' 1)) | (((len (<*(f /. (len f))*> ^ g)) -' 2) + 1) by FINSEQ_6:def_3
.= ((<*(f /. (len f))*> ^ g) /^ 1) | (((len (<*(f /. (len f))*> ^ g)) -' 2) + 1) by NAT_D:34
.= g | (((len (<*(f /. (len f))*> ^ g)) -' 2) + 1) by FINSEQ_6:45
.= g | ((((len (<*(f /. (len f))*> ^ g)) -' 1) -' 1) + 1) by NAT_D:45
.= g | (((len g) -' 1) + 1) by A13, NAT_D:34
.= g | (len g) by A7, XREAL_1:235, XXREAL_0:2
.= g by FINSEQ_1:58 ;
f /. (len f) in L~ f by A10, A11, GOBOARD1:1;
then f /. (len f) <> g /. 1 by A4, A9, XBOOLE_0:3;
then A15: <*(f /. (len f))*> ^ g is being_S-Seq by A2, A3, A6, SPRECT_2:60;
(L~ f) /\ (L~ (<*(f /. (len f))*> ^ g)) = (L~ f) /\ ((LSeg ((f /. (len f)),(g /. 1))) \/ (L~ g)) by A2, SPPOL_2:20
.= ((L~ f) /\ (LSeg ((f /. (len f)),(g /. 1)))) \/ ((L~ f) /\ (L~ g)) by XBOOLE_1:23
.= ((L~ f) /\ (LSeg ((f /. (len f)),(g /. 1)))) \/ {} by A4, XBOOLE_0:def_7
.= {((<*(f /. (len f))*> ^ g) . 1)} by A5, A11, A12, PARTFUN1:def_6 ;
hence f ^ g is being_S-Seq by A1, A12, A15, A14, JORDAN3:38; ::_thesis: verum
end;
theorem :: SPRECT_3:22
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
(R_Cut (f,p)) /. 1 = 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
(R_Cut (f,p)) /. 1 = f /. 1
let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies (R_Cut (f,p)) /. 1 = f /. 1 )
set i = Index (p,f);
assume A1: p in L~ f ; ::_thesis: (R_Cut (f,p)) /. 1 = f /. 1
then A2: 1 <= Index (p,f) by JORDAN3:8;
Index (p,f) <= len f by A1, JORDAN3:8;
then f <> {} by A2;
then A3: 1 in dom f by FINSEQ_5:6;
( p = f . 1 or p <> f . 1 ) ;
then ( len (R_Cut (f,p)) = Index (p,f) or len (R_Cut (f,p)) = (Index (p,f)) + 1 ) by A1, JORDAN3:25;
then 1 <= len (R_Cut (f,p)) by A1, JORDAN3:8, NAT_1:11;
hence (R_Cut (f,p)) /. 1 = (R_Cut (f,p)) . 1 by FINSEQ_4:15
.= f . 1 by A1, A2, JORDAN3:24
.= f /. 1 by A3, PARTFUN1:def_6 ;
::_thesis: verum
end;
theorem :: SPRECT_3:23
for j being Element of NAT
for f being S-Sequence_in_R2
for p, q being Point of (TOP-REAL 2) st 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg ((f /. j),p) holds
LE q,p, L~ f,f /. 1,f /. (len f)
proof
let j be Element of NAT ; ::_thesis: for f being S-Sequence_in_R2
for p, q being Point of (TOP-REAL 2) st 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg ((f /. j),p) holds
LE q,p, L~ f,f /. 1,f /. (len f)
let f be S-Sequence_in_R2; ::_thesis: for p, q being Point of (TOP-REAL 2) st 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg ((f /. j),p) holds
LE q,p, L~ f,f /. 1,f /. (len f)
let p, q be Point of (TOP-REAL 2); ::_thesis: ( 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg ((f /. j),p) implies LE q,p, L~ f,f /. 1,f /. (len f) )
assume that
A1: 1 <= j and
A2: j < len f and
A3: p in LSeg (f,j) and
A4: q in LSeg ((f /. j),p) ; ::_thesis: LE q,p, L~ f,f /. 1,f /. (len f)
A5: j + 1 <= len f by A2, NAT_1:13;
then A6: LSeg (f,j) = LSeg ((f /. j),(f /. (j + 1))) by A1, TOPREAL1:def_3;
A7: f /. j in LSeg (f,j) by A1, A5, TOPREAL1:21;
then A8: LSeg ((f /. j),p) c= LSeg (f,j) by A3, A6, TOPREAL1:6;
then A9: q in LSeg (f,j) by A4;
A10: LSeg (f,j) c= L~ f by TOPREAL3:19;
percases ( p = q or q <> p ) ;
suppose p = q ; ::_thesis: LE q,p, L~ f,f /. 1,f /. (len f)
hence LE q,p, L~ f,f /. 1,f /. (len f) by A3, A10, JORDAN5C:9; ::_thesis: verum
end;
supposeA11: q <> p ; ::_thesis: LE q,p, L~ f,f /. 1,f /. (len f)
for i, j being Element of NAT st q in LSeg (f,i) & p in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q,p,f /. i,f /. (i + 1) ) )
proof
1 <= j + 1 by NAT_1:11;
then A12: j + 1 in dom f by A5, FINSEQ_3:25;
let i1, i2 be Element of NAT ; ::_thesis: ( q in LSeg (f,i1) & p in LSeg (f,i2) & 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f implies ( i1 <= i2 & ( i1 = i2 implies LE q,p,f /. i1,f /. (i1 + 1) ) ) )
assume that
A13: q in LSeg (f,i1) and
A14: p in LSeg (f,i2) and
1 <= i1 and
A15: i1 + 1 <= len f and
A16: 1 <= i2 and
i2 + 1 <= len f ; ::_thesis: ( i1 <= i2 & ( i1 = i2 implies LE q,p,f /. i1,f /. (i1 + 1) ) )
A17: p in (LSeg (f,i2)) /\ (LSeg (f,j)) by A3, A14, XBOOLE_0:def_4;
then A18: LSeg (f,i2) meets LSeg (f,j) by XBOOLE_0:4;
then A19: j + 1 >= i2 by TOPREAL1:def_7;
A20: q in (LSeg (f,i1)) /\ (LSeg (f,j)) by A4, A8, A13, XBOOLE_0:def_4;
then A21: LSeg (f,i1) meets LSeg (f,j) by XBOOLE_0:4;
then A22: i1 + 1 >= j by TOPREAL1:def_7;
A23: now__::_thesis:_not_i2_+_1_=_j
assume A24: i2 + 1 = j ; ::_thesis: contradiction
i2 + (1 + 1) = (i2 + 1) + 1 ;
then i2 + 2 <= len f by A2, A24, NAT_1:13;
then p in {(f /. j)} by A16, A17, A24, TOPREAL1:def_6;
then p = f /. j by TARSKI:def_1;
then q in {p} by A4, RLTOPSP1:70;
hence contradiction by A11, TARSKI:def_1; ::_thesis: verum
end;
A25: now__::_thesis:_(_i2_+_1_>_j_&_j_+_1_>_i2_implies_i2_=_j_)
assume that
A26: i2 + 1 > j and
A27: j + 1 > i2 ; ::_thesis: i2 = j
A28: j <= i2 by A26, NAT_1:13;
i2 <= j by A27, NAT_1:13;
hence i2 = j by A28, XXREAL_0:1; ::_thesis: verum
end;
i2 + 1 >= j by A18, TOPREAL1:def_7;
then ( i2 + 1 = j or i2 = j or j + 1 = i2 ) by A25, A19, XXREAL_0:1;
then A29: i2 >= j by A23, NAT_1:11;
A30: now__::_thesis:_(_i1_+_1_>_j_&_j_+_1_>_i1_implies_i1_=_j_)
assume that
A31: i1 + 1 > j and
A32: j + 1 > i1 ; ::_thesis: i1 = j
A33: j <= i1 by A31, NAT_1:13;
i1 <= j by A32, NAT_1:13;
hence i1 = j by A33, XXREAL_0:1; ::_thesis: verum
end;
A34: j in dom f by A1, A2, FINSEQ_3:25;
A35: now__::_thesis:_not_f_/._(j_+_1)_=_f_/._j
assume f /. (j + 1) = f /. j ; ::_thesis: contradiction
then j = j + 1 by A12, A34, PARTFUN2:10;
hence contradiction ; ::_thesis: verum
end;
A36: now__::_thesis:_not_i1_=_j_+_1
A37: j + (1 + 1) = (j + 1) + 1 ;
assume i1 = j + 1 ; ::_thesis: contradiction
then q in {(f /. (j + 1))} by A1, A15, A20, A37, TOPREAL1:def_6;
then q = f /. (j + 1) by TARSKI:def_1;
hence contradiction by A3, A4, A6, A7, A11, A35, SPPOL_1:7, TOPREAL1:6; ::_thesis: verum
end;
A38: j + 1 >= i1 by A21, TOPREAL1:def_7;
then ( i1 + 1 = j or i1 = j or j + 1 = i1 ) by A30, A22, XXREAL_0:1;
then i1 <= j by A36, NAT_1:11;
hence i1 <= i2 by A29, XXREAL_0:2; ::_thesis: ( i1 = i2 implies LE q,p,f /. i1,f /. (i1 + 1) )
assume A39: i1 = i2 ; ::_thesis: LE q,p,f /. i1,f /. (i1 + 1)
not p in LSeg ((f /. j),q) by A4, A11, Th6;
then not LE p,q,f /. j,f /. (j + 1) by JORDAN3:30;
then LT q,p,f /. j,f /. (j + 1) by A3, A6, A13, A23, A30, A22, A38, A35, A36, A39, JORDAN3:28, XXREAL_0:1;
hence LE q,p,f /. i1,f /. (i1 + 1) by A23, A30, A22, A38, A36, A39, JORDAN3:def_6, XXREAL_0:1; ::_thesis: verum
end;
hence LE q,p, L~ f,f /. 1,f /. (len f) by A3, A9, A10, A11, JORDAN5C:30; ::_thesis: verum
end;
end;
end;
begin
theorem Th24: :: SPRECT_3:24
for f being non constant standard special_circular_sequence holds
( LeftComp f is open & RightComp f is open )
proof
let f be non constant standard special_circular_sequence; ::_thesis: ( LeftComp f is open & RightComp f is open )
LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1;
hence LeftComp f is open by Th8; ::_thesis: RightComp f is open
RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2;
hence RightComp f is open by Th8; ::_thesis: verum
end;
registration
let f be non constant standard special_circular_sequence;
cluster L~ f -> non horizontal non vertical ;
coherence
( not L~ f is vertical & not L~ f is horizontal )
proof
W-bound (L~ f) <> E-bound (L~ f) by TOPREAL5:17;
hence not L~ f is vertical by SPRECT_1:15; ::_thesis: not L~ f is horizontal
S-bound (L~ f) <> N-bound (L~ f) by TOPREAL5:16;
hence not L~ f is horizontal by SPRECT_1:16; ::_thesis: verum
end;
cluster LeftComp f -> being_Region ;
coherence
LeftComp f is being_Region
proof
thus LeftComp f is open by Th24; :: according to TOPREAL4:def_3 ::_thesis: LeftComp f is connected
LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1;
then consider A being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that
A1: A = LeftComp f and
A2: A is a_component by CONNSP_1:def_6;
A is connected by A2, CONNSP_1:def_5;
hence LeftComp f is connected by A1, CONNSP_1:23; ::_thesis: verum
end;
cluster RightComp f -> being_Region ;
coherence
RightComp f is being_Region
proof
thus RightComp f is open by Th24; :: according to TOPREAL4:def_3 ::_thesis: RightComp f is connected
RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2;
then consider A being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that
A3: A = RightComp f and
A4: A is a_component by CONNSP_1:def_6;
A is connected by A4, CONNSP_1:def_5;
hence RightComp f is connected by A3, CONNSP_1:23; ::_thesis: verum
end;
end;
theorem Th25: :: SPRECT_3:25
for f being non constant standard special_circular_sequence holds RightComp f misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: RightComp f misses L~ f
(L~ f) ` = (LeftComp f) \/ (RightComp f) by GOBRD12:10;
then RightComp f c= (L~ f) ` by XBOOLE_1:7;
hence RightComp f misses L~ f by SUBSET_1:23; ::_thesis: verum
end;
theorem Th26: :: SPRECT_3:26
for f being non constant standard special_circular_sequence holds LeftComp f misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: LeftComp f misses L~ f
(L~ f) ` = (LeftComp f) \/ (RightComp f) by GOBRD12:10;
then LeftComp f c= (L~ f) ` by XBOOLE_1:7;
hence LeftComp f misses L~ f by SUBSET_1:23; ::_thesis: verum
end;
theorem Th27: :: SPRECT_3:27
for f being non constant standard special_circular_sequence holds i_w_n f < i_e_n f
proof
let f be non constant standard special_circular_sequence; ::_thesis: i_w_n f < i_e_n f
set G = GoB f;
A1: i_w_n f <= len (GoB f) by JORDAN5D:45;
A2: (GoB f) * ((i_w_n f),(width (GoB f))) = N-min (L~ f) by JORDAN5D:def_7;
assume A3: i_w_n f >= i_e_n f ; ::_thesis: contradiction
A4: 1 <= i_e_n f by JORDAN5D:45;
A5: (N-min (L~ f)) `1 < (N-max (L~ f)) `1 by SPRECT_2:51;
A6: (GoB f) * ((i_e_n f),(width (GoB f))) = N-max (L~ f) by JORDAN5D:def_8;
then i_w_n f <> i_e_n f by A5, JORDAN5D:def_7;
then A7: i_w_n f > i_e_n f by A3, XXREAL_0:1;
width (GoB f) > 1 by GOBOARD7:33;
hence contradiction by A1, A2, A4, A6, A5, A7, GOBOARD5:3; ::_thesis: verum
end;
theorem Th28: :: SPRECT_3:28
for f being non constant standard special_circular_sequence ex i being Element of NAT st
( 1 <= i & i < len (GoB f) & N-min (L~ f) = (GoB f) * (i,(width (GoB f))) )
proof
let f be non constant standard special_circular_sequence; ::_thesis: ex i being Element of NAT st
( 1 <= i & i < len (GoB f) & N-min (L~ f) = (GoB f) * (i,(width (GoB f))) )
take i = i_w_n f; ::_thesis: ( 1 <= i & i < len (GoB f) & N-min (L~ f) = (GoB f) * (i,(width (GoB f))) )
thus 1 <= i by JORDAN5D:45; ::_thesis: ( i < len (GoB f) & N-min (L~ f) = (GoB f) * (i,(width (GoB f))) )
i_e_n f <= len (GoB f) by JORDAN5D:45;
hence i < len (GoB f) by Th27, XXREAL_0:2; ::_thesis: N-min (L~ f) = (GoB f) * (i,(width (GoB f)))
thus N-min (L~ f) = (GoB f) * (i,(width (GoB f))) by JORDAN5D:def_7; ::_thesis: verum
end;
theorem Th29: :: SPRECT_3:29
for i being Element of NAT
for f being non constant standard clockwise_oriented special_circular_sequence st i in dom (GoB f) & f /. 1 = (GoB f) * (i,(width (GoB f))) & f /. 1 = N-min (L~ f) holds
( f /. 2 = (GoB f) * ((i + 1),(width (GoB f))) & f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) )
proof
let i be Element of NAT ; ::_thesis: for f being non constant standard clockwise_oriented special_circular_sequence st i in dom (GoB f) & f /. 1 = (GoB f) * (i,(width (GoB f))) & f /. 1 = N-min (L~ f) holds
( f /. 2 = (GoB f) * ((i + 1),(width (GoB f))) & f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) )
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( i in dom (GoB f) & f /. 1 = (GoB f) * (i,(width (GoB f))) & f /. 1 = N-min (L~ f) implies ( f /. 2 = (GoB f) * ((i + 1),(width (GoB f))) & f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) ) )
assume that
A1: i in dom (GoB f) and
A2: f /. 1 = (GoB f) * (i,(width (GoB f))) and
A3: f /. 1 = N-min (L~ f) ; ::_thesis: ( f /. 2 = (GoB f) * ((i + 1),(width (GoB f))) & f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) )
A4: i <= len (GoB f) by A1, FINSEQ_3:25;
4 < len f by GOBOARD7:34;
then A5: ((len f) -' 1) + 1 = len f by XREAL_1:235, XXREAL_0:2;
A6: f /. (len f) = f /. 1 by FINSEQ_6:def_1;
A7: 1 <= len f by GOBOARD7:34, XXREAL_0:2;
then A8: 1 in dom f by FINSEQ_3:25;
A9: 1 <= width (GoB f) by GOBRD11:34;
A10: f /. 2 in N-most (L~ f) by A3, SPRECT_2:30;
A11: 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
then A12: 1 + 1 in dom f by FINSEQ_3:25;
then consider i1, j1 being Element of NAT such that
A13: [i1,j1] in Indices (GoB f) and
A14: f /. 2 = (GoB f) * (i1,j1) by GOBOARD2:14;
A15: 1 <= j1 by A13, MATRIX_1:38;
A16: j1 <= width (GoB f) by A13, MATRIX_1:38;
A17: 1 <= i1 by A13, MATRIX_1:38;
A18: i1 <= len (GoB f) by A13, MATRIX_1:38;
now__::_thesis:_not_j1_<_width_(GoB_f)
A19: (f /. 2) `2 = (N-min (L~ f)) `2 by A10, PSCOMP_1:39
.= N-bound (L~ f) by EUCLID:52 ;
assume A20: j1 < width (GoB f) ; ::_thesis: contradiction
((GoB f) * (i1,(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A9, A17, A18, GOBOARD5:1
.= N-bound (L~ f) by JORDAN5D:40 ;
hence contradiction by A14, A15, A17, A18, A20, A19, GOBOARD5:4; ::_thesis: verum
end;
then A21: j1 = width (GoB f) by A16, XXREAL_0:1;
A22: now__::_thesis:_not_i_>_i1
assume i > i1 ; ::_thesis: contradiction
then (f /. 2) `1 < (N-min (L~ f)) `1 by A2, A3, A14, A4, A15, A17, A21, GOBOARD5:3;
hence contradiction by A10, PSCOMP_1:39; ::_thesis: verum
end;
A23: 1 <= i by A1, FINSEQ_3:25;
then A24: [i,(width (GoB f))] in Indices (GoB f) by A9, A4, MATRIX_1:36;
(abs (i - i1)) + 0 = (abs (i - i1)) + (abs ((width (GoB f)) - (width (GoB f)))) by ABSVALUE:2
.= 1 by A2, A12, A13, A14, A8, A24, A21, GOBOARD5:12 ;
hence A25: f /. 2 = (GoB f) * ((i + 1),(width (GoB f))) by A14, A21, A22, SEQM_3:41; ::_thesis: f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1))
A26: (len f) -' 1 <= len f by NAT_D:44;
1 <= (len f) -' 1 by A11, NAT_D:49;
then A27: (len f) -' 1 in dom f by A26, FINSEQ_3:25;
then consider i2, j2 being Element of NAT such that
A28: [i2,j2] in Indices (GoB f) and
A29: f /. ((len f) -' 1) = (GoB f) * (i2,j2) by GOBOARD2:14;
A30: 1 <= i2 by A28, MATRIX_1:38;
A31: j2 <= width (GoB f) by A28, MATRIX_1:38;
A32: i2 <= len (GoB f) by A28, MATRIX_1:38;
len f in dom f by A7, FINSEQ_3:25;
then A33: (abs (i2 - i)) + (abs (j2 - (width (GoB f)))) = 1 by A2, A24, A6, A5, A27, A28, A29, GOBOARD5:12;
percases ( ( abs (i2 - i) = 1 & j2 = width (GoB f) ) or ( abs (j2 - (width (GoB f))) = 1 & i2 = i ) ) by A33, SEQM_3:42;
supposethat A34: abs (i2 - i) = 1 and
A35: j2 = width (GoB f) ; ::_thesis: f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1))
(f /. ((len f) -' 1)) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A9, A29, A30, A32, A35, GOBOARD5:1
.= (N-min (L~ f)) `2 by A2, A3, A9, A23, A4, GOBOARD5:1
.= N-bound (L~ f) by EUCLID:52 ;
then A36: f /. ((len f) -' 1) in N-most (L~ f) by A11, A27, GOBOARD1:1, SPRECT_2:10;
now__::_thesis:_contradiction
percases ( i > i2 or i + 1 = i2 ) by A34, SEQM_3:41;
suppose i > i2 ; ::_thesis: contradiction
then (f /. ((len f) -' 1)) `1 < (N-min (L~ f)) `1 by A2, A3, A9, A4, A29, A30, A35, GOBOARD5:3;
hence contradiction by A36, PSCOMP_1:39; ::_thesis: verum
end;
suppose i + 1 = i2 ; ::_thesis: contradiction
then 2 >= (len f) -' 1 by A25, A26, A29, A35, GOBOARD7:37;
then 2 + 1 >= len f by NAT_D:52;
hence contradiction by GOBOARD7:34, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) ; ::_thesis: verum
end;
supposethat A37: abs (j2 - (width (GoB f))) = 1 and
A38: i2 = i ; ::_thesis: f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1))
width (GoB f) in NAT ;
then width (GoB f) = j2 + 1 by A31, A37, SEQM_3:41;
hence f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) by A29, A38, NAT_D:34; ::_thesis: verum
end;
end;
end;
theorem :: SPRECT_3:30
for i, j being Element of NAT
for f being non constant standard special_circular_sequence st 1 <= i & i < j & j <= len f & f /. 1 in L~ (mid (f,i,j)) & not i = 1 holds
j = len f
proof
let i, j be Element of NAT ; ::_thesis: for f being non constant standard special_circular_sequence st 1 <= i & i < j & j <= len f & f /. 1 in L~ (mid (f,i,j)) & not i = 1 holds
j = len f
let f be non constant standard special_circular_sequence; ::_thesis: ( 1 <= i & i < j & j <= len f & f /. 1 in L~ (mid (f,i,j)) & not i = 1 implies j = len f )
assume that
A1: 1 <= i and
A2: i < j and
A3: j <= len f ; ::_thesis: ( not f /. 1 in L~ (mid (f,i,j)) or i = 1 or j = len f )
1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
then A4: f /. 1 in LSeg (f,1) by TOPREAL1:21;
assume f /. 1 in L~ (mid (f,i,j)) ; ::_thesis: ( i = 1 or j = len f )
then consider n being Element of NAT such that
A5: 1 <= n and
A6: n + 1 <= len (mid (f,i,j)) and
A7: f /. 1 in LSeg ((mid (f,i,j)),n) by SPPOL_2:13;
n < len (mid (f,i,j)) by A6, NAT_1:13;
then A8: n < (j -' i) + 1 by A1, A2, A3, JORDAN4:8;
then LSeg ((mid (f,i,j)),n) = LSeg (f,((n + i) -' 1)) by A1, A2, A3, A5, JORDAN4:19;
then A9: f /. 1 in (LSeg (f,1)) /\ (LSeg (f,((n + i) -' 1))) by A7, A4, XBOOLE_0:def_4;
then A10: LSeg (f,1) meets LSeg (f,((n + i) -' 1)) by XBOOLE_0:4;
assume that
A11: i <> 1 and
A12: j <> len f ; ::_thesis: contradiction
percases ( 1 + 1 >= (n + i) -' 1 or ((n + i) -' 1) + 1 >= len f ) by A10, GOBOARD5:def_4;
suppose 1 + 1 >= (n + i) -' 1 ; ::_thesis: contradiction
then A13: n + i <= 2 + 1 by NAT_D:52;
i > 1 by A1, A11, XXREAL_0:1;
then A14: i >= 1 + 1 by NAT_1:13;
n + i >= i + 1 by A5, XREAL_1:6;
then i + 1 <= 2 + 1 by A13, XXREAL_0:2;
then i <= 2 by XREAL_1:6;
then A15: i = 2 by A14, XXREAL_0:1;
then n <= 1 by A13, XREAL_1:6;
then n = 1 by A5, XXREAL_0:1;
then A16: (n + i) -' 1 = 2 by A15, NAT_D:34;
A17: 2 < len f by GOBOARD7:34, XXREAL_0:2;
1 + 2 <= len f by GOBOARD7:34, XXREAL_0:2;
then (LSeg (f,1)) /\ (LSeg (f,(1 + 1))) = {(f /. (1 + 1))} by TOPREAL1:def_6;
then f /. 1 = f /. 2 by A9, A16, TARSKI:def_1;
hence contradiction by A17, GOBOARD7:36; ::_thesis: verum
end;
supposeA18: ((n + i) -' 1) + 1 >= len f ; ::_thesis: contradiction
n <= n + i by NAT_1:11;
then A19: len f <= n + i by A5, A18, XREAL_1:235, XXREAL_0:2;
((j -' i) + 1) + i = ((j -' i) + i) + 1
.= j + 1 by A2, XREAL_1:235 ;
then n + i < j + 1 by A8, XREAL_1:6;
then A20: n + i <= j by NAT_1:13;
j < len f by A3, A12, XXREAL_0:1;
hence contradiction by A19, A20, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
theorem :: SPRECT_3:31
for f being non constant standard clockwise_oriented special_circular_sequence st f /. 1 = N-min (L~ f) holds
LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f))
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( f /. 1 = N-min (L~ f) implies LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f)) )
A1: N-most (L~ f) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by XBOOLE_1:17;
assume A2: f /. 1 = N-min (L~ f) ; ::_thesis: LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f))
then A3: f /. 2 in N-most (L~ f) by SPRECT_2:30;
A4: LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) c= L~ (SpStSeq (L~ f)) by Th14;
f /. 1 in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A2, Th15;
then LSeg ((f /. 1),(f /. 2)) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A3, A1, TOPREAL1:6;
hence LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f)) by A4, XBOOLE_1:1; ::_thesis: verum
end;
begin
theorem Th32: :: SPRECT_3:32
for f being rectangular FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) holds
( not p in L~ f or p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) )
proof
let f be rectangular FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) holds
( not p in L~ f or p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) )
let p be Point of (TOP-REAL 2); ::_thesis: ( not p in L~ f or p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) )
assume A1: p in L~ f ; ::_thesis: ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) )
consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that
A2: f = SpStSeq D by SPRECT_1:def_2;
L~ f = ((LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D)))) \/ ((LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D)))) by A2, SPRECT_1:41;
then A3: ( p in (LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D))) or p in (LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D))) ) by A1, XBOOLE_0:def_3;
percases ( p in LSeg ((NW-corner D),(NE-corner D)) or p in LSeg ((NE-corner D),(SE-corner D)) or p in LSeg ((SE-corner D),(SW-corner D)) or p in LSeg ((SW-corner D),(NW-corner D)) ) by A3, XBOOLE_0:def_3;
supposeA4: p in LSeg ((NW-corner D),(NE-corner D)) ; ::_thesis: ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) )
A5: N-bound (L~ (SpStSeq D)) = N-bound D by SPRECT_1:60;
then A6: (NE-corner D) `2 = N-bound (L~ f) by A2, EUCLID:52;
(NW-corner D) `2 = N-bound (L~ f) by A2, A5, EUCLID:52;
hence ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) by A4, A6, GOBOARD7:6; ::_thesis: verum
end;
supposeA7: p in LSeg ((NE-corner D),(SE-corner D)) ; ::_thesis: ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) )
A8: E-bound (L~ (SpStSeq D)) = E-bound D by SPRECT_1:61;
then A9: (SE-corner D) `1 = E-bound (L~ f) by A2, EUCLID:52;
(NE-corner D) `1 = E-bound (L~ f) by A2, A8, EUCLID:52;
hence ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) by A7, A9, GOBOARD7:5; ::_thesis: verum
end;
supposeA10: p in LSeg ((SE-corner D),(SW-corner D)) ; ::_thesis: ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) )
A11: S-bound (L~ (SpStSeq D)) = S-bound D by SPRECT_1:59;
then A12: (SW-corner D) `2 = S-bound (L~ f) by A2, EUCLID:52;
(SE-corner D) `2 = S-bound (L~ f) by A2, A11, EUCLID:52;
hence ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) by A10, A12, GOBOARD7:6; ::_thesis: verum
end;
supposeA13: p in LSeg ((SW-corner D),(NW-corner D)) ; ::_thesis: ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) )
A14: W-bound (L~ (SpStSeq D)) = W-bound D by SPRECT_1:58;
then A15: (NW-corner D) `1 = W-bound (L~ f) by A2, EUCLID:52;
(SW-corner D) `1 = W-bound (L~ f) by A2, A14, EUCLID:52;
hence ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) by A13, A15, GOBOARD7:5; ::_thesis: verum
end;
end;
end;
registration
cluster non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like V236( the U1 of (TOP-REAL 2)) special unfolded s.c.c. rectangular for FinSequence of the U1 of (TOP-REAL 2);
existence
ex b1 being special_circular_sequence st b1 is rectangular
proof
set C = the non empty compact non horizontal non vertical Subset of (TOP-REAL 2);
SpStSeq the non empty compact non horizontal non vertical Subset of (TOP-REAL 2) is special_circular_sequence ;
hence ex b1 being special_circular_sequence st b1 is rectangular ; ::_thesis: verum
end;
end;
theorem Th33: :: SPRECT_3:33
for f being rectangular special_circular_sequence
for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
L~ f meets L~ g
proof
let f be rectangular special_circular_sequence; ::_thesis: for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
L~ f meets L~ g
let g be S-Sequence_in_R2; ::_thesis: ( g /. 1 in LeftComp f & g /. (len g) in RightComp f implies L~ f meets L~ g )
assume that
A1: g /. 1 in LeftComp f and
A2: g /. (len g) in RightComp f ; ::_thesis: L~ f meets L~ g
A3: len g >= 2 by TOPREAL1:def_8;
then g /. 1 in L~ g by JORDAN3:1;
then g /. 1 in (LeftComp f) /\ (L~ g) by A1, XBOOLE_0:def_4;
then A4: LeftComp f meets L~ g by XBOOLE_0:4;
g /. (len g) in L~ g by A3, JORDAN3:1;
then g /. (len g) in (RightComp f) /\ (L~ g) by A2, XBOOLE_0:def_4;
then A5: RightComp f meets L~ g by XBOOLE_0:4;
A6: LeftComp f misses RightComp f by SPRECT_1:88;
assume L~ f misses L~ g ; ::_thesis: contradiction
then L~ g c= (L~ f) ` by SUBSET_1:23;
then A7: L~ g c= (LeftComp f) \/ (RightComp f) by GOBRD12:10;
A8: L~ g is_an_arc_of g /. 1,g /. (len g) by TOPREAL1:25;
A9: RightComp f is open by Th24;
LeftComp f is open by Th24;
hence contradiction by A7, A9, A4, A5, A6, A8, JORDAN6:10, TOPREAL5:1; ::_thesis: verum
end;
theorem Th34: :: SPRECT_3:34
for f being rectangular special_circular_sequence holds SpStSeq (L~ f) = f
proof
let f be rectangular special_circular_sequence; ::_thesis: SpStSeq (L~ f) = f
set C = L~ f;
set g = SpStSeq (L~ f);
consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that
A1: f = SpStSeq D by SPRECT_1:def_2;
A2: 5 = len f by SPRECT_1:82;
SpStSeq (L~ f) = <*(NW-corner (L~ f)),(NE-corner (L~ f)),(SE-corner (L~ f))*> ^ <*(SW-corner (L~ f)),(NW-corner (L~ f))*> by SPRECT_1:def_1;
then A3: len (SpStSeq (L~ f)) = (len <*(NW-corner (L~ f)),(NE-corner (L~ f)),(SE-corner (L~ f))*>) + (len <*(SW-corner (L~ f)),(NW-corner (L~ f))*>) by FINSEQ_1:22
.= 3 + (len <*(SW-corner (L~ f)),(NW-corner (L~ f))*>) by FINSEQ_1:45
.= 3 + 2 by FINSEQ_1:44 ;
A4: for i being Nat st i in dom f holds
f /. i = (SpStSeq (L~ f)) /. i
proof
let i be Nat; ::_thesis: ( i in dom f implies f /. i = (SpStSeq (L~ f)) /. i )
assume A5: i in dom f ; ::_thesis: f /. i = (SpStSeq (L~ f)) /. i
then A6: 0 <> i by FINSEQ_3:25;
A7: i <= len f by A5, FINSEQ_3:25;
A8: f /. 1 = W-max (L~ f) by SPRECT_1:83
.= NW-corner D by A1, SPRECT_1:75
.= NW-corner (L~ f) by A1, SPRECT_1:62
.= (SpStSeq (L~ f)) /. 1 by SPRECT_1:35 ;
percases ( i = 1 or i = 2 or i = 3 or i = 4 or i = 5 ) by A2, A6, A7, NAT_1:29;
suppose i = 1 ; ::_thesis: f /. i = (SpStSeq (L~ f)) /. i
hence f /. i = (SpStSeq (L~ f)) /. i by A8; ::_thesis: verum
end;
supposeA9: i = 2 ; ::_thesis: f /. i = (SpStSeq (L~ f)) /. i
hence f /. i = E-max (L~ f) by SPRECT_1:84
.= NE-corner D by A1, SPRECT_1:79
.= NE-corner (L~ f) by A1, SPRECT_1:63
.= (SpStSeq (L~ f)) /. i by A9, SPRECT_1:36 ;
::_thesis: verum
end;
supposeA10: i = 3 ; ::_thesis: f /. i = (SpStSeq (L~ f)) /. i
hence f /. i = E-min (L~ f) by SPRECT_1:85
.= SE-corner D by A1, SPRECT_1:78
.= SE-corner (L~ f) by A1, SPRECT_1:65
.= (SpStSeq (L~ f)) /. i by A10, SPRECT_1:37 ;
::_thesis: verum
end;
supposeA11: i = 4 ; ::_thesis: f /. i = (SpStSeq (L~ f)) /. i
hence f /. i = W-min (L~ f) by SPRECT_1:86
.= SW-corner D by A1, SPRECT_1:74
.= SW-corner (L~ f) by A1, SPRECT_1:64
.= (SpStSeq (L~ f)) /. i by A11, SPRECT_1:38 ;
::_thesis: verum
end;
supposeA12: i = 5 ; ::_thesis: f /. i = (SpStSeq (L~ f)) /. i
hence f /. i = f /. 1 by A2, FINSEQ_6:def_1
.= (SpStSeq (L~ f)) /. i by A3, A8, A12, FINSEQ_6:def_1 ;
::_thesis: verum
end;
end;
end;
dom f = dom (SpStSeq (L~ f)) by A2, A3, FINSEQ_3:29;
hence SpStSeq (L~ f) = f by A4, FINSEQ_5:12; ::_thesis: verum
end;
theorem Th35: :: SPRECT_3:35
for f being rectangular special_circular_sequence holds L~ f = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) }
proof
let f be rectangular special_circular_sequence; ::_thesis: L~ f = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) }
set C = L~ f;
set E = { p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) } ;
set S = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) } ;
set N = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) } ;
set W = { p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) } ;
A1: LSeg ((SE-corner (L~ f)),(NE-corner (L~ f))) = { p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) } by SPRECT_1:23;
A2: LSeg ((SW-corner (L~ f)),(SE-corner (L~ f))) = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) } by SPRECT_1:24;
A3: LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))) = { p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) } by SPRECT_1:26;
A4: LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) } by SPRECT_1:25;
A5: L~ f = L~ (SpStSeq (L~ f)) by Th34;
thus L~ f c= { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } :: according to XBOOLE_0:def_10 ::_thesis: { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } c= L~ f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } )
assume A6: x in L~ f ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) }
then reconsider q = x as Point of (TOP-REAL 2) ;
q in ((LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))))) \/ ((LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))))) by A5, A6, SPRECT_1:41;
then ( q in (LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f)))) or q in (LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) ) by XBOOLE_0:def_3;
then ( q in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) or q in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) or q in LSeg ((SE-corner (L~ f)),(SW-corner (L~ f))) or q in LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))) ) by XBOOLE_0:def_3;
then ( ex p being Point of (TOP-REAL 2) st
( x = p & p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ex p being Point of (TOP-REAL 2) st
( x = p & p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ex p being Point of (TOP-REAL 2) st
( x = p & p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ex p being Point of (TOP-REAL 2) st
( x = p & p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) by A1, A2, A4, A3;
hence x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } or x in L~ f )
assume x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } ; ::_thesis: x in L~ f
then ex p being Point of (TOP-REAL 2) st
( x = p & ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) ) ;
then ( x in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) or x in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) or x in LSeg ((SE-corner (L~ f)),(SW-corner (L~ f))) or x in LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))) ) by A1, A2, A4, A3;
then ( x in (LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f)))) or x in (LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) ) by XBOOLE_0:def_3;
then x in ((LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))))) \/ ((LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))))) by XBOOLE_0:def_3;
hence x in L~ f by A5, SPRECT_1:41; ::_thesis: verum
end;
theorem Th36: :: SPRECT_3:36
for f being rectangular special_circular_sequence holds GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))
proof
let f be rectangular special_circular_sequence; ::_thesis: GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))
set G = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2));
set v1 = Incr (X_axis f);
set v2 = Incr (Y_axis f);
A1: f /. 2 = N-max (L~ f) by SPRECT_1:84;
A2: f /. 1 = N-min (L~ f) by SPRECT_1:83;
then A3: (f /. 1) `1 < (f /. 2) `1 by A1, SPRECT_2:51;
A4: (f /. 2) `2 = (f /. 1) `2 by A2, A1, PSCOMP_1:37;
A5: f /. 4 = S-min (L~ f) by SPRECT_1:86;
A6: f /. 3 = S-max (L~ f) by SPRECT_1:85;
then A7: (f /. 3) `2 = (f /. 4) `2 by A5, PSCOMP_1:53;
A8: len <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> = 3 by FINSEQ_1:45;
A9: len f = 5 by SPRECT_1:82;
then A10: f /. 1 = f /. 5 by FINSEQ_6:def_1;
set g = <*((f /. 1) `1),((f /. 2) `1)*>;
set h = <*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>;
A11: f /. 3 = E-min (L~ f) by SPRECT_1:85;
A12: f /. 2 = E-max (L~ f) by SPRECT_1:84;
then A13: (f /. 3) `1 = (f /. 2) `1 by A11, PSCOMP_1:45;
A14: len <*((f /. 1) `1),((f /. 2) `1)*> = 2 by FINSEQ_1:44;
A15: dom <*((f /. 1) `1),((f /. 2) `1)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
A16: <*((f /. 1) `1),((f /. 2) `1)*> is increasing
proof
A17: <*((f /. 1) `1),((f /. 2) `1)*> . 2 = (f /. 2) `1 by FINSEQ_1:44;
A18: <*((f /. 1) `1),((f /. 2) `1)*> . 1 = (f /. 1) `1 by FINSEQ_1:44;
let n be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: for b1 being Element of NAT holds
( not n in K74(<*((f /. 1) `1),((f /. 2) `1)*>) or not b1 in K74(<*((f /. 1) `1),((f /. 2) `1)*>) or b1 <= n or not K571(<*((f /. 1) `1),((f /. 2) `1)*>,b1) <= K571(<*((f /. 1) `1),((f /. 2) `1)*>,n) )
let m be Element of NAT ; ::_thesis: ( not n in K74(<*((f /. 1) `1),((f /. 2) `1)*>) or not m in K74(<*((f /. 1) `1),((f /. 2) `1)*>) or m <= n or not K571(<*((f /. 1) `1),((f /. 2) `1)*>,m) <= K571(<*((f /. 1) `1),((f /. 2) `1)*>,n) )
assume that
A19: n in dom <*((f /. 1) `1),((f /. 2) `1)*> and
A20: m in dom <*((f /. 1) `1),((f /. 2) `1)*> and
A21: n < m ; ::_thesis: not K571(<*((f /. 1) `1),((f /. 2) `1)*>,m) <= K571(<*((f /. 1) `1),((f /. 2) `1)*>,n)
A22: ( m = 1 or m = 2 ) by A15, A20, TARSKI:def_2;
( n = 1 or n = 2 ) by A15, A19, TARSKI:def_2;
hence <*((f /. 1) `1),((f /. 2) `1)*> . n < <*((f /. 1) `1),((f /. 2) `1)*> . m by A2, A1, A21, A18, A17, A22, SPRECT_2:51; ::_thesis: verum
end;
A23: f /. 4 = W-min (L~ f) by SPRECT_1:86;
A24: len (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) = (len <*((f /. 1) `1),((f /. 2) `1)*>) + (len <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) by FINSEQ_1:22
.= (len <*((f /. 1) `1),((f /. 2) `1)*>) + 3 by FINSEQ_1:45
.= 2 + 3 by FINSEQ_1:44
.= len f by SPRECT_1:82 ;
for n being Element of NAT st n in dom (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) holds
(<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1
proof
let n be Element of NAT ; ::_thesis: ( n in dom (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) implies (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1 )
assume A25: n in dom (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) ; ::_thesis: (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1
then A26: 1 <= n by FINSEQ_3:25;
A27: n <= 5 by A9, A24, A25, FINSEQ_3:25;
percases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A26, A27, NAT_1:29;
supposeA28: n = 1 ; ::_thesis: (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1
then n in dom <*((f /. 1) `1),((f /. 2) `1)*> by A14, FINSEQ_3:25;
hence (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = <*((f /. 1) `1),((f /. 2) `1)*> . 1 by A28, FINSEQ_1:def_7
.= (f /. n) `1 by A28, FINSEQ_1:44 ;
::_thesis: verum
end;
supposeA29: n = 2 ; ::_thesis: (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1
then n in dom <*((f /. 1) `1),((f /. 2) `1)*> by A14, FINSEQ_3:25;
hence (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = <*((f /. 1) `1),((f /. 2) `1)*> . 2 by A29, FINSEQ_1:def_7
.= (f /. n) `1 by A29, FINSEQ_1:44 ;
::_thesis: verum
end;
supposeA30: n = 3 ; ::_thesis: (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1
hence (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . (2 + 1)
.= <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> . 1 by A14, A8, FINSEQ_1:65
.= (f /. n) `1 by A30, FINSEQ_1:45 ;
::_thesis: verum
end;
supposeA31: n = 4 ; ::_thesis: (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1
hence (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . (2 + 2)
.= <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> . 2 by A14, A8, FINSEQ_1:65
.= (f /. n) `1 by A31, FINSEQ_1:45 ;
::_thesis: verum
end;
supposeA32: n = 5 ; ::_thesis: (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1
hence (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . (2 + 3)
.= <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> . 3 by A14, A8, FINSEQ_1:65
.= (f /. n) `1 by A32, FINSEQ_1:45 ;
::_thesis: verum
end;
end;
end;
then A33: X_axis f = <*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> by A24, GOBOARD1:def_1;
A34: rng <*((f /. 1) `1),((f /. 2) `1)*> = {((f /. 1) `1),((f /. 2) `1)} by FINSEQ_2:127;
A35: f /. 1 = W-max (L~ f) by SPRECT_1:83;
then A36: (f /. 4) `2 < (f /. 5) `2 by A23, A10, SPRECT_2:57;
{((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)} c= {((f /. 1) `1),((f /. 2) `1)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)} or x in {((f /. 1) `1),((f /. 2) `1)} )
assume A37: x in {((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)} ; ::_thesis: x in {((f /. 1) `1),((f /. 2) `1)}
percases ( x = (f /. 3) `1 or x = (f /. 4) `1 or x = (f /. 5) `1 ) by A37, ENUMSET1:def_1;
suppose x = (f /. 3) `1 ; ::_thesis: x in {((f /. 1) `1),((f /. 2) `1)}
then x = (f /. 2) `1 by A12, A11, PSCOMP_1:45;
hence x in {((f /. 1) `1),((f /. 2) `1)} by TARSKI:def_2; ::_thesis: verum
end;
suppose x = (f /. 4) `1 ; ::_thesis: x in {((f /. 1) `1),((f /. 2) `1)}
then x = (f /. 1) `1 by A35, A23, PSCOMP_1:29;
hence x in {((f /. 1) `1),((f /. 2) `1)} by TARSKI:def_2; ::_thesis: verum
end;
suppose x = (f /. 5) `1 ; ::_thesis: x in {((f /. 1) `1),((f /. 2) `1)}
then x = (f /. 1) `1 by A9, FINSEQ_6:def_1;
hence x in {((f /. 1) `1),((f /. 2) `1)} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
then A38: rng <*((f /. 1) `1),((f /. 2) `1)*> = (rng <*((f /. 1) `1),((f /. 2) `1)*>) \/ {((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)} by A34, XBOOLE_1:12
.= (rng <*((f /. 1) `1),((f /. 2) `1)*>) \/ (rng <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) by FINSEQ_2:128
.= rng (X_axis f) by A33, FINSEQ_1:31 ;
len <*((f /. 1) `1),((f /. 2) `1)*> = 2 by FINSEQ_1:44
.= card (rng (X_axis f)) by A34, A38, A3, CARD_2:57 ;
then A39: Incr (X_axis f) = <*((f /. 1) `1),((f /. 2) `1)*> by A38, A16, SEQ_4:def_21;
then A40: (Incr (X_axis f)) . 1 = (f /. 1) `1 by FINSEQ_1:44;
set g = <*((f /. 4) `2),((f /. 5) `2)*>;
set h = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>;
A41: len (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) = (len <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*>) + (len <*((f /. 4) `2),((f /. 5) `2)*>) by FINSEQ_1:22
.= (len <*((f /. 4) `2),((f /. 5) `2)*>) + 3 by FINSEQ_1:45
.= 2 + 3 by FINSEQ_1:44
.= len f by SPRECT_1:82 ;
A42: len <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> = 3 by FINSEQ_1:45;
A43: dom <*((f /. 4) `2),((f /. 5) `2)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
A44: <*((f /. 4) `2),((f /. 5) `2)*> is increasing
proof
A45: <*((f /. 4) `2),((f /. 5) `2)*> . 2 = (f /. 5) `2 by FINSEQ_1:44;
A46: <*((f /. 4) `2),((f /. 5) `2)*> . 1 = (f /. 4) `2 by FINSEQ_1:44;
let n be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: for b1 being Element of NAT holds
( not n in K74(<*((f /. 4) `2),((f /. 5) `2)*>) or not b1 in K74(<*((f /. 4) `2),((f /. 5) `2)*>) or b1 <= n or not K571(<*((f /. 4) `2),((f /. 5) `2)*>,b1) <= K571(<*((f /. 4) `2),((f /. 5) `2)*>,n) )
let m be Element of NAT ; ::_thesis: ( not n in K74(<*((f /. 4) `2),((f /. 5) `2)*>) or not m in K74(<*((f /. 4) `2),((f /. 5) `2)*>) or m <= n or not K571(<*((f /. 4) `2),((f /. 5) `2)*>,m) <= K571(<*((f /. 4) `2),((f /. 5) `2)*>,n) )
assume that
A47: n in dom <*((f /. 4) `2),((f /. 5) `2)*> and
A48: m in dom <*((f /. 4) `2),((f /. 5) `2)*> and
A49: n < m ; ::_thesis: not K571(<*((f /. 4) `2),((f /. 5) `2)*>,m) <= K571(<*((f /. 4) `2),((f /. 5) `2)*>,n)
A50: ( m = 1 or m = 2 ) by A43, A48, TARSKI:def_2;
( n = 1 or n = 2 ) by A43, A47, TARSKI:def_2;
hence <*((f /. 4) `2),((f /. 5) `2)*> . n < <*((f /. 4) `2),((f /. 5) `2)*> . m by A35, A23, A10, A49, A46, A45, A50, SPRECT_2:57; ::_thesis: verum
end;
A51: (Incr (X_axis f)) . 2 = (f /. 2) `1 by A39, FINSEQ_1:44;
A52: len <*((f /. 4) `2),((f /. 5) `2)*> = 2 by FINSEQ_1:44;
for n being Element of NAT st n in dom (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) holds
(<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2
proof
let n be Element of NAT ; ::_thesis: ( n in dom (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) implies (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2 )
assume A53: n in dom (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) ; ::_thesis: (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2
then A54: 1 <= n by FINSEQ_3:25;
A55: n <= 5 by A9, A41, A53, FINSEQ_3:25;
percases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A54, A55, NAT_1:29;
supposeA56: n = 1 ; ::_thesis: (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2
then n in dom <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> by A42, FINSEQ_3:25;
hence (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> . 1 by A56, FINSEQ_1:def_7
.= (f /. n) `2 by A56, FINSEQ_1:45 ;
::_thesis: verum
end;
supposeA57: n = 2 ; ::_thesis: (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2
then n in dom <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> by A42, FINSEQ_3:25;
hence (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> . 2 by A57, FINSEQ_1:def_7
.= (f /. n) `2 by A57, FINSEQ_1:45 ;
::_thesis: verum
end;
supposeA58: n = 3 ; ::_thesis: (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2
then n in dom <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> by A42, FINSEQ_3:25;
hence (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> . 3 by A58, FINSEQ_1:def_7
.= (f /. n) `2 by A58, FINSEQ_1:45 ;
::_thesis: verum
end;
supposeA59: n = 4 ; ::_thesis: (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2
hence (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . (3 + 1)
.= <*((f /. 4) `2),((f /. 5) `2)*> . 1 by A52, A42, FINSEQ_1:65
.= (f /. n) `2 by A59, FINSEQ_1:44 ;
::_thesis: verum
end;
supposeA60: n = 5 ; ::_thesis: (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2
hence (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . (2 + 3)
.= <*((f /. 4) `2),((f /. 5) `2)*> . 2 by A52, A42, FINSEQ_1:65
.= (f /. n) `2 by A60, FINSEQ_1:44 ;
::_thesis: verum
end;
end;
end;
then A61: Y_axis f = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*> by A41, GOBOARD1:def_2;
A62: rng <*((f /. 4) `2),((f /. 5) `2)*> = {((f /. 4) `2),((f /. 5) `2)} by FINSEQ_2:127;
{((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)} c= {((f /. 4) `2),((f /. 5) `2)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)} or x in {((f /. 4) `2),((f /. 5) `2)} )
assume A63: x in {((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)} ; ::_thesis: x in {((f /. 4) `2),((f /. 5) `2)}
percases ( x = (f /. 1) `2 or x = (f /. 2) `2 or x = (f /. 3) `2 ) by A63, ENUMSET1:def_1;
suppose x = (f /. 1) `2 ; ::_thesis: x in {((f /. 4) `2),((f /. 5) `2)}
hence x in {((f /. 4) `2),((f /. 5) `2)} by A10, TARSKI:def_2; ::_thesis: verum
end;
suppose x = (f /. 2) `2 ; ::_thesis: x in {((f /. 4) `2),((f /. 5) `2)}
then x = (f /. 1) `2 by A2, A1, PSCOMP_1:37;
hence x in {((f /. 4) `2),((f /. 5) `2)} by A10, TARSKI:def_2; ::_thesis: verum
end;
suppose x = (f /. 3) `2 ; ::_thesis: x in {((f /. 4) `2),((f /. 5) `2)}
then x = (f /. 4) `2 by A6, A5, PSCOMP_1:53;
hence x in {((f /. 4) `2),((f /. 5) `2)} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
then A64: rng <*((f /. 4) `2),((f /. 5) `2)*> = {((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)} \/ {((f /. 4) `2),((f /. 5) `2)} by A62, XBOOLE_1:12
.= (rng <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*>) \/ {((f /. 4) `2),((f /. 5) `2)} by FINSEQ_2:128
.= (rng <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*>) \/ (rng <*((f /. 4) `2),((f /. 5) `2)*>) by FINSEQ_2:127
.= rng (Y_axis f) by A61, FINSEQ_1:31 ;
len <*((f /. 4) `2),((f /. 5) `2)*> = 2 by FINSEQ_1:44
.= card (rng (Y_axis f)) by A62, A64, A36, CARD_2:57 ;
then A65: Incr (Y_axis f) = <*((f /. 4) `2),((f /. 1) `2)*> by A10, A64, A44, SEQ_4:def_21;
then A66: (Incr (Y_axis f)) . 1 = (f /. 4) `2 by FINSEQ_1:44;
A67: (Incr (Y_axis f)) . 2 = (f /. 1) `2 by A65, FINSEQ_1:44;
A68: (f /. 1) `1 = (f /. 4) `1 by A35, A23, PSCOMP_1:29;
A69: for n, m being Element of NAT st [n,m] in Indices (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) holds
(((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
proof
let n, m be Element of NAT ; ::_thesis: ( [n,m] in Indices (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) implies (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| )
assume [n,m] in Indices (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) ; ::_thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A70: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by Th2;
percases ( [n,m] = [1,1] or [n,m] = [1,2] or [n,m] = [2,1] or [n,m] = [2,2] ) by A70, ENUMSET1:def_2;
supposeA71: [n,m] = [1,1] ; ::_thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A72: m = 1 by XTUPLE_0:1;
A73: n = 1 by A71, XTUPLE_0:1;
hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 4 by A72, MATRIX_2:6
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A40, A66, A68, A73, A72, EUCLID:53 ;
::_thesis: verum
end;
supposeA74: [n,m] = [1,2] ; ::_thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A75: m = 2 by XTUPLE_0:1;
A76: n = 1 by A74, XTUPLE_0:1;
hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 1 by A75, MATRIX_2:6
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A40, A67, A76, A75, EUCLID:53 ;
::_thesis: verum
end;
supposeA77: [n,m] = [2,1] ; ::_thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A78: m = 1 by XTUPLE_0:1;
A79: n = 2 by A77, XTUPLE_0:1;
hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 3 by A78, MATRIX_2:6
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A51, A66, A13, A7, A79, A78, EUCLID:53 ;
::_thesis: verum
end;
supposeA80: [n,m] = [2,2] ; ::_thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A81: m = 2 by XTUPLE_0:1;
A82: n = 2 by A80, XTUPLE_0:1;
hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 2 by A81, MATRIX_2:6
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A51, A67, A4, A82, A81, EUCLID:53 ;
::_thesis: verum
end;
end;
end;
A83: width (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) = 2 by MATRIX_2:3
.= len (Incr (Y_axis f)) by A65, FINSEQ_1:44 ;
len (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) = 2 by MATRIX_2:3
.= len (Incr (X_axis f)) by A39, FINSEQ_1:44 ;
then GoB ((Incr (X_axis f)),(Incr (Y_axis f))) = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) by A83, A69, GOBOARD2:def_1;
hence GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) by GOBOARD2:def_2; ::_thesis: verum
end;
theorem Th37: :: SPRECT_3:37
for f being rectangular special_circular_sequence holds
( LeftComp f = { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) } & RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } )
proof
let f be rectangular special_circular_sequence; ::_thesis: ( LeftComp f = { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) } & RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } )
defpred S1[ Element of (TOP-REAL 2)] means ( not W-bound (L~ f) <= $1 `1 or not $1 `1 <= E-bound (L~ f) or not S-bound (L~ f) <= $1 `2 or not $1 `2 <= N-bound (L~ f) );
defpred S2[ Element of (TOP-REAL 2)] means ( W-bound (L~ f) < $1 `1 & $1 `1 < E-bound (L~ f) & S-bound (L~ f) < $1 `2 & $1 `2 < N-bound (L~ f) );
defpred S3[ Element of (TOP-REAL 2)] means ( ( $1 `1 = W-bound (L~ f) & $1 `2 <= N-bound (L~ f) & $1 `2 >= S-bound (L~ f) ) or ( $1 `1 <= E-bound (L~ f) & $1 `1 >= W-bound (L~ f) & $1 `2 = N-bound (L~ f) ) or ( $1 `1 <= E-bound (L~ f) & $1 `1 >= W-bound (L~ f) & $1 `2 = S-bound (L~ f) ) or ( $1 `1 = E-bound (L~ f) & $1 `2 <= N-bound (L~ f) & $1 `2 >= S-bound (L~ f) ) );
set LC = { p where p is Point of (TOP-REAL 2) : S1[p] } ;
set RC = { q where q is Point of (TOP-REAL 2) : S2[q] } ;
set Lf = { p where p is Point of (TOP-REAL 2) : S3[p] } ;
A1: S-bound (L~ f) < N-bound (L~ f) by SPRECT_1:32;
A2: { p where p is Point of (TOP-REAL 2) : S3[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_7();
A3: { q where q is Point of (TOP-REAL 2) : S2[q] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_7();
A4: L~ f = { p where p is Point of (TOP-REAL 2) : S3[p] } by Th35;
{ p where p is Point of (TOP-REAL 2) : S1[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_7();
then reconsider Lc9 = { p where p is Point of (TOP-REAL 2) : S1[p] } , Rc9 = { q where q is Point of (TOP-REAL 2) : S2[q] } , Lf = { p where p is Point of (TOP-REAL 2) : S3[p] } as Subset of (TOP-REAL 2) by A3, A2;
reconsider Lf = Lf as Subset of (TOP-REAL 2) ;
reconsider Lc9 = Lc9, Rc9 = Rc9 as Subset of (TOP-REAL 2) ;
A5: W-bound (L~ f) < E-bound (L~ f) by SPRECT_1:31;
then reconsider Lc = Lc9, Rc = Rc9 as Subset of ((TOP-REAL 2) | (Lf `)) by A1, JORDAN1:39, JORDAN1:41;
reconsider Lc = Lc, Rc = Rc as Subset of ((TOP-REAL 2) | (Lf `)) ;
A6: ((1 / 2) * (S-bound (L~ f))) + ((1 / 2) * (S-bound (L~ f))) = S-bound (L~ f) ;
Rc = Rc9 ;
then Lc is a_component by A5, A1, JORDAN1:36;
then A7: Lc9 is_a_component_of Lf ` by CONNSP_1:def_6;
set p = ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|;
set q = (1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))));
A8: 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
A9: (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2) + (|[0,1]| `2) by TOPREAL3:2
.= (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2) + 1 by EUCLID:52 ;
A10: GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) by Th36;
then A11: 1 + 1 = width (GoB f) by MATRIX_2:3;
then ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2 = ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + (f /. 2))) `2 by A10, MATRIX_2:6
.= ((1 / 2) * ((f /. 1) + (f /. 2))) `2 by A10, A11, MATRIX_2:6
.= (1 / 2) * (((f /. 1) + (f /. 2)) `2) by TOPREAL3:4
.= (1 / 2) * (((f /. 1) `2) + ((f /. 2) `2)) by TOPREAL3:2
.= (1 / 2) * (((N-min (L~ f)) `2) + ((f /. 2) `2)) by SPRECT_1:83
.= (1 / 2) * (((N-min (L~ f)) `2) + ((N-max (L~ f)) `2)) by SPRECT_1:84
.= (1 / 2) * ((N-bound (L~ f)) + ((N-max (L~ f)) `2)) by EUCLID:52
.= (1 / 2) * ((N-bound (L~ f)) + (N-bound (L~ f))) by EUCLID:52
.= N-bound (L~ f) ;
then (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|) `2 > 0 + (N-bound (L~ f)) by A9, XREAL_1:8;
then A12: ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]| in { p where p is Point of (TOP-REAL 2) : S1[p] } ;
A13: 1 + 1 = len (GoB f) by A10, MATRIX_2:3;
then A14: ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]| in Int (cell ((GoB f),1,(1 + 1))) by A11, GOBOARD6:32;
A15: f /. (1 + 1) = (GoB f) * ((1 + 1),(1 + 1)) by A10, MATRIX_2:6;
1 < width (GoB f) by GOBOARD7:33;
then A16: 1 + 1 <= width (GoB f) by NAT_1:13;
then A17: [(1 + 1),(1 + 1)] in Indices (GoB f) by A13, MATRIX_1:36;
1 <= len (GoB f) by GOBOARD7:32;
then A18: [1,(1 + 1)] in Indices (GoB f) by A16, MATRIX_1:36;
A19: f /. 1 = (GoB f) * (1,(1 + 1)) by A10, MATRIX_2:6;
then right_cell (f,1) = cell ((GoB f),1,1) by A8, A18, A17, A15, GOBOARD5:28;
then A20: Int (cell ((GoB f),1,1)) c= RightComp f by GOBOARD9:def_2;
left_cell (f,1) = cell ((GoB f),1,(1 + 1)) by A8, A18, A19, A17, A15, GOBOARD5:28;
then Int (cell ((GoB f),1,(1 + 1))) c= LeftComp f by GOBOARD9:def_1;
then A21: { p where p is Point of (TOP-REAL 2) : S1[p] } meets LeftComp f by A14, A12, XBOOLE_0:3;
A22: (f /. 2) `1 = (E-max (L~ f)) `1 by SPRECT_1:84
.= E-bound (L~ f) by EUCLID:52 ;
set p = (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)));
A23: (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) in Int (cell ((GoB f),1,1)) by A13, A11, GOBOARD6:31;
A24: (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) = (1 / 2) * (((GoB f) * (1,1)) + (f /. 2)) by A10, MATRIX_2:6
.= (1 / 2) * ((f /. 4) + (f /. 2)) by A10, MATRIX_2:6 ;
then A25: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 = (1 / 2) * (((f /. 4) + (f /. 2)) `1) by TOPREAL3:4
.= (1 / 2) * (((f /. 4) `1) + ((f /. 2) `1)) by TOPREAL3:2
.= ((1 / 2) * ((f /. 4) `1)) + ((1 / 2) * ((f /. 2) `1)) ;
LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1;
hence LeftComp f = { p where p is Point of (TOP-REAL 2) : S1[p] } by A4, A7, A21, GOBOARD9:1; ::_thesis: RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) }
A26: ((1 / 2) * (W-bound (L~ f))) + ((1 / 2) * (W-bound (L~ f))) = W-bound (L~ f) ;
A27: ((1 / 2) * (E-bound (L~ f))) + ((1 / 2) * (E-bound (L~ f))) = E-bound (L~ f) ;
A28: ((1 / 2) * (N-bound (L~ f))) + ((1 / 2) * (N-bound (L~ f))) = N-bound (L~ f) ;
A29: (f /. 4) `1 = (W-min (L~ f)) `1 by SPRECT_1:86
.= W-bound (L~ f) by EUCLID:52 ;
then (1 / 2) * ((f /. 4) `1) < (1 / 2) * (E-bound (L~ f)) by SPRECT_1:31, XREAL_1:68;
then A30: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 < E-bound (L~ f) by A27, A25, A22, XREAL_1:6;
A31: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 = (1 / 2) * (((f /. 4) + (f /. 2)) `2) by A24, TOPREAL3:4
.= (1 / 2) * (((f /. 4) `2) + ((f /. 2) `2)) by TOPREAL3:2
.= ((1 / 2) * ((f /. 4) `2)) + ((1 / 2) * ((f /. 2) `2)) ;
Lc = Lc9 ;
then Rc is a_component by A5, A1, JORDAN1:36;
then A32: Rc9 is_a_component_of Lf ` by CONNSP_1:def_6;
A33: (f /. 2) `2 = (N-max (L~ f)) `2 by SPRECT_1:84
.= N-bound (L~ f) by EUCLID:52 ;
A34: (f /. 4) `2 = (S-min (L~ f)) `2 by SPRECT_1:86
.= S-bound (L~ f) by EUCLID:52 ;
then (1 / 2) * ((f /. 4) `2) < (1 / 2) * (N-bound (L~ f)) by SPRECT_1:32, XREAL_1:68;
then A35: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 < N-bound (L~ f) by A28, A31, A33, XREAL_1:6;
(1 / 2) * ((f /. 2) `2) > (1 / 2) * (S-bound (L~ f)) by A33, SPRECT_1:32, XREAL_1:68;
then A36: S-bound (L~ f) < ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 by A6, A31, A34, XREAL_1:6;
(1 / 2) * ((f /. 2) `1) > (1 / 2) * (W-bound (L~ f)) by A22, SPRECT_1:31, XREAL_1:68;
then W-bound (L~ f) < ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 by A26, A25, A29, XREAL_1:6;
then (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) in { q where q is Point of (TOP-REAL 2) : S2[q] } by A30, A36, A35;
then A37: { q where q is Point of (TOP-REAL 2) : S2[q] } meets RightComp f by A23, A20, XBOOLE_0:3;
RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2;
hence RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by A4, A32, A37, GOBOARD9:1; ::_thesis: verum
end;
registration
cluster non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V236( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard rectangular clockwise_oriented for FinSequence of the U1 of (TOP-REAL 2);
existence
ex b1 being rectangular special_circular_sequence st b1 is clockwise_oriented
proof
set C = the non empty compact non horizontal non vertical Subset of (TOP-REAL 2);
SpStSeq the non empty compact non horizontal non vertical Subset of (TOP-REAL 2) is clockwise_oriented ;
hence ex b1 being rectangular special_circular_sequence st b1 is clockwise_oriented ; ::_thesis: verum
end;
end;
registration
cluster non empty V236( the U1 of (TOP-REAL 2)) special unfolded s.c.c. rectangular -> rectangular clockwise_oriented for FinSequence of the U1 of (TOP-REAL 2);
coherence
for b1 being rectangular special_circular_sequence holds b1 is clockwise_oriented
proof
let f be rectangular special_circular_sequence; ::_thesis: f is clockwise_oriented
ex D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st f = SpStSeq D by SPRECT_1:def_2;
hence f is clockwise_oriented ; ::_thesis: verum
end;
end;
theorem :: SPRECT_3:38
for f being rectangular special_circular_sequence
for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> NW-corner (L~ f)
proof
let f be rectangular special_circular_sequence; ::_thesis: for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> NW-corner (L~ f)
let g be S-Sequence_in_R2; ::_thesis: ( g /. 1 in LeftComp f & g /. (len g) in RightComp f implies Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> NW-corner (L~ f) )
assume that
A1: g /. 1 in LeftComp f and
A2: g /. (len g) in RightComp f ; ::_thesis: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> NW-corner (L~ f)
A3: L~ f meets L~ g by A1, A2, Th33;
assume A4: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = NW-corner (L~ f) ; ::_thesis: contradiction
set nw = NW-corner (L~ f);
set inw = Index ((NW-corner (L~ f)),g);
A5: len g in dom g by FINSEQ_5:6;
then A6: g . (len g) = g /. (len g) by PARTFUN1:def_6;
A7: 1 <= (Index ((NW-corner (L~ f)),g)) + 1 by NAT_1:11;
L~ g is_an_arc_of g /. 1,g /. (len g) by TOPREAL1:25;
then A8: NW-corner (L~ f) in (L~ g) /\ (L~ f) by A3, A4, JORDAN5C:def_2;
then A9: NW-corner (L~ f) in L~ g by XBOOLE_0:def_4;
then A10: 1 <= Index ((NW-corner (L~ f)),g) by JORDAN3:8;
A11: NW-corner (L~ f) in LSeg (g,(Index ((NW-corner (L~ f)),g))) by A9, JORDAN3:9;
A12: Index ((NW-corner (L~ f)),g) < len g by A9, JORDAN3:8;
then A13: (Index ((NW-corner (L~ f)),g)) + 1 <= len g by NAT_1:13;
then A14: (Index ((NW-corner (L~ f)),g)) + 1 in dom g by A7, FINSEQ_3:25;
A15: L~ f misses RightComp f by Th25;
A16: now__::_thesis:_not_NW-corner_(L~_f)_<>_g_._((Index_((NW-corner_(L~_f)),g))_+_1)
A17: len g >= 1 by A13, A7, XXREAL_0:2;
assume NW-corner (L~ f) <> g . ((Index ((NW-corner (L~ f)),g)) + 1) ; ::_thesis: contradiction
then A18: NW-corner (L~ f) <> g /. ((Index ((NW-corner (L~ f)),g)) + 1) by A14, PARTFUN1:def_6;
percases ( g /. ((Index ((NW-corner (L~ f)),g)) + 1) in L~ f or not g /. ((Index ((NW-corner (L~ f)),g)) + 1) in L~ f ) ;
supposeA19: g /. ((Index ((NW-corner (L~ f)),g)) + 1) in L~ f ; ::_thesis: contradiction
then (Index ((NW-corner (L~ f)),g)) + 1 <> len g by A2, A15, XBOOLE_0:3;
then (Index ((NW-corner (L~ f)),g)) + 1 < len g by A13, XXREAL_0:1;
then A20: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 <= len g by NAT_1:13;
then g /. ((Index ((NW-corner (L~ f)),g)) + 1) in LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) by A7, TOPREAL1:21;
then Index ((NW-corner (L~ f)),g) >= (Index ((NW-corner (L~ f)),g)) + 1 by A3, A4, A10, A13, A11, A7, A18, A19, A20, JORDAN5C:28;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
supposeA21: not g /. ((Index ((NW-corner (L~ f)),g)) + 1) in L~ f ; ::_thesis: contradiction
A22: now__::_thesis:_not_g_/._((Index_((NW-corner_(L~_f)),g))_+_1)_in_RightComp_f
assume A23: g /. ((Index ((NW-corner (L~ f)),g)) + 1) in RightComp f ; ::_thesis: contradiction
RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by Th37;
then A24: ex q being Point of (TOP-REAL 2) st
( g /. ((Index ((NW-corner (L~ f)),g)) + 1) = q & W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) by A23;
A25: ( LSeg (g,(Index ((NW-corner (L~ f)),g))) is vertical or LSeg (g,(Index ((NW-corner (L~ f)),g))) is horizontal ) by SPPOL_1:19;
LSeg (g,(Index ((NW-corner (L~ f)),g))) = LSeg ((g /. (Index ((NW-corner (L~ f)),g))),(g /. ((Index ((NW-corner (L~ f)),g)) + 1))) by A10, A13, TOPREAL1:def_3;
then ( (g /. ((Index ((NW-corner (L~ f)),g)) + 1)) `1 = (NW-corner (L~ f)) `1 or (g /. ((Index ((NW-corner (L~ f)),g)) + 1)) `2 = (NW-corner (L~ f)) `2 ) by A11, A25, SPPOL_1:40, SPPOL_1:41;
hence contradiction by A24, EUCLID:52; ::_thesis: verum
end;
then reconsider m = mid (g,((Index ((NW-corner (L~ f)),g)) + 1),(len g)) as S-Sequence_in_R2 by A2, A13, A7, A17, JORDAN3:6;
A26: (Index ((NW-corner (L~ f)),g)) + 1 < len g by A2, A13, A22, XXREAL_0:1;
g /. ((Index ((NW-corner (L~ f)),g)) + 1) in (L~ f) ` by A21, SUBSET_1:29;
then g /. ((Index ((NW-corner (L~ f)),g)) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:10;
then g /. ((Index ((NW-corner (L~ f)),g)) + 1) in LeftComp f by A22, XBOOLE_0:def_3;
then A27: m /. 1 in LeftComp f by A5, A14, SPRECT_2:8;
m /. (len m) in RightComp f by A2, A5, A14, SPRECT_2:9;
then L~ f meets L~ m by A27, Th33;
then consider q being set such that
A28: q in L~ f and
A29: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A29;
consider i being Element of NAT such that
A30: 1 <= i and
A31: i + 1 <= len m and
A32: q in LSeg (m,i) by A29, SPPOL_2:13;
set j = (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1;
A33: (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 = ((i + (Index ((NW-corner (L~ f)),g))) + 1) -' 1
.= i + (Index ((NW-corner (L~ f)),g)) by NAT_D:34 ;
A34: len m = ((len g) -' ((Index ((NW-corner (L~ f)),g)) + 1)) + 1 by A13, A7, JORDAN4:8;
then len m = (len g) -' (Index ((NW-corner (L~ f)),g)) by A9, JORDAN3:8, NAT_2:7;
then (len m) + (Index ((NW-corner (L~ f)),g)) = len g by A12, XREAL_1:235;
then (i + 1) + (Index ((NW-corner (L~ f)),g)) <= len g by A31, XREAL_1:6;
then A35: ((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1) + 1 <= len g by A33;
i < len m by A31, NAT_1:13;
then A36: LSeg (m,i) = LSeg (g,((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1)) by A7, A26, A30, A34, JORDAN4:19;
A37: (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 >= (Index ((NW-corner (L~ f)),g)) + 1 by A30, A33, XREAL_1:6;
A38: now__::_thesis:_not_NW-corner_(L~_f)_=_q
assume NW-corner (L~ f) = q ; ::_thesis: contradiction
then A39: NW-corner (L~ f) in (LSeg (g,(Index ((NW-corner (L~ f)),g)))) /\ (LSeg (g,((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1))) by A11, A32, A36, XBOOLE_0:def_4;
then A40: LSeg (g,(Index ((NW-corner (L~ f)),g))) meets LSeg (g,((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1)) by XBOOLE_0:4;
percases ( (Index ((NW-corner (L~ f)),g)) + 1 = (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 or (Index ((NW-corner (L~ f)),g)) + 1 < (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 ) by A37, XXREAL_0:1;
supposeA41: (Index ((NW-corner (L~ f)),g)) + 1 = (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 ; ::_thesis: contradiction
((Index ((NW-corner (L~ f)),g)) + 1) + 1 <= len g by A26, NAT_1:13;
then (Index ((NW-corner (L~ f)),g)) + (1 + 1) <= len g ;
then (LSeg (g,(Index ((NW-corner (L~ f)),g)))) /\ (LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1))) = {(g /. ((Index ((NW-corner (L~ f)),g)) + 1))} by A10, TOPREAL1:def_6;
hence contradiction by A18, A39, A41, TARSKI:def_1; ::_thesis: verum
end;
suppose (Index ((NW-corner (L~ f)),g)) + 1 < (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 ; ::_thesis: contradiction
hence contradiction by A40, TOPREAL1:def_7; ::_thesis: verum
end;
end;
end;
Index ((NW-corner (L~ f)),g) >= 0 by NAT_1:2;
then 0 + 1 <= (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 by A30, A33, XREAL_1:7;
then Index ((NW-corner (L~ f)),g) >= (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 by A3, A4, A10, A13, A11, A28, A32, A36, A35, A38, JORDAN5C:28;
then Index ((NW-corner (L~ f)),g) >= (Index ((NW-corner (L~ f)),g)) + 1 by A37, XXREAL_0:2;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
end;
end;
NW-corner (L~ f) in L~ f by A8, XBOOLE_0:def_4;
then NW-corner (L~ f) <> g . (len g) by A2, A15, A6, XBOOLE_0:3;
then A42: (Index ((NW-corner (L~ f)),g)) + 1 < len g by A13, A16, XXREAL_0:1;
then A43: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 <= len g by NAT_1:13;
then g /. ((Index ((NW-corner (L~ f)),g)) + 1) in LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) by A7, TOPREAL1:21;
then A44: NW-corner (L~ f) in LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) by A14, A16, PARTFUN1:def_6;
A45: 1 <= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by NAT_1:11;
then A46: len g >= 1 by A43, XXREAL_0:2;
A47: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 in dom g by A43, A45, FINSEQ_3:25;
(Index ((NW-corner (L~ f)),g)) + 1 < ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by NAT_1:13;
then A48: NW-corner (L~ f) <> g . (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A14, A16, A47, FUNCT_1:def_4;
then A49: NW-corner (L~ f) <> g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A47, PARTFUN1:def_6;
percases ( g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f or not g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f ) ;
supposeA50: g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f ; ::_thesis: contradiction
A51: NW-corner (L~ f) <> g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A47, A48, PARTFUN1:def_6;
((Index ((NW-corner (L~ f)),g)) + 1) + 1 <> len g by A2, A15, A50, XBOOLE_0:3;
then ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < len g by A43, XXREAL_0:1;
then A52: (((Index ((NW-corner (L~ f)),g)) + 1) + 1) + 1 <= len g by NAT_1:13;
then g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in LSeg (g,(((Index ((NW-corner (L~ f)),g)) + 1) + 1)) by A45, TOPREAL1:21;
then (Index ((NW-corner (L~ f)),g)) + 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A3, A4, A7, A43, A45, A44, A50, A52, A51, JORDAN5C:28;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
supposeA53: not g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f ; ::_thesis: contradiction
A54: now__::_thesis:_not_g_/._(((Index_((NW-corner_(L~_f)),g))_+_1)_+_1)_in_RightComp_f
assume A55: g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in RightComp f ; ::_thesis: contradiction
RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by Th37;
then A56: ex q being Point of (TOP-REAL 2) st
( g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) = q & W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) by A55;
A57: ( LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) is vertical or LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) is horizontal ) by SPPOL_1:19;
LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) = LSeg ((g /. ((Index ((NW-corner (L~ f)),g)) + 1)),(g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1))) by A7, A43, TOPREAL1:def_3;
then ( (g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) `1 = (NW-corner (L~ f)) `1 or (g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) `2 = (NW-corner (L~ f)) `2 ) by A44, A57, SPPOL_1:40, SPPOL_1:41;
hence contradiction by A56, EUCLID:52; ::_thesis: verum
end;
then reconsider m = mid (g,(((Index ((NW-corner (L~ f)),g)) + 1) + 1),(len g)) as S-Sequence_in_R2 by A2, A43, A45, A46, JORDAN3:6;
A58: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < len g by A2, A43, A54, XXREAL_0:1;
g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in (L~ f) ` by A53, SUBSET_1:29;
then g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:10;
then g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in LeftComp f by A54, XBOOLE_0:def_3;
then A59: m /. 1 in LeftComp f by A5, A47, SPRECT_2:8;
m /. (len m) in RightComp f by A2, A5, A47, SPRECT_2:9;
then L~ f meets L~ m by A59, Th33;
then consider q being set such that
A60: q in L~ f and
A61: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A61;
consider i being Element of NAT such that
A62: 1 <= i and
A63: i + 1 <= len m and
A64: q in LSeg (m,i) by A61, SPPOL_2:13;
set j = (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1;
A65: len m = ((len g) -' (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) + 1 by A43, A45, JORDAN4:8;
then len m = (len g) -' ((Index ((NW-corner (L~ f)),g)) + 1) by A42, NAT_2:7;
then (len m) + ((Index ((NW-corner (L~ f)),g)) + 1) = len g by A13, XREAL_1:235;
then (i + 1) + ((Index ((NW-corner (L~ f)),g)) + 1) <= len g by A63, XREAL_1:6;
then A66: ((i + 1) + (Index ((NW-corner (L~ f)),g))) + 1 <= len g ;
i < len m by A63, NAT_1:13;
then A67: LSeg (m,i) = LSeg (g,((i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1)) by A45, A58, A62, A65, JORDAN4:19;
A68: (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 = (((i + (Index ((NW-corner (L~ f)),g))) + 1) + 1) -' 1
.= (i + (Index ((NW-corner (L~ f)),g))) + 1 by NAT_D:34 ;
then (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 = i + ((Index ((NW-corner (L~ f)),g)) + 1) ;
then A69: (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A62, XREAL_1:6;
A70: now__::_thesis:_not_NW-corner_(L~_f)_=_q
assume NW-corner (L~ f) = q ; ::_thesis: contradiction
then A71: NW-corner (L~ f) in (LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1))) /\ (LSeg (g,((i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1))) by A44, A64, A67, XBOOLE_0:def_4;
then A72: LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) meets LSeg (g,((i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1)) by XBOOLE_0:4;
percases ( ((Index ((NW-corner (L~ f)),g)) + 1) + 1 = (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 or ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 ) by A69, XXREAL_0:1;
supposeA73: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 = (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 ; ::_thesis: contradiction
(((Index ((NW-corner (L~ f)),g)) + 1) + 1) + 1 <= len g by A58, NAT_1:13;
then ((Index ((NW-corner (L~ f)),g)) + 1) + (1 + 1) <= len g ;
then (LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1))) /\ (LSeg (g,(((Index ((NW-corner (L~ f)),g)) + 1) + 1))) = {(g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1))} by A7, TOPREAL1:def_6;
hence contradiction by A49, A71, A73, TARSKI:def_1; ::_thesis: verum
end;
suppose ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 ; ::_thesis: contradiction
hence contradiction by A72, TOPREAL1:def_7; ::_thesis: verum
end;
end;
end;
0 + 1 <= (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 by A68, NAT_1:11;
then (Index ((NW-corner (L~ f)),g)) + 1 >= (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 by A3, A4, A7, A43, A44, A60, A64, A67, A68, A66, A70, JORDAN5C:28;
then (Index ((NW-corner (L~ f)),g)) + 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A69, XXREAL_0:2;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
end;
end;
theorem :: SPRECT_3:39
for f being rectangular special_circular_sequence
for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> SE-corner (L~ f)
proof
let f be rectangular special_circular_sequence; ::_thesis: for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> SE-corner (L~ f)
let g be S-Sequence_in_R2; ::_thesis: ( g /. 1 in LeftComp f & g /. (len g) in RightComp f implies Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> SE-corner (L~ f) )
assume that
A1: g /. 1 in LeftComp f and
A2: g /. (len g) in RightComp f ; ::_thesis: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> SE-corner (L~ f)
A3: L~ f meets L~ g by A1, A2, Th33;
assume A4: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = SE-corner (L~ f) ; ::_thesis: contradiction
set se = SE-corner (L~ f);
set ise = Index ((SE-corner (L~ f)),g);
A5: len g in dom g by FINSEQ_5:6;
then A6: g . (len g) = g /. (len g) by PARTFUN1:def_6;
A7: 1 <= (Index ((SE-corner (L~ f)),g)) + 1 by NAT_1:11;
L~ g is_an_arc_of g /. 1,g /. (len g) by TOPREAL1:25;
then A8: SE-corner (L~ f) in (L~ g) /\ (L~ f) by A3, A4, JORDAN5C:def_2;
then A9: SE-corner (L~ f) in L~ g by XBOOLE_0:def_4;
then A10: 1 <= Index ((SE-corner (L~ f)),g) by JORDAN3:8;
A11: SE-corner (L~ f) in LSeg (g,(Index ((SE-corner (L~ f)),g))) by A9, JORDAN3:9;
A12: Index ((SE-corner (L~ f)),g) < len g by A9, JORDAN3:8;
then A13: (Index ((SE-corner (L~ f)),g)) + 1 <= len g by NAT_1:13;
then A14: (Index ((SE-corner (L~ f)),g)) + 1 in dom g by A7, FINSEQ_3:25;
A15: L~ f misses RightComp f by Th25;
A16: now__::_thesis:_not_SE-corner_(L~_f)_<>_g_._((Index_((SE-corner_(L~_f)),g))_+_1)
A17: len g >= 1 by A13, A7, XXREAL_0:2;
assume SE-corner (L~ f) <> g . ((Index ((SE-corner (L~ f)),g)) + 1) ; ::_thesis: contradiction
then A18: SE-corner (L~ f) <> g /. ((Index ((SE-corner (L~ f)),g)) + 1) by A14, PARTFUN1:def_6;
percases ( g /. ((Index ((SE-corner (L~ f)),g)) + 1) in L~ f or not g /. ((Index ((SE-corner (L~ f)),g)) + 1) in L~ f ) ;
supposeA19: g /. ((Index ((SE-corner (L~ f)),g)) + 1) in L~ f ; ::_thesis: contradiction
then (Index ((SE-corner (L~ f)),g)) + 1 <> len g by A2, A15, XBOOLE_0:3;
then (Index ((SE-corner (L~ f)),g)) + 1 < len g by A13, XXREAL_0:1;
then A20: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 <= len g by NAT_1:13;
then g /. ((Index ((SE-corner (L~ f)),g)) + 1) in LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) by A7, TOPREAL1:21;
then Index ((SE-corner (L~ f)),g) >= (Index ((SE-corner (L~ f)),g)) + 1 by A3, A4, A10, A13, A11, A7, A18, A19, A20, JORDAN5C:28;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
supposeA21: not g /. ((Index ((SE-corner (L~ f)),g)) + 1) in L~ f ; ::_thesis: contradiction
A22: now__::_thesis:_not_g_/._((Index_((SE-corner_(L~_f)),g))_+_1)_in_RightComp_f
assume A23: g /. ((Index ((SE-corner (L~ f)),g)) + 1) in RightComp f ; ::_thesis: contradiction
RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by Th37;
then A24: ex q being Point of (TOP-REAL 2) st
( g /. ((Index ((SE-corner (L~ f)),g)) + 1) = q & W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) by A23;
A25: ( LSeg (g,(Index ((SE-corner (L~ f)),g))) is vertical or LSeg (g,(Index ((SE-corner (L~ f)),g))) is horizontal ) by SPPOL_1:19;
LSeg (g,(Index ((SE-corner (L~ f)),g))) = LSeg ((g /. (Index ((SE-corner (L~ f)),g))),(g /. ((Index ((SE-corner (L~ f)),g)) + 1))) by A10, A13, TOPREAL1:def_3;
then ( (g /. ((Index ((SE-corner (L~ f)),g)) + 1)) `1 = (SE-corner (L~ f)) `1 or (g /. ((Index ((SE-corner (L~ f)),g)) + 1)) `2 = (SE-corner (L~ f)) `2 ) by A11, A25, SPPOL_1:40, SPPOL_1:41;
hence contradiction by A24, EUCLID:52; ::_thesis: verum
end;
then reconsider m = mid (g,((Index ((SE-corner (L~ f)),g)) + 1),(len g)) as S-Sequence_in_R2 by A2, A13, A7, A17, JORDAN3:6;
A26: (Index ((SE-corner (L~ f)),g)) + 1 < len g by A2, A13, A22, XXREAL_0:1;
g /. ((Index ((SE-corner (L~ f)),g)) + 1) in (L~ f) ` by A21, SUBSET_1:29;
then g /. ((Index ((SE-corner (L~ f)),g)) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:10;
then g /. ((Index ((SE-corner (L~ f)),g)) + 1) in LeftComp f by A22, XBOOLE_0:def_3;
then A27: m /. 1 in LeftComp f by A5, A14, SPRECT_2:8;
m /. (len m) in RightComp f by A2, A5, A14, SPRECT_2:9;
then L~ f meets L~ m by A27, Th33;
then consider q being set such that
A28: q in L~ f and
A29: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A29;
consider i being Element of NAT such that
A30: 1 <= i and
A31: i + 1 <= len m and
A32: q in LSeg (m,i) by A29, SPPOL_2:13;
set j = (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1;
A33: (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 = ((i + (Index ((SE-corner (L~ f)),g))) + 1) -' 1
.= i + (Index ((SE-corner (L~ f)),g)) by NAT_D:34 ;
A34: len m = ((len g) -' ((Index ((SE-corner (L~ f)),g)) + 1)) + 1 by A13, A7, JORDAN4:8;
then len m = (len g) -' (Index ((SE-corner (L~ f)),g)) by A9, JORDAN3:8, NAT_2:7;
then (len m) + (Index ((SE-corner (L~ f)),g)) = len g by A12, XREAL_1:235;
then (i + 1) + (Index ((SE-corner (L~ f)),g)) <= len g by A31, XREAL_1:6;
then A35: ((i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1) + 1 <= len g by A33;
i < len m by A31, NAT_1:13;
then A36: LSeg (m,i) = LSeg (g,((i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1)) by A7, A26, A30, A34, JORDAN4:19;
A37: (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 >= (Index ((SE-corner (L~ f)),g)) + 1 by A30, A33, XREAL_1:6;
A38: now__::_thesis:_not_SE-corner_(L~_f)_=_q
assume SE-corner (L~ f) = q ; ::_thesis: contradiction
then A39: SE-corner (L~ f) in (LSeg (g,(Index ((SE-corner (L~ f)),g)))) /\ (LSeg (g,((i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1))) by A11, A32, A36, XBOOLE_0:def_4;
then A40: LSeg (g,(Index ((SE-corner (L~ f)),g))) meets LSeg (g,((i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1)) by XBOOLE_0:4;
percases ( (Index ((SE-corner (L~ f)),g)) + 1 = (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 or (Index ((SE-corner (L~ f)),g)) + 1 < (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 ) by A37, XXREAL_0:1;
supposeA41: (Index ((SE-corner (L~ f)),g)) + 1 = (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 ; ::_thesis: contradiction
((Index ((SE-corner (L~ f)),g)) + 1) + 1 <= len g by A26, NAT_1:13;
then (Index ((SE-corner (L~ f)),g)) + (1 + 1) <= len g ;
then (LSeg (g,(Index ((SE-corner (L~ f)),g)))) /\ (LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1))) = {(g /. ((Index ((SE-corner (L~ f)),g)) + 1))} by A10, TOPREAL1:def_6;
hence contradiction by A18, A39, A41, TARSKI:def_1; ::_thesis: verum
end;
suppose (Index ((SE-corner (L~ f)),g)) + 1 < (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 ; ::_thesis: contradiction
hence contradiction by A40, TOPREAL1:def_7; ::_thesis: verum
end;
end;
end;
Index ((SE-corner (L~ f)),g) >= 0 by NAT_1:2;
then 0 + 1 <= (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 by A30, A33, XREAL_1:7;
then Index ((SE-corner (L~ f)),g) >= (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 by A3, A4, A10, A13, A11, A28, A32, A36, A35, A38, JORDAN5C:28;
then Index ((SE-corner (L~ f)),g) >= (Index ((SE-corner (L~ f)),g)) + 1 by A37, XXREAL_0:2;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
end;
end;
SE-corner (L~ f) in L~ f by A8, XBOOLE_0:def_4;
then SE-corner (L~ f) <> g . (len g) by A2, A15, A6, XBOOLE_0:3;
then A42: (Index ((SE-corner (L~ f)),g)) + 1 < len g by A13, A16, XXREAL_0:1;
then A43: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 <= len g by NAT_1:13;
then g /. ((Index ((SE-corner (L~ f)),g)) + 1) in LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) by A7, TOPREAL1:21;
then A44: SE-corner (L~ f) in LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) by A14, A16, PARTFUN1:def_6;
A45: 1 <= ((Index ((SE-corner (L~ f)),g)) + 1) + 1 by NAT_1:11;
then A46: len g >= 1 by A43, XXREAL_0:2;
A47: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 in dom g by A43, A45, FINSEQ_3:25;
(Index ((SE-corner (L~ f)),g)) + 1 < ((Index ((SE-corner (L~ f)),g)) + 1) + 1 by NAT_1:13;
then A48: SE-corner (L~ f) <> g . (((Index ((SE-corner (L~ f)),g)) + 1) + 1) by A14, A16, A47, FUNCT_1:def_4;
then A49: SE-corner (L~ f) <> g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) by A47, PARTFUN1:def_6;
percases ( g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in L~ f or not g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in L~ f ) ;
supposeA50: g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in L~ f ; ::_thesis: contradiction
A51: SE-corner (L~ f) <> g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) by A47, A48, PARTFUN1:def_6;
((Index ((SE-corner (L~ f)),g)) + 1) + 1 <> len g by A2, A15, A50, XBOOLE_0:3;
then ((Index ((SE-corner (L~ f)),g)) + 1) + 1 < len g by A43, XXREAL_0:1;
then A52: (((Index ((SE-corner (L~ f)),g)) + 1) + 1) + 1 <= len g by NAT_1:13;
then g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in LSeg (g,(((Index ((SE-corner (L~ f)),g)) + 1) + 1)) by A45, TOPREAL1:21;
then (Index ((SE-corner (L~ f)),g)) + 1 >= ((Index ((SE-corner (L~ f)),g)) + 1) + 1 by A3, A4, A7, A43, A45, A44, A50, A52, A51, JORDAN5C:28;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
supposeA53: not g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in L~ f ; ::_thesis: contradiction
A54: now__::_thesis:_not_g_/._(((Index_((SE-corner_(L~_f)),g))_+_1)_+_1)_in_RightComp_f
assume A55: g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in RightComp f ; ::_thesis: contradiction
RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by Th37;
then A56: ex q being Point of (TOP-REAL 2) st
( g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) = q & W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) by A55;
A57: ( LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) is vertical or LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) is horizontal ) by SPPOL_1:19;
LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) = LSeg ((g /. ((Index ((SE-corner (L~ f)),g)) + 1)),(g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1))) by A7, A43, TOPREAL1:def_3;
then ( (g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) `1 = (SE-corner (L~ f)) `1 or (g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) `2 = (SE-corner (L~ f)) `2 ) by A44, A57, SPPOL_1:40, SPPOL_1:41;
hence contradiction by A56, EUCLID:52; ::_thesis: verum
end;
then reconsider m = mid (g,(((Index ((SE-corner (L~ f)),g)) + 1) + 1),(len g)) as S-Sequence_in_R2 by A2, A43, A45, A46, JORDAN3:6;
A58: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 < len g by A2, A43, A54, XXREAL_0:1;
g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in (L~ f) ` by A53, SUBSET_1:29;
then g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:10;
then g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in LeftComp f by A54, XBOOLE_0:def_3;
then A59: m /. 1 in LeftComp f by A5, A47, SPRECT_2:8;
m /. (len m) in RightComp f by A2, A5, A47, SPRECT_2:9;
then L~ f meets L~ m by A59, Th33;
then consider q being set such that
A60: q in L~ f and
A61: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A61;
consider i being Element of NAT such that
A62: 1 <= i and
A63: i + 1 <= len m and
A64: q in LSeg (m,i) by A61, SPPOL_2:13;
set j = (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1;
A65: len m = ((len g) -' (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) + 1 by A43, A45, JORDAN4:8;
then len m = (len g) -' ((Index ((SE-corner (L~ f)),g)) + 1) by A42, NAT_2:7;
then (len m) + ((Index ((SE-corner (L~ f)),g)) + 1) = len g by A13, XREAL_1:235;
then (i + 1) + ((Index ((SE-corner (L~ f)),g)) + 1) <= len g by A63, XREAL_1:6;
then A66: ((i + 1) + (Index ((SE-corner (L~ f)),g))) + 1 <= len g ;
i < len m by A63, NAT_1:13;
then A67: LSeg (m,i) = LSeg (g,((i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1)) by A45, A58, A62, A65, JORDAN4:19;
A68: (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 = (((i + (Index ((SE-corner (L~ f)),g))) + 1) + 1) -' 1
.= (i + (Index ((SE-corner (L~ f)),g))) + 1 by NAT_D:34 ;
then (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 = i + ((Index ((SE-corner (L~ f)),g)) + 1) ;
then A69: (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 >= ((Index ((SE-corner (L~ f)),g)) + 1) + 1 by A62, XREAL_1:6;
A70: now__::_thesis:_not_SE-corner_(L~_f)_=_q
assume SE-corner (L~ f) = q ; ::_thesis: contradiction
then A71: SE-corner (L~ f) in (LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1))) /\ (LSeg (g,((i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1))) by A44, A64, A67, XBOOLE_0:def_4;
then A72: LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) meets LSeg (g,((i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1)) by XBOOLE_0:4;
percases ( ((Index ((SE-corner (L~ f)),g)) + 1) + 1 = (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 or ((Index ((SE-corner (L~ f)),g)) + 1) + 1 < (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 ) by A69, XXREAL_0:1;
supposeA73: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 = (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 ; ::_thesis: contradiction
(((Index ((SE-corner (L~ f)),g)) + 1) + 1) + 1 <= len g by A58, NAT_1:13;
then ((Index ((SE-corner (L~ f)),g)) + 1) + (1 + 1) <= len g ;
then (LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1))) /\ (LSeg (g,(((Index ((SE-corner (L~ f)),g)) + 1) + 1))) = {(g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1))} by A7, TOPREAL1:def_6;
hence contradiction by A49, A71, A73, TARSKI:def_1; ::_thesis: verum
end;
suppose ((Index ((SE-corner (L~ f)),g)) + 1) + 1 < (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 ; ::_thesis: contradiction
hence contradiction by A72, TOPREAL1:def_7; ::_thesis: verum
end;
end;
end;
0 + 1 <= (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 by A68, NAT_1:11;
then (Index ((SE-corner (L~ f)),g)) + 1 >= (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 by A3, A4, A7, A43, A44, A60, A64, A67, A68, A66, A70, JORDAN5C:28;
then (Index ((SE-corner (L~ f)),g)) + 1 >= ((Index ((SE-corner (L~ f)),g)) + 1) + 1 by A69, XXREAL_0:2;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
end;
end;
theorem Th40: :: SPRECT_3:40
for f being rectangular special_circular_sequence
for p being Point of (TOP-REAL 2) st ( W-bound (L~ f) > p `1 or p `1 > E-bound (L~ f) or S-bound (L~ f) > p `2 or p `2 > N-bound (L~ f) ) holds
p in LeftComp f
proof
let f be rectangular special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) st ( W-bound (L~ f) > p `1 or p `1 > E-bound (L~ f) or S-bound (L~ f) > p `2 or p `2 > N-bound (L~ f) ) holds
p in LeftComp f
let p be Point of (TOP-REAL 2); ::_thesis: ( ( W-bound (L~ f) > p `1 or p `1 > E-bound (L~ f) or S-bound (L~ f) > p `2 or p `2 > N-bound (L~ f) ) implies p in LeftComp f )
LeftComp f = { q where q is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= q `1 or not q `1 <= E-bound (L~ f) or not S-bound (L~ f) <= q `2 or not q `2 <= N-bound (L~ f) ) } by Th37;
hence ( ( W-bound (L~ f) > p `1 or p `1 > E-bound (L~ f) or S-bound (L~ f) > p `2 or p `2 > N-bound (L~ f) ) implies p in LeftComp f ) ; ::_thesis: verum
end;
theorem :: SPRECT_3:41
for f being non constant standard clockwise_oriented special_circular_sequence st f /. 1 = N-min (L~ f) holds
LeftComp (SpStSeq (L~ f)) c= LeftComp f
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( f /. 1 = N-min (L~ f) implies LeftComp (SpStSeq (L~ f)) c= LeftComp f )
assume A1: f /. 1 = N-min (L~ f) ; ::_thesis: LeftComp (SpStSeq (L~ f)) c= LeftComp f
defpred S1[ Element of (TOP-REAL 2)] means $1 `2 < S-bound (L~ f);
reconsider P1 = { p where p is Point of (TOP-REAL 2) : S1[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_7();
defpred S2[ Element of (TOP-REAL 2)] means $1 `2 > N-bound (L~ f);
reconsider P2 = { p where p is Point of (TOP-REAL 2) : S2[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_7();
defpred S3[ Element of (TOP-REAL 2)] means $1 `1 > E-bound (L~ f);
reconsider P3 = { p where p is Point of (TOP-REAL 2) : S3[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_7();
defpred S4[ Element of (TOP-REAL 2)] means $1 `1 < W-bound (L~ f);
reconsider P4 = { p where p is Point of (TOP-REAL 2) : S4[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_7();
A2: W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f) by SPRECT_1:58;
for p being Point of (TOP-REAL 2) st p in P2 holds
p `2 > ((GoB f) * (1,(width (GoB f)))) `2
proof
let p be Point of (TOP-REAL 2); ::_thesis: ( p in P2 implies p `2 > ((GoB f) * (1,(width (GoB f)))) `2 )
assume p in P2 ; ::_thesis: p `2 > ((GoB f) * (1,(width (GoB f)))) `2
then ex q being Point of (TOP-REAL 2) st
( p = q & q `2 > N-bound (L~ f) ) ;
hence p `2 > ((GoB f) * (1,(width (GoB f)))) `2 by JORDAN5D:40; ::_thesis: verum
end;
then A3: P2 misses L~ f by GOBOARD8:24;
A4: 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
A5: ((width (GoB f)) -' 1) + 1 = width (GoB f) by GOBRD11:34, XREAL_1:235;
consider i being Element of NAT such that
A6: 1 <= i and
A7: i < len (GoB f) and
A8: N-min (L~ f) = (GoB f) * (i,(width (GoB f))) by Th28;
A9: i + 1 <= len (GoB f) by A7, NAT_1:13;
A10: i in dom (GoB f) by A6, A7, FINSEQ_3:25;
then A11: f /. 2 = (GoB f) * ((i + 1),(width (GoB f))) by A1, A8, Th29;
A12: width (GoB f) >= 1 by GOBRD11:34;
then A13: [i,(width (GoB f))] in Indices (GoB f) by A6, A7, MATRIX_1:36;
A14: 1 <= i + 1 by A6, NAT_1:13;
then A15: (f /. 2) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A11, A12, A9, GOBOARD5:1
.= (N-min (L~ f)) `2 by A6, A7, A8, A12, GOBOARD5:1
.= N-bound (L~ f) by EUCLID:52 ;
set a = ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|;
set q = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))));
A16: (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2) + (|[0,1]| `2) by TOPREAL3:2
.= (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2) + 1 by EUCLID:52 ;
((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2 = ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + (f /. 2))) `2 by A1, A8, A10, Th29
.= (1 / 2) * (((f /. 1) + (f /. 2)) `2) by A1, A8, TOPREAL3:4
.= (1 / 2) * (((f /. 1) `2) + ((f /. 2) `2)) by TOPREAL3:2
.= (1 / 2) * ((N-bound (L~ f)) + (N-bound (L~ f))) by A1, A15, EUCLID:52
.= N-bound (L~ f) ;
then (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|) `2 > 0 + (N-bound (L~ f)) by A16, XREAL_1:8;
then A17: (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|) `2 > N-bound (L~ (SpStSeq (L~ f))) by SPRECT_1:60;
LeftComp (SpStSeq (L~ f)) = { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ (SpStSeq (L~ f))) <= p `1 or not p `1 <= E-bound (L~ (SpStSeq (L~ f))) or not S-bound (L~ (SpStSeq (L~ f))) <= p `2 or not p `2 <= N-bound (L~ (SpStSeq (L~ f))) ) } by Th37;
then A18: ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]| in LeftComp (SpStSeq (L~ f)) by A17;
[(i + 1),(width (GoB f))] in Indices (GoB f) by A12, A14, A9, MATRIX_1:36;
then left_cell (f,1) = cell ((GoB f),i,(width (GoB f))) by A1, A8, A11, A5, A4, A13, GOBOARD5:28;
then A19: Int (cell ((GoB f),i,(width (GoB f)))) c= LeftComp f by GOBOARD9:def_1;
((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]| in Int (cell ((GoB f),i,(width (GoB f)))) by A6, A9, GOBOARD6:32;
then A20: LeftComp f meets LeftComp (SpStSeq (L~ f)) by A19, A18, XBOOLE_0:3;
A21: S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f) by SPRECT_1:59;
for p being Point of (TOP-REAL 2) st p in P4 holds
p `1 < ((GoB f) * (1,1)) `1
proof
let p be Point of (TOP-REAL 2); ::_thesis: ( p in P4 implies p `1 < ((GoB f) * (1,1)) `1 )
assume p in P4 ; ::_thesis: p `1 < ((GoB f) * (1,1)) `1
then ex q being Point of (TOP-REAL 2) st
( p = q & q `1 < W-bound (L~ f) ) ;
hence p `1 < ((GoB f) * (1,1)) `1 by JORDAN5D:37; ::_thesis: verum
end;
then A22: P4 misses L~ f by GOBOARD8:21;
for p being Point of (TOP-REAL 2) st p in P3 holds
p `1 > ((GoB f) * ((len (GoB f)),1)) `1
proof
let p be Point of (TOP-REAL 2); ::_thesis: ( p in P3 implies p `1 > ((GoB f) * ((len (GoB f)),1)) `1 )
assume p in P3 ; ::_thesis: p `1 > ((GoB f) * ((len (GoB f)),1)) `1
then ex q being Point of (TOP-REAL 2) st
( p = q & q `1 > E-bound (L~ f) ) ;
hence p `1 > ((GoB f) * ((len (GoB f)),1)) `1 by JORDAN5D:39; ::_thesis: verum
end;
then P3 misses L~ f by GOBOARD8:22;
then A23: P3 \/ P4 misses L~ f by A22, XBOOLE_1:70;
LeftComp (SpStSeq (L~ f)) is_a_component_of (L~ (SpStSeq (L~ f))) ` by GOBOARD9:def_1;
then consider B1 being Subset of ((TOP-REAL 2) | ((L~ (SpStSeq (L~ f))) `)) such that
A24: B1 = LeftComp (SpStSeq (L~ f)) and
A25: B1 is a_component by CONNSP_1:def_6;
B1 is connected by A25, CONNSP_1:def_5;
then A26: LeftComp (SpStSeq (L~ f)) is connected by A24, CONNSP_1:23;
A27: E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) by SPRECT_1:61;
A28: N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f) by SPRECT_1:60;
A29: LeftComp (SpStSeq (L~ f)) = (P1 \/ P2) \/ (P3 \/ P4)
proof
thus LeftComp (SpStSeq (L~ f)) c= (P1 \/ P2) \/ (P3 \/ P4) :: according to XBOOLE_0:def_10 ::_thesis: (P1 \/ P2) \/ (P3 \/ P4) c= LeftComp (SpStSeq (L~ f))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LeftComp (SpStSeq (L~ f)) or x in (P1 \/ P2) \/ (P3 \/ P4) )
assume x in LeftComp (SpStSeq (L~ f)) ; ::_thesis: x in (P1 \/ P2) \/ (P3 \/ P4)
then x in { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) } by A28, A2, A21, A27, Th37;
then ex p being Point of (TOP-REAL 2) st
( p = x & ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) ) ;
then ( x in P1 or x in P2 or x in P3 or x in P4 ) ;
then ( x in P1 \/ P2 or x in P3 \/ P4 ) by XBOOLE_0:def_3;
hence x in (P1 \/ P2) \/ (P3 \/ P4) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (P1 \/ P2) \/ (P3 \/ P4) or x in LeftComp (SpStSeq (L~ f)) )
assume x in (P1 \/ P2) \/ (P3 \/ P4) ; ::_thesis: x in LeftComp (SpStSeq (L~ f))
then A30: ( x in P1 \/ P2 or x in P3 \/ P4 ) by XBOOLE_0:def_3;
percases ( x in P1 or x in P2 or x in P3 or x in P4 ) by A30, XBOOLE_0:def_3;
suppose x in P1 ; ::_thesis: x in LeftComp (SpStSeq (L~ f))
then ex p being Point of (TOP-REAL 2) st
( x = p & p `2 < S-bound (L~ f) ) ;
hence x in LeftComp (SpStSeq (L~ f)) by A21, Th40; ::_thesis: verum
end;
suppose x in P2 ; ::_thesis: x in LeftComp (SpStSeq (L~ f))
then ex p being Point of (TOP-REAL 2) st
( x = p & p `2 > N-bound (L~ f) ) ;
hence x in LeftComp (SpStSeq (L~ f)) by A28, Th40; ::_thesis: verum
end;
suppose x in P3 ; ::_thesis: x in LeftComp (SpStSeq (L~ f))
then ex p being Point of (TOP-REAL 2) st
( x = p & p `1 > E-bound (L~ f) ) ;
hence x in LeftComp (SpStSeq (L~ f)) by A27, Th40; ::_thesis: verum
end;
suppose x in P4 ; ::_thesis: x in LeftComp (SpStSeq (L~ f))
then ex p being Point of (TOP-REAL 2) st
( x = p & p `1 < W-bound (L~ f) ) ;
hence x in LeftComp (SpStSeq (L~ f)) by A2, Th40; ::_thesis: verum
end;
end;
end;
for p being Point of (TOP-REAL 2) st p in P1 holds
p `2 < ((GoB f) * (1,1)) `2
proof
let p be Point of (TOP-REAL 2); ::_thesis: ( p in P1 implies p `2 < ((GoB f) * (1,1)) `2 )
assume p in P1 ; ::_thesis: p `2 < ((GoB f) * (1,1)) `2
then ex q being Point of (TOP-REAL 2) st
( p = q & q `2 < S-bound (L~ f) ) ;
hence p `2 < ((GoB f) * (1,1)) `2 by JORDAN5D:38; ::_thesis: verum
end;
then P1 misses L~ f by GOBOARD8:23;
then P1 \/ P2 misses L~ f by A3, XBOOLE_1:70;
then LeftComp (SpStSeq (L~ f)) misses L~ f by A29, A23, XBOOLE_1:70;
then A31: LeftComp (SpStSeq (L~ f)) c= (L~ f) ` by SUBSET_1:23;
LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1;
hence LeftComp (SpStSeq (L~ f)) c= LeftComp f by A26, A20, A31, GOBOARD9:4; ::_thesis: verum
end;
begin
theorem Th42: :: SPRECT_3:42
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) holds
( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) )
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) holds
( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) )
let p, q be Point of (TOP-REAL 2); ::_thesis: ( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) )
thus ( <*p,q*> is_in_the_area_of f implies ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) ) ::_thesis: ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f implies <*p,q*> is_in_the_area_of f )
proof
A1: dom <*p,q*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then A2: 1 in dom <*p,q*> by TARSKI:def_2;
assume A3: <*p,q*> is_in_the_area_of f ; ::_thesis: ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f )
A4: <*p,q*> /. 1 = p by FINSEQ_4:17;
then A5: p `1 <= E-bound (L~ f) by A3, A2, SPRECT_2:def_1;
A6: p `2 <= N-bound (L~ f) by A3, A2, A4, SPRECT_2:def_1;
A7: S-bound (L~ f) <= p `2 by A3, A2, A4, SPRECT_2:def_1;
A8: W-bound (L~ f) <= p `1 by A3, A2, A4, SPRECT_2:def_1;
thus <*p*> is_in_the_area_of f ::_thesis: <*q*> is_in_the_area_of f
proof
let i be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not i in dom <*p*> or ( W-bound (L~ f) <= (<*p*> /. i) `1 & (<*p*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p*> /. i) `2 & (<*p*> /. i) `2 <= N-bound (L~ f) ) )
assume i in dom <*p*> ; ::_thesis: ( W-bound (L~ f) <= (<*p*> /. i) `1 & (<*p*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p*> /. i) `2 & (<*p*> /. i) `2 <= N-bound (L~ f) )
then i in {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by TARSKI:def_1;
hence ( W-bound (L~ f) <= (<*p*> /. i) `1 & (<*p*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p*> /. i) `2 & (<*p*> /. i) `2 <= N-bound (L~ f) ) by A8, A5, A7, A6, FINSEQ_4:16; ::_thesis: verum
end;
let i be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not i in dom <*q*> or ( W-bound (L~ f) <= (<*q*> /. i) `1 & (<*q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*q*> /. i) `2 & (<*q*> /. i) `2 <= N-bound (L~ f) ) )
assume i in dom <*q*> ; ::_thesis: ( W-bound (L~ f) <= (<*q*> /. i) `1 & (<*q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*q*> /. i) `2 & (<*q*> /. i) `2 <= N-bound (L~ f) )
then i in {1} by FINSEQ_1:2, FINSEQ_1:38;
then A9: i = 1 by TARSKI:def_1;
A10: <*p,q*> /. 2 = q by FINSEQ_4:17;
A11: 2 in dom <*p,q*> by A1, TARSKI:def_2;
then A12: q `1 <= E-bound (L~ f) by A3, A10, SPRECT_2:def_1;
A13: q `2 <= N-bound (L~ f) by A3, A11, A10, SPRECT_2:def_1;
A14: S-bound (L~ f) <= q `2 by A3, A11, A10, SPRECT_2:def_1;
W-bound (L~ f) <= q `1 by A3, A11, A10, SPRECT_2:def_1;
hence ( W-bound (L~ f) <= (<*q*> /. i) `1 & (<*q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*q*> /. i) `2 & (<*q*> /. i) `2 <= N-bound (L~ f) ) by A12, A14, A13, A9, FINSEQ_4:16; ::_thesis: verum
end;
A15: <*p*> /. 1 = p by FINSEQ_4:16;
dom <*q*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A16: 1 in dom <*q*> by TARSKI:def_1;
dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A17: 1 in dom <*p*> by TARSKI:def_1;
assume A18: <*p*> is_in_the_area_of f ; ::_thesis: ( not <*q*> is_in_the_area_of f or <*p,q*> is_in_the_area_of f )
then A19: p `1 <= E-bound (L~ f) by A17, A15, SPRECT_2:def_1;
A20: p `2 <= N-bound (L~ f) by A18, A17, A15, SPRECT_2:def_1;
A21: S-bound (L~ f) <= p `2 by A18, A17, A15, SPRECT_2:def_1;
A22: <*q*> /. 1 = q by FINSEQ_4:16;
assume A23: <*q*> is_in_the_area_of f ; ::_thesis: <*p,q*> is_in_the_area_of f
then A24: W-bound (L~ f) <= q `1 by A16, A22, SPRECT_2:def_1;
A25: q `1 <= E-bound (L~ f) by A23, A16, A22, SPRECT_2:def_1;
let i be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not i in dom <*p,q*> or ( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) ) )
assume i in dom <*p,q*> ; ::_thesis: ( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) )
then i in {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then A26: ( i = 1 or i = 2 ) by TARSKI:def_2;
A27: q `2 <= N-bound (L~ f) by A23, A16, A22, SPRECT_2:def_1;
A28: S-bound (L~ f) <= q `2 by A23, A16, A22, SPRECT_2:def_1;
W-bound (L~ f) <= p `1 by A18, A17, A15, SPRECT_2:def_1;
hence ( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) ) by A19, A21, A20, A24, A25, A28, A27, A26, FINSEQ_4:17; ::_thesis: verum
end;
theorem Th43: :: SPRECT_3:43
for f being rectangular FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st <*p*> is_in_the_area_of f & ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) holds
p in L~ f
proof
let f be rectangular FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st <*p*> is_in_the_area_of f & ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) holds
p in L~ f
let p be Point of (TOP-REAL 2); ::_thesis: ( <*p*> is_in_the_area_of f & ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) implies p in L~ f )
A1: <*p*> /. 1 = p by FINSEQ_4:16;
dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A2: 1 in dom <*p*> by TARSKI:def_1;
assume A3: <*p*> is_in_the_area_of f ; ::_thesis: ( ( not p `1 = W-bound (L~ f) & not p `1 = E-bound (L~ f) & not p `2 = S-bound (L~ f) & not p `2 = N-bound (L~ f) ) or p in L~ f )
then A4: W-bound (L~ f) <= p `1 by A2, A1, SPRECT_2:def_1;
A5: p `2 <= N-bound (L~ f) by A3, A2, A1, SPRECT_2:def_1;
A6: S-bound (L~ f) <= p `2 by A3, A2, A1, SPRECT_2:def_1;
A7: p `1 <= E-bound (L~ f) by A3, A2, A1, SPRECT_2:def_1;
consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that
A8: f = SpStSeq D by SPRECT_1:def_2;
A9: E-bound (L~ (SpStSeq D)) = E-bound D by SPRECT_1:61;
A10: N-bound (L~ (SpStSeq D)) = N-bound D by SPRECT_1:60;
A11: S-bound (L~ (SpStSeq D)) = S-bound D by SPRECT_1:59;
A12: W-bound (L~ (SpStSeq D)) = W-bound D by SPRECT_1:58;
A13: L~ f = ((LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D)))) \/ ((LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D)))) by A8, SPRECT_1:41;
assume A14: ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) ; ::_thesis: p in L~ f
percases ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) by A14;
supposeA15: p `1 = W-bound (L~ f) ; ::_thesis: p in L~ f
A16: (NW-corner D) `1 = W-bound D by EUCLID:52;
A17: (NW-corner D) `2 = N-bound D by EUCLID:52;
A18: (SW-corner D) `2 = S-bound D by EUCLID:52;
(SW-corner D) `1 = W-bound D by EUCLID:52;
then p in LSeg ((SW-corner D),(NW-corner D)) by A6, A5, A8, A12, A11, A10, A15, A16, A18, A17, GOBOARD7:7;
then p in (LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D))) by XBOOLE_0:def_3;
hence p in L~ f by A13, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA19: p `1 = E-bound (L~ f) ; ::_thesis: p in L~ f
A20: (SE-corner D) `1 = E-bound D by EUCLID:52;
A21: (SE-corner D) `2 = S-bound D by EUCLID:52;
A22: (NE-corner D) `2 = N-bound D by EUCLID:52;
(NE-corner D) `1 = E-bound D by EUCLID:52;
then p in LSeg ((NE-corner D),(SE-corner D)) by A6, A5, A8, A11, A10, A9, A19, A20, A22, A21, GOBOARD7:7;
then p in (LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D))) by XBOOLE_0:def_3;
hence p in L~ f by A13, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA23: p `2 = S-bound (L~ f) ; ::_thesis: p in L~ f
A24: (SW-corner D) `1 = W-bound D by EUCLID:52;
A25: (SW-corner D) `2 = S-bound D by EUCLID:52;
A26: (SE-corner D) `2 = S-bound D by EUCLID:52;
(SE-corner D) `1 = E-bound D by EUCLID:52;
then p in LSeg ((SE-corner D),(SW-corner D)) by A4, A7, A8, A12, A11, A9, A23, A24, A26, A25, GOBOARD7:8;
then p in (LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D))) by XBOOLE_0:def_3;
hence p in L~ f by A13, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA27: p `2 = N-bound (L~ f) ; ::_thesis: p in L~ f
A28: (NE-corner D) `1 = E-bound D by EUCLID:52;
A29: (NE-corner D) `2 = N-bound D by EUCLID:52;
A30: (NW-corner D) `2 = N-bound D by EUCLID:52;
(NW-corner D) `1 = W-bound D by EUCLID:52;
then p in LSeg ((NW-corner D),(NE-corner D)) by A4, A7, A8, A12, A10, A9, A27, A28, A30, A29, GOBOARD7:8;
then p in (LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D))) by XBOOLE_0:def_3;
hence p in L~ f by A13, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
theorem Th44: :: SPRECT_3:44
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2)
for r being Real st 0 <= r & r <= 1 & <*p,q*> is_in_the_area_of f holds
<*(((1 - r) * p) + (r * q))*> is_in_the_area_of f
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2)
for r being Real st 0 <= r & r <= 1 & <*p,q*> is_in_the_area_of f holds
<*(((1 - r) * p) + (r * q))*> is_in_the_area_of f
let p, q be Point of (TOP-REAL 2); ::_thesis: for r being Real st 0 <= r & r <= 1 & <*p,q*> is_in_the_area_of f holds
<*(((1 - r) * p) + (r * q))*> is_in_the_area_of f
let r be Real; ::_thesis: ( 0 <= r & r <= 1 & <*p,q*> is_in_the_area_of f implies <*(((1 - r) * p) + (r * q))*> is_in_the_area_of f )
assume that
A1: 0 <= r and
A2: r <= 1 and
A3: <*p,q*> is_in_the_area_of f ; ::_thesis: <*(((1 - r) * p) + (r * q))*> is_in_the_area_of f
A4: dom <*p,q*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then A5: 2 in dom <*p,q*> by TARSKI:def_2;
A6: <*p,q*> /. 2 = q by FINSEQ_4:17;
then W-bound (L~ f) <= q `1 by A3, A5, SPRECT_2:def_1;
then A7: r * (W-bound (L~ f)) <= r * (q `1) by A1, XREAL_1:64;
q `1 <= E-bound (L~ f) by A3, A5, A6, SPRECT_2:def_1;
then A8: r * (q `1) <= r * (E-bound (L~ f)) by A1, XREAL_1:64;
A9: <*p,q*> /. 1 = p by FINSEQ_4:17;
A10: 1 - r >= 0 by A2, XREAL_1:48;
A11: 1 in dom <*p,q*> by A4, TARSKI:def_2;
then W-bound (L~ f) <= p `1 by A3, A9, SPRECT_2:def_1;
then A12: (1 - r) * (W-bound (L~ f)) <= (1 - r) * (p `1) by A10, XREAL_1:64;
p `1 <= E-bound (L~ f) by A3, A11, A9, SPRECT_2:def_1;
then A13: (1 - r) * (p `1) <= (1 - r) * (E-bound (L~ f)) by A10, XREAL_1:64;
S-bound (L~ f) <= p `2 by A3, A11, A9, SPRECT_2:def_1;
then A14: (1 - r) * (S-bound (L~ f)) <= (1 - r) * (p `2) by A10, XREAL_1:64;
A15: (((1 - r) * p) + (r * q)) `1 = (((1 - r) * p) `1) + ((r * q) `1) by TOPREAL3:2
.= ((1 - r) * (p `1)) + ((r * q) `1) by TOPREAL3:4
.= ((1 - r) * (p `1)) + (r * (q `1)) by TOPREAL3:4 ;
p `2 <= N-bound (L~ f) by A3, A11, A9, SPRECT_2:def_1;
then A16: (1 - r) * (p `2) <= (1 - r) * (N-bound (L~ f)) by A10, XREAL_1:64;
let n be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not n in dom <*(((1 - r) * p) + (r * q))*> or ( W-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `1 & (<*(((1 - r) * p) + (r * q))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 & (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) ) )
A17: dom <*(((1 - r) * p) + (r * q))*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
assume n in dom <*(((1 - r) * p) + (r * q))*> ; ::_thesis: ( W-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `1 & (<*(((1 - r) * p) + (r * q))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 & (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) )
then A18: n = 1 by A17, TARSKI:def_1;
((1 - r) * (W-bound (L~ f))) + (r * (W-bound (L~ f))) = 1 * (W-bound (L~ f)) ;
then W-bound (L~ f) <= ((1 - r) * (p `1)) + (r * (q `1)) by A7, A12, XREAL_1:7;
hence W-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `1 by A18, A15, FINSEQ_4:16; ::_thesis: ( (<*(((1 - r) * p) + (r * q))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 & (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) )
((1 - r) * (E-bound (L~ f))) + (r * (E-bound (L~ f))) = 1 * (E-bound (L~ f)) ;
then ((1 - r) * (p `1)) + (r * (q `1)) <= E-bound (L~ f) by A8, A13, XREAL_1:7;
hence (<*(((1 - r) * p) + (r * q))*> /. n) `1 <= E-bound (L~ f) by A18, A15, FINSEQ_4:16; ::_thesis: ( S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 & (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) )
A19: (((1 - r) * p) + (r * q)) `2 = (((1 - r) * p) `2) + ((r * q) `2) by TOPREAL3:2
.= ((1 - r) * (p `2)) + ((r * q) `2) by TOPREAL3:4
.= ((1 - r) * (p `2)) + (r * (q `2)) by TOPREAL3:4 ;
q `2 <= N-bound (L~ f) by A3, A5, A6, SPRECT_2:def_1;
then A20: r * (q `2) <= r * (N-bound (L~ f)) by A1, XREAL_1:64;
S-bound (L~ f) <= q `2 by A3, A5, A6, SPRECT_2:def_1;
then A21: r * (S-bound (L~ f)) <= r * (q `2) by A1, XREAL_1:64;
((1 - r) * (S-bound (L~ f))) + (r * (S-bound (L~ f))) = 1 * (S-bound (L~ f)) ;
then S-bound (L~ f) <= ((1 - r) * (p `2)) + (r * (q `2)) by A21, A14, XREAL_1:7;
hence S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 by A18, A19, FINSEQ_4:16; ::_thesis: (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f)
((1 - r) * (N-bound (L~ f))) + (r * (N-bound (L~ f))) = 1 * (N-bound (L~ f)) ;
then ((1 - r) * (p `2)) + (r * (q `2)) <= N-bound (L~ f) by A20, A16, XREAL_1:7;
hence (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) by A18, A19, FINSEQ_4:16; ::_thesis: verum
end;
theorem Th45: :: SPRECT_3:45
for i being Element of NAT
for f, g being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f & i in dom g holds
<*(g /. i)*> is_in_the_area_of f
proof
let i be Element of NAT ; ::_thesis: for f, g being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f & i in dom g holds
<*(g /. i)*> is_in_the_area_of f
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( g is_in_the_area_of f & i in dom g implies <*(g /. i)*> is_in_the_area_of f )
assume that
A1: g is_in_the_area_of f and
A2: i in dom g ; ::_thesis: <*(g /. i)*> is_in_the_area_of f
let n be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not n in dom <*(g /. i)*> or ( W-bound (L~ f) <= (<*(g /. i)*> /. n) `1 & (<*(g /. i)*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(g /. i)*> /. n) `2 & (<*(g /. i)*> /. n) `2 <= N-bound (L~ f) ) )
A3: dom <*(g /. i)*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
assume n in dom <*(g /. i)*> ; ::_thesis: ( W-bound (L~ f) <= (<*(g /. i)*> /. n) `1 & (<*(g /. i)*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(g /. i)*> /. n) `2 & (<*(g /. i)*> /. n) `2 <= N-bound (L~ f) )
then n = 1 by A3, TARSKI:def_1;
then <*(g /. i)*> /. n = g /. i by FINSEQ_4:16;
hence ( W-bound (L~ f) <= (<*(g /. i)*> /. n) `1 & (<*(g /. i)*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(g /. i)*> /. n) `2 & (<*(g /. i)*> /. n) `2 <= N-bound (L~ f) ) by A1, A2, SPRECT_2:def_1; ::_thesis: verum
end;
theorem Th46: :: SPRECT_3:46
for f, g being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & p in L~ g holds
<*p*> is_in_the_area_of f
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & p in L~ g holds
<*p*> is_in_the_area_of f
let p be Point of (TOP-REAL 2); ::_thesis: ( g is_in_the_area_of f & p in L~ g implies <*p*> is_in_the_area_of f )
assume A1: g is_in_the_area_of f ; ::_thesis: ( not p in L~ g or <*p*> is_in_the_area_of f )
assume p in L~ g ; ::_thesis: <*p*> is_in_the_area_of f
then consider i being Element of NAT such that
A2: 1 <= i and
A3: i + 1 <= len g and
A4: p in LSeg ((g /. i),(g /. (i + 1))) by SPPOL_2:14;
A5: ex r being Real st
( p = ((1 - r) * (g /. i)) + (r * (g /. (i + 1))) & 0 <= r & r <= 1 ) by A4;
i <= i + 1 by NAT_1:11;
then i <= len g by A3, XXREAL_0:2;
then i in dom g by A2, FINSEQ_3:25;
then A6: <*(g /. i)*> is_in_the_area_of f by A1, Th45;
1 <= i + 1 by NAT_1:11;
then i + 1 in dom g by A3, FINSEQ_3:25;
then <*(g /. (i + 1))*> is_in_the_area_of f by A1, Th45;
then <*(g /. i),(g /. (i + 1))*> is_in_the_area_of f by A6, Th42;
hence <*p*> is_in_the_area_of f by A5, Th44; ::_thesis: verum
end;
theorem Th47: :: SPRECT_3:47
for f being rectangular FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st not q in L~ f & <*p,q*> is_in_the_area_of f holds
(LSeg (p,q)) /\ (L~ f) c= {p}
proof
let f be rectangular FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st not q in L~ f & <*p,q*> is_in_the_area_of f holds
(LSeg (p,q)) /\ (L~ f) c= {p}
let p, q be Point of (TOP-REAL 2); ::_thesis: ( not q in L~ f & <*p,q*> is_in_the_area_of f implies (LSeg (p,q)) /\ (L~ f) c= {p} )
assume A1: not q in L~ f ; ::_thesis: ( not <*p,q*> is_in_the_area_of f or (LSeg (p,q)) /\ (L~ f) c= {p} )
assume A2: <*p,q*> is_in_the_area_of f ; ::_thesis: (LSeg (p,q)) /\ (L~ f) c= {p}
A3: dom <*p,q*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then A4: 2 in dom <*p,q*> by TARSKI:def_2;
A5: <*p,q*> /. 2 = q by FINSEQ_4:17;
then A6: W-bound (L~ f) <= q `1 by A2, A4, SPRECT_2:def_1;
A7: <*q*> is_in_the_area_of f by A2, Th42;
then q `1 <> W-bound (L~ f) by A1, Th43;
then A8: W-bound (L~ f) < q `1 by A6, XXREAL_0:1;
A9: q `2 <= N-bound (L~ f) by A2, A4, A5, SPRECT_2:def_1;
q `2 <> N-bound (L~ f) by A1, A7, Th43;
then A10: q `2 < N-bound (L~ f) by A9, XXREAL_0:1;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LSeg (p,q)) /\ (L~ f) or x in {p} )
A11: <*p,q*> /. 1 = p by FINSEQ_4:17;
A12: q `1 <= E-bound (L~ f) by A2, A4, A5, SPRECT_2:def_1;
q `1 <> E-bound (L~ f) by A1, A7, Th43;
then A13: q `1 < E-bound (L~ f) by A12, XXREAL_0:1;
assume A14: x in (LSeg (p,q)) /\ (L~ f) ; ::_thesis: x in {p}
then reconsider p9 = x as Point of (TOP-REAL 2) ;
A15: p9 in L~ f by A14, XBOOLE_0:def_4;
A16: 1 in dom <*p,q*> by A3, TARSKI:def_2;
then A17: W-bound (L~ f) <= p `1 by A2, A11, SPRECT_2:def_1;
A18: p `2 <= N-bound (L~ f) by A2, A16, A11, SPRECT_2:def_1;
A19: S-bound (L~ f) <= p `2 by A2, A16, A11, SPRECT_2:def_1;
A20: p `1 <= E-bound (L~ f) by A2, A16, A11, SPRECT_2:def_1;
A21: S-bound (L~ f) <= q `2 by A2, A4, A5, SPRECT_2:def_1;
q `2 <> S-bound (L~ f) by A1, A7, Th43;
then A22: S-bound (L~ f) < q `2 by A21, XXREAL_0:1;
x in LSeg (p,q) by A14, XBOOLE_0:def_4;
then consider r being Real such that
A23: p9 = ((1 - r) * p) + (r * q) and
A24: 0 <= r and
A25: r <= 1 ;
A26: p9 `1 = (((1 - r) * p) `1) + ((r * q) `1) by A23, TOPREAL3:2
.= ((1 - r) * (p `1)) + ((r * q) `1) by TOPREAL3:4
.= ((1 - r) * (p `1)) + (r * (q `1)) by TOPREAL3:4 ;
A27: p9 `2 = (((1 - r) * p) `2) + ((r * q) `2) by A23, TOPREAL3:2
.= ((1 - r) * (p `2)) + ((r * q) `2) by TOPREAL3:4
.= ((1 - r) * (p `2)) + (r * (q `2)) by TOPREAL3:4 ;
percases ( p9 `1 = W-bound (L~ f) or p9 `1 = E-bound (L~ f) or p9 `2 = S-bound (L~ f) or p9 `2 = N-bound (L~ f) ) by A15, Th32;
suppose p9 `1 = W-bound (L~ f) ; ::_thesis: x in {p}
then r = 0 by A17, A8, A24, A25, A26, XREAL_1:180;
then p9 = (1 * p) + (0. (TOP-REAL 2)) by A23, EUCLID:29
.= 1 * p by EUCLID:27
.= p by EUCLID:29 ;
hence x in {p} by ZFMISC_1:31; ::_thesis: verum
end;
suppose p9 `1 = E-bound (L~ f) ; ::_thesis: x in {p}
then r = 0 by A20, A13, A24, A25, A26, XREAL_1:179;
then p9 = (1 * p) + (0. (TOP-REAL 2)) by A23, EUCLID:29
.= 1 * p by EUCLID:27
.= p by EUCLID:29 ;
hence x in {p} by ZFMISC_1:31; ::_thesis: verum
end;
suppose p9 `2 = S-bound (L~ f) ; ::_thesis: x in {p}
then r = 0 by A19, A22, A24, A25, A27, XREAL_1:180;
then p9 = (1 * p) + (0. (TOP-REAL 2)) by A23, EUCLID:29
.= 1 * p by EUCLID:27
.= p by EUCLID:29 ;
hence x in {p} by ZFMISC_1:31; ::_thesis: verum
end;
suppose p9 `2 = N-bound (L~ f) ; ::_thesis: x in {p}
then r = 0 by A18, A10, A24, A25, A27, XREAL_1:179;
then p9 = (1 * p) + (0. (TOP-REAL 2)) by A23, EUCLID:29
.= 1 * p by EUCLID:27
.= p by EUCLID:29 ;
hence x in {p} by ZFMISC_1:31; ::_thesis: verum
end;
end;
end;
theorem :: SPRECT_3:48
for f being rectangular FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f & not q in L~ f & <*q*> is_in_the_area_of f holds
(LSeg (p,q)) /\ (L~ f) = {p}
proof
let f be rectangular FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & not q in L~ f & <*q*> is_in_the_area_of f holds
(LSeg (p,q)) /\ (L~ f) = {p}
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & not q in L~ f & <*q*> is_in_the_area_of f implies (LSeg (p,q)) /\ (L~ f) = {p} )
assume that
A1: p in L~ f and
A2: not q in L~ f and
A3: <*q*> is_in_the_area_of f ; ::_thesis: (LSeg (p,q)) /\ (L~ f) = {p}
A4: <*p,q*> = <*p*> ^ <*q*> by FINSEQ_1:def_9;
<*p*> is_in_the_area_of f by A1, Th46, SPRECT_2:21;
hence (LSeg (p,q)) /\ (L~ f) c= {p} by A2, A3, A4, Th47, SPRECT_2:24; :: according to XBOOLE_0:def_10 ::_thesis: {p} c= (LSeg (p,q)) /\ (L~ f)
p in LSeg (p,q) by RLTOPSP1:68;
then p in (LSeg (p,q)) /\ (L~ f) by A1, XBOOLE_0:def_4;
hence {p} c= (LSeg (p,q)) /\ (L~ f) by ZFMISC_1:31; ::_thesis: verum
end;
theorem Th49: :: SPRECT_3:49
for i, j being Element of NAT
for f being non constant standard special_circular_sequence st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds
<*((GoB f) * (i,j))*> is_in_the_area_of f
proof
let i, j be Element of NAT ; ::_thesis: for f being non constant standard special_circular_sequence st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds
<*((GoB f) * (i,j))*> is_in_the_area_of f
let f be non constant standard special_circular_sequence; ::_thesis: ( 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) implies <*((GoB f) * (i,j))*> is_in_the_area_of f )
assume that
A1: 1 <= i and
A2: i <= len (GoB f) and
A3: 1 <= j and
A4: j <= width (GoB f) ; ::_thesis: <*((GoB f) * (i,j))*> is_in_the_area_of f
set G = GoB f;
A5: 1 <= width (GoB f) by A3, A4, XXREAL_0:2;
A6: 1 <= len (GoB f) by A1, A2, XXREAL_0:2;
A7: N-bound (L~ f) = ((GoB f) * (1,(width (GoB f)))) `2 by JORDAN5D:40
.= ((GoB f) * (i,(width (GoB f)))) `2 by A1, A2, A5, GOBOARD5:1 ;
A8: ( j = 1 or j > 1 ) by A3, XXREAL_0:1;
A9: S-bound (L~ f) = ((GoB f) * (1,1)) `2 by JORDAN5D:38
.= ((GoB f) * (i,1)) `2 by A1, A2, A5, GOBOARD5:1 ;
A10: ( i = 1 or i > 1 ) by A1, XXREAL_0:1;
A11: E-bound (L~ f) = ((GoB f) * ((len (GoB f)),1)) `1 by JORDAN5D:39
.= ((GoB f) * ((len (GoB f)),j)) `1 by A3, A4, A6, GOBOARD5:2 ;
A12: ( j = width (GoB f) or j < width (GoB f) ) by A4, XXREAL_0:1;
A13: ( i = len (GoB f) or i < len (GoB f) ) by A2, XXREAL_0:1;
let n be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not n in dom <*((GoB f) * (i,j))*> or ( W-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `1 & (<*((GoB f) * (i,j))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `2 & (<*((GoB f) * (i,j))*> /. n) `2 <= N-bound (L~ f) ) )
set p = (GoB f) * (i,j);
assume n in dom <*((GoB f) * (i,j))*> ; ::_thesis: ( W-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `1 & (<*((GoB f) * (i,j))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `2 & (<*((GoB f) * (i,j))*> /. n) `2 <= N-bound (L~ f) )
then n in {1} by FINSEQ_1:2, FINSEQ_1:38;
then n = 1 by TARSKI:def_1;
then A14: <*((GoB f) * (i,j))*> /. n = (GoB f) * (i,j) by FINSEQ_4:16;
W-bound (L~ f) = ((GoB f) * (1,1)) `1 by JORDAN5D:37
.= ((GoB f) * (1,j)) `1 by A3, A4, A6, GOBOARD5:2 ;
hence ( W-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `1 & (<*((GoB f) * (i,j))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `2 & (<*((GoB f) * (i,j))*> /. n) `2 <= N-bound (L~ f) ) by A14, A10, A9, A8, A11, A13, A7, A12, GOBOARD5:3, GOBOARD5:4; ::_thesis: verum
end;
theorem :: SPRECT_3:50
for g being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st <*p,q*> is_in_the_area_of g holds
<*((1 / 2) * (p + q))*> is_in_the_area_of g
proof
let g be FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st <*p,q*> is_in_the_area_of g holds
<*((1 / 2) * (p + q))*> is_in_the_area_of g
let p, q be Point of (TOP-REAL 2); ::_thesis: ( <*p,q*> is_in_the_area_of g implies <*((1 / 2) * (p + q))*> is_in_the_area_of g )
(1 / 2) * (p + q) = ((1 - (1 / 2)) * p) + ((1 / 2) * q) by EUCLID:32;
hence ( <*p,q*> is_in_the_area_of g implies <*((1 / 2) * (p + q))*> is_in_the_area_of g ) by Th44; ::_thesis: verum
end;
theorem :: SPRECT_3:51
for f, g being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f holds
Rev g is_in_the_area_of f
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( g is_in_the_area_of f implies Rev g is_in_the_area_of f )
assume A1: g is_in_the_area_of f ; ::_thesis: Rev g is_in_the_area_of f
A2: Rev (Rev g) = g ;
let n be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not n in dom (Rev g) or ( W-bound (L~ f) <= ((Rev g) /. n) `1 & ((Rev g) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((Rev g) /. n) `2 & ((Rev g) /. n) `2 <= N-bound (L~ f) ) )
assume A3: n in dom (Rev g) ; ::_thesis: ( W-bound (L~ f) <= ((Rev g) /. n) `1 & ((Rev g) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((Rev g) /. n) `2 & ((Rev g) /. n) `2 <= N-bound (L~ f) )
n >= 1 by A3, FINSEQ_3:25;
then A4: n - 1 >= 0 by XREAL_1:48;
set i = ((len g) + 1) -' n;
A5: len (Rev g) = len g by FINSEQ_5:def_3;
then A6: n <= len g by A3, FINSEQ_3:25;
then A7: ((len g) + 1) -' n = ((len g) -' n) + 1 by NAT_D:38;
then ((len g) + 1) -' n = ((len g) - n) + 1 by A6, XREAL_1:233
.= (len g) - (n - 1) ;
then A8: ((len g) + 1) -' n <= (len g) - 0 by A4, XREAL_1:13;
1 <= ((len g) + 1) -' n by A7, NAT_1:11;
then A9: ((len g) + 1) -' n in dom g by A8, FINSEQ_3:25;
len g <= (len g) + 1 by NAT_1:11;
then n + (((len g) + 1) -' n) = (len g) + 1 by A6, XREAL_1:235, XXREAL_0:2;
then (Rev g) /. n = g /. (((len g) + 1) -' n) by A2, A5, A3, FINSEQ_5:66;
hence ( W-bound (L~ f) <= ((Rev g) /. n) `1 & ((Rev g) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((Rev g) /. n) `2 & ((Rev g) /. n) `2 <= N-bound (L~ f) ) by A1, A9, SPRECT_2:def_1; ::_thesis: verum
end;
theorem :: SPRECT_3:52
for f, g being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g holds
R_Cut (g,p) is_in_the_area_of f
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g holds
R_Cut (g,p) is_in_the_area_of f
let p be Point of (TOP-REAL 2); ::_thesis: ( g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g implies R_Cut (g,p) is_in_the_area_of f )
assume that
A1: g is_in_the_area_of f and
A2: <*p*> is_in_the_area_of f and
A3: g is being_S-Seq ; ::_thesis: ( not p in L~ g or R_Cut (g,p) is_in_the_area_of f )
2 <= len g by A3, TOPREAL1:def_8;
then A4: 1 <= len g by XXREAL_0:2;
then A5: 1 in dom g by FINSEQ_3:25;
assume A6: p in L~ g ; ::_thesis: R_Cut (g,p) is_in_the_area_of f
then A7: Index (p,g) < len g by JORDAN3:8;
1 <= Index (p,g) by A6, JORDAN3:8;
then A8: Index (p,g) in dom g by A7, FINSEQ_3:25;
percases ( p <> g . 1 or p = g . 1 ) ;
suppose p <> g . 1 ; ::_thesis: R_Cut (g,p) is_in_the_area_of f
then A9: R_Cut (g,p) = (mid (g,1,(Index (p,g)))) ^ <*p*> by JORDAN3:def_4;
mid (g,1,(Index (p,g))) is_in_the_area_of f by A1, A5, A8, SPRECT_2:22;
hence R_Cut (g,p) is_in_the_area_of f by A2, A9, SPRECT_2:24; ::_thesis: verum
end;
suppose p = g . 1 ; ::_thesis: R_Cut (g,p) is_in_the_area_of f
then R_Cut (g,p) = <*(g . 1)*> by JORDAN3:def_4
.= <*(g /. 1)*> by A5, PARTFUN1:def_6
.= mid (g,1,1) by A4, JORDAN4:15 ;
hence R_Cut (g,p) is_in_the_area_of f by A1, A5, SPRECT_2:22; ::_thesis: verum
end;
end;
end;
theorem :: SPRECT_3:53
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2) holds
( g is_in_the_area_of f iff g is_in_the_area_of SpStSeq (L~ f) )
proof
let f be non constant standard special_circular_sequence; ::_thesis: for g being FinSequence of (TOP-REAL 2) holds
( g is_in_the_area_of f iff g is_in_the_area_of SpStSeq (L~ f) )
let g be FinSequence of (TOP-REAL 2); ::_thesis: ( g is_in_the_area_of f iff g is_in_the_area_of SpStSeq (L~ f) )
A1: S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f) by SPRECT_1:59;
A2: N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f) by SPRECT_1:60;
A3: E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) by SPRECT_1:61;
A4: W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f) by SPRECT_1:58;
thus ( g is_in_the_area_of f implies g is_in_the_area_of SpStSeq (L~ f) ) ::_thesis: ( g is_in_the_area_of SpStSeq (L~ f) implies g is_in_the_area_of f )
proof
assume A5: g is_in_the_area_of f ; ::_thesis: g is_in_the_area_of SpStSeq (L~ f)
let n be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not n in dom g or ( W-bound (L~ (SpStSeq (L~ f))) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ (SpStSeq (L~ f))) & S-bound (L~ (SpStSeq (L~ f))) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ (SpStSeq (L~ f))) ) )
thus ( not n in dom g or ( W-bound (L~ (SpStSeq (L~ f))) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ (SpStSeq (L~ f))) & S-bound (L~ (SpStSeq (L~ f))) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ (SpStSeq (L~ f))) ) ) by A4, A1, A2, A3, A5, SPRECT_2:def_1; ::_thesis: verum
end;
assume A6: g is_in_the_area_of SpStSeq (L~ f) ; ::_thesis: g is_in_the_area_of f
let n be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not n in dom g or ( W-bound (L~ f) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ f) ) )
thus ( not n in dom g or ( W-bound (L~ f) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ f) ) ) by A4, A1, A2, A3, A6, SPRECT_2:def_1; ::_thesis: verum
end;
theorem :: SPRECT_3:54
for f being rectangular special_circular_sequence
for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) is_in_the_area_of f
proof
let f be rectangular special_circular_sequence; ::_thesis: for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) is_in_the_area_of f
let g be S-Sequence_in_R2; ::_thesis: ( g /. 1 in LeftComp f & g /. (len g) in RightComp f implies L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) is_in_the_area_of f )
assume that
A1: g /. 1 in LeftComp f and
A2: g /. (len g) in RightComp f ; ::_thesis: L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) is_in_the_area_of f
A3: L~ g meets L~ f by A1, A2, Th33;
1 in dom g by FINSEQ_5:6;
then A4: len g >= 1 by FINSEQ_3:25;
set lp = Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f));
set ilp = Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g);
set h = L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))));
L~ g is_an_arc_of g /. 1,g /. (len g) by TOPREAL1:25;
then A5: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in (L~ g) /\ (L~ f) by A3, JORDAN5C:def_2;
then A6: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in L~ g by XBOOLE_0:def_4;
then A7: 1 <= Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) by JORDAN3:8;
A8: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) by A6, JORDAN3:9;
A9: Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) < len g by A6, JORDAN3:8;
then A10: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 <= len g by NAT_1:13;
given n being Element of NAT such that A11: n in dom (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) and
A12: ( W-bound (L~ f) > ((L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n) `1 or ((L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n) `1 > E-bound (L~ f) or S-bound (L~ f) > ((L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n) `2 or ((L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n) `2 > N-bound (L~ f) ) ; :: according to SPRECT_2:def_1 ::_thesis: contradiction
A13: 1 <= n by A11, FINSEQ_3:25;
then A14: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 = (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + (n -' 1) by NAT_D:38;
LeftComp f = { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) } by Th37;
then A15: (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n in LeftComp f by A12;
A16: 1 <= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 by NAT_1:11;
then A17: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 in dom g by A10, FINSEQ_3:25;
A18: LeftComp f misses RightComp f by SPRECT_1:88;
A19: L~ f misses LeftComp f by Th26;
A20: len g in dom g by FINSEQ_5:6;
A21: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in L~ f by A5, XBOOLE_0:def_4;
now__::_thesis:_not_n_=_1
assume A22: n = 1 ; ::_thesis: contradiction
percases ( Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) or Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) ) ;
suppose Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) ; ::_thesis: contradiction
then L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) = <*(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))*> ^ (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by JORDAN3:def_3;
then (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) by A22, FINSEQ_5:15;
hence contradiction by A19, A21, A15, XBOOLE_0:3; ::_thesis: verum
end;
supposeA23: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) ; ::_thesis: contradiction
then L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) = mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g)) by JORDAN3:def_3;
then (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = g /. ((1 + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1)) -' 1) by A20, A11, A10, A17, A22, SPRECT_2:3
.= g /. ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) by NAT_D:34
.= Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) by A17, A23, PARTFUN1:def_6 ;
hence contradiction by A19, A21, A15, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
then A24: n > 1 by A13, XXREAL_0:1;
then A25: 1 + 1 < (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A7, XREAL_1:8;
then A26: 1 <= ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 by NAT_D:49;
set m = mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g));
A27: len <*(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))*> = 1 by FINSEQ_1:39;
A28: n <= len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) by A11, FINSEQ_3:25;
then A29: n + (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) <= (len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))))) + (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) by XREAL_1:6;
A30: n = (n -' 1) + 1 by A13, XREAL_1:235;
then A31: 1 <= n -' 1 by A24, NAT_1:13;
A32: len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) = ((len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1)) + 1 by A10, A16, JORDAN4:8
.= (len g) -' (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) by A6, JORDAN3:8, NAT_2:7 ;
then A33: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + (len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))))) + 1 = (len g) + 1 by A9, XREAL_1:235;
now__::_thesis:_not_Last_Point_((L~_g),(g_/._1),(g_/._(len_g)),(L~_f))_<>_g_._((Index_((Last_Point_((L~_g),(g_/._1),(g_/._(len_g)),(L~_f))),g))_+_1)
A34: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 <= ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 by A14, A31, XREAL_1:6;
assume A35: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) ; ::_thesis: contradiction
then A36: L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) = <*(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))*> ^ (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by JORDAN3:def_3;
then A37: len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) = 1 + (len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g)))) by A27, FINSEQ_1:22;
then A38: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 <= len g by A33, A29, NAT_D:53;
A39: (len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))))) -' 1 = len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by A37, NAT_D:34;
then n -' 1 <= len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by A28, NAT_D:42;
then A40: n -' 1 in dom (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by A31, FINSEQ_3:25;
(L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) /. (n -' 1) by A28, A30, A27, A31, A36, A39, NAT_D:42, SEQ_4:136;
then A41: (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = g /. (((n -' 1) + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1)) -' 1) by A20, A10, A17, A40, SPRECT_2:3
.= g /. ((n + (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) -' 1) by A30 ;
then A42: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 <> len g by A2, A15, A18, XBOOLE_0:3;
then A43: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 < len g by A38, XXREAL_0:1;
reconsider m = mid (g,(((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1),(len g)) as S-Sequence_in_R2 by A4, A26, A38, A42, JORDAN3:6;
A44: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 in dom g by A26, A38, FINSEQ_3:25;
then A45: m /. (len m) in RightComp f by A2, A20, SPRECT_2:9;
m /. 1 in LeftComp f by A20, A15, A41, A44, SPRECT_2:8;
then L~ f meets L~ m by A45, Th33;
then consider q being set such that
A46: q in L~ f and
A47: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A47;
consider i being Element of NAT such that
A48: 1 <= i and
A49: i + 1 <= len m and
A50: q in LSeg (m,i) by A47, SPPOL_2:13;
A51: len m = ((len g) -' (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) + 1 by A26, A38, JORDAN4:8;
then i <= (len g) -' (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) by A49, XREAL_1:6;
then A52: i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) <= len g by A38, NAT_D:54;
i < len m by A49, NAT_1:13;
then A53: LSeg (m,i) = LSeg (g,((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1)) by A26, A48, A51, A43, JORDAN4:19;
set j = (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1;
i <= i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) by NAT_1:11;
then A54: ((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1) + 1 <= len g by A48, A52, XREAL_1:235, XXREAL_0:2;
(i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 = (i -' 1) + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) by A48, NAT_D:38;
then (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 >= ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 by NAT_1:11;
then A55: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 <= (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 by A34, XXREAL_0:2;
A56: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> g /. ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) by A17, A35, PARTFUN1:def_6;
A57: now__::_thesis:_not_Last_Point_((L~_g),(g_/._1),(g_/._(len_g)),(L~_f))_=_q
assume Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = q ; ::_thesis: contradiction
then A58: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in (LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)))) /\ (LSeg (g,((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1))) by A8, A50, A53, XBOOLE_0:def_4;
then A59: LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) meets LSeg (g,((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1)) by XBOOLE_0:4;
percases ( (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 = (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 or (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 < (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 ) by A55, XXREAL_0:1;
supposeA60: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 = (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 ; ::_thesis: contradiction
then (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + (1 + 1) <= len g by A54;
then (LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)))) /\ (LSeg (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1))) = {(g /. ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1))} by A7, TOPREAL1:def_6;
hence contradiction by A56, A58, A60, TARSKI:def_1; ::_thesis: verum
end;
suppose (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 < (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 ; ::_thesis: contradiction
hence contradiction by A59, TOPREAL1:def_7; ::_thesis: verum
end;
end;
end;
1 <= (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 by A16, A55, XXREAL_0:2;
then Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) >= (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 by A3, A8, A10, A7, A46, A50, A53, A54, A57, JORDAN5C:28;
then Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) >= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 by A55, XXREAL_0:2;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
then A61: L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) = mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g)) by JORDAN3:def_3;
then A62: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + (len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))))) = len g by A9, A32, XREAL_1:235;
then A63: mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g)) = g /^ (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) by A29, FINSEQ_6:117;
A64: 1 <= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A25, XXREAL_0:2;
(((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) + 1 = (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A25, XREAL_1:235, XXREAL_0:2;
then ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 < len g by A29, A62, NAT_1:13;
then A65: (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g))) /. (len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g)))) in RightComp f by A2, A63, JORDAN4:6;
A66: (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = g /. ((n + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1)) -' 1) by A20, A11, A10, A17, A61, SPRECT_2:3
.= g /. (((n + (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) + 1) -' 1)
.= g /. ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) by NAT_D:34 ;
then A67: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n <> len g by A2, A15, A18, XBOOLE_0:3;
then reconsider m = mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g)) as S-Sequence_in_R2 by A4, A29, A62, A64, JORDAN3:6;
(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n in dom g by A29, A62, A64, FINSEQ_3:25;
then m /. 1 in LeftComp f by A20, A15, A66, SPRECT_2:8;
then L~ f meets L~ m by A65, Th33;
then consider q being set such that
A68: q in L~ f and
A69: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A69;
consider i being Element of NAT such that
A70: 1 <= i and
A71: i + 1 <= len m and
A72: q in LSeg (m,i) by A69, SPPOL_2:13;
set j = (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1;
A73: (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 = (i -' 1) + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) by A70, NAT_D:38;
then A74: (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 >= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by NAT_1:11;
len m = ((len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) + 1 by A4, A29, A62, A64, FINSEQ_6:118;
then A75: i < ((len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) + 1 by A71, NAT_1:13;
then i -' 1 < (len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) by A70, NAT_D:54;
then (i -' 1) + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) < len g by NAT_D:53;
then A76: ((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1) + 1 <= len g by A73, NAT_1:13;
(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n < len g by A29, A62, A67, XXREAL_0:1;
then A77: LSeg (m,i) = LSeg (g,((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1)) by A64, A70, A75, JORDAN4:19;
(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 < (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A24, XREAL_1:6;
then A78: (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 > (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 by A74, XXREAL_0:2;
A79: now__::_thesis:_not_Last_Point_((L~_g),(g_/._1),(g_/._(len_g)),(L~_f))_=_q
assume Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = q ; ::_thesis: contradiction
then Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in (LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)))) /\ (LSeg (g,((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1))) by A8, A72, A77, XBOOLE_0:def_4;
then LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) meets LSeg (g,((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1)) by XBOOLE_0:4;
hence contradiction by A78, TOPREAL1:def_7; ::_thesis: verum
end;
1 <= (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 by A64, A74, XXREAL_0:2;
then Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) >= (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 by A3, A8, A10, A7, A68, A72, A77, A79, A76, JORDAN5C:28;
then Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) >= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 by A78, XXREAL_0:2;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
theorem :: SPRECT_3:55
for i, j being Element of NAT
for f being non constant standard special_circular_sequence st 1 <= i & i < len (GoB f) & 1 <= j & j < width (GoB f) holds
Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f))
proof
let i, j be Element of NAT ; ::_thesis: for f being non constant standard special_circular_sequence st 1 <= i & i < len (GoB f) & 1 <= j & j < width (GoB f) holds
Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f))
let f be non constant standard special_circular_sequence; ::_thesis: ( 1 <= i & i < len (GoB f) & 1 <= j & j < width (GoB f) implies Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f)) )
assume that
A1: 1 <= i and
A2: i < len (GoB f) and
A3: 1 <= j and
A4: j < width (GoB f) ; ::_thesis: Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f))
A5: i + 1 <= len (GoB f) by A2, NAT_1:13;
set G = GoB f;
A6: Int (cell ((GoB f),i,j)) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i,1)) `1 < r & r < ((GoB f) * ((i + 1),1)) `1 & ((GoB f) * (1,j)) `2 < s & s < ((GoB f) * (1,(j + 1))) `2 ) } by A1, A2, A3, A4, GOBOARD6:26;
A7: N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f) by SPRECT_1:60;
A8: 1 <= width (GoB f) by GOBRD11:34;
then A9: <*((GoB f) * (i,1))*> is_in_the_area_of f by A1, A2, Th49;
1 <= i + 1 by A1, NAT_1:13;
then A10: <*((GoB f) * ((i + 1),1))*> is_in_the_area_of f by A8, A5, Th49;
assume Int (cell ((GoB f),i,j)) meets L~ (SpStSeq (L~ f)) ; ::_thesis: contradiction
then consider x being set such that
A11: x in Int (cell ((GoB f),i,j)) and
A12: x in L~ (SpStSeq (L~ f)) by XBOOLE_0:3;
A13: W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f) by SPRECT_1:58;
A14: 1 <= len (GoB f) by GOBRD11:34;
then A15: <*((GoB f) * (1,j))*> is_in_the_area_of f by A3, A4, Th49;
A16: j + 1 <= width (GoB f) by A4, NAT_1:13;
1 <= j + 1 by A3, NAT_1:13;
then A17: <*((GoB f) * (1,(j + 1)))*> is_in_the_area_of f by A14, A16, Th49;
A18: L~ (SpStSeq (L~ f)) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = N-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 = E-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) ) } by Th35;
A19: E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) by SPRECT_1:61;
consider p being Point of (TOP-REAL 2) such that
A20: p = x and
A21: ( ( p `1 = W-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = N-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 = E-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) ) by A12, A18;
A22: S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f) by SPRECT_1:59;
consider r, s being Real such that
A23: x = |[r,s]| and
A24: ((GoB f) * (i,1)) `1 < r and
A25: r < ((GoB f) * ((i + 1),1)) `1 and
A26: ((GoB f) * (1,j)) `2 < s and
A27: s < ((GoB f) * (1,(j + 1))) `2 by A6, A11;
A28: p `1 = r by A23, A20, EUCLID:52;
A29: p `2 = s by A23, A20, EUCLID:52;
percases ( p `1 = W-bound (L~ (SpStSeq (L~ f))) or p `2 = N-bound (L~ (SpStSeq (L~ f))) or p `2 = S-bound (L~ (SpStSeq (L~ f))) or p `1 = E-bound (L~ (SpStSeq (L~ f))) ) by A21;
supposeA30: p `1 = W-bound (L~ (SpStSeq (L~ f))) ; ::_thesis: contradiction
A31: 1 in dom <*((GoB f) * (i,1))*> by FINSEQ_5:6;
<*((GoB f) * (i,1))*> /. 1 = (GoB f) * (i,1) by FINSEQ_4:16;
hence contradiction by A24, A9, A28, A13, A30, A31, SPRECT_2:def_1; ::_thesis: verum
end;
supposeA32: p `2 = N-bound (L~ (SpStSeq (L~ f))) ; ::_thesis: contradiction
A33: 1 in dom <*((GoB f) * (1,(j + 1)))*> by FINSEQ_5:6;
<*((GoB f) * (1,(j + 1)))*> /. 1 = (GoB f) * (1,(j + 1)) by FINSEQ_4:16;
hence contradiction by A27, A17, A29, A7, A32, A33, SPRECT_2:def_1; ::_thesis: verum
end;
supposeA34: p `2 = S-bound (L~ (SpStSeq (L~ f))) ; ::_thesis: contradiction
A35: 1 in dom <*((GoB f) * (1,j))*> by FINSEQ_5:6;
<*((GoB f) * (1,j))*> /. 1 = (GoB f) * (1,j) by FINSEQ_4:16;
hence contradiction by A26, A15, A29, A22, A34, A35, SPRECT_2:def_1; ::_thesis: verum
end;
supposeA36: p `1 = E-bound (L~ (SpStSeq (L~ f))) ; ::_thesis: contradiction
A37: 1 in dom <*((GoB f) * ((i + 1),1))*> by FINSEQ_5:6;
<*((GoB f) * ((i + 1),1))*> /. 1 = (GoB f) * ((i + 1),1) by FINSEQ_4:16;
hence contradiction by A25, A10, A28, A19, A36, A37, SPRECT_2:def_1; ::_thesis: verum
end;
end;
end;
theorem :: SPRECT_3:56
for f, g being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g holds
L_Cut (g,p) is_in_the_area_of f
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g holds
L_Cut (g,p) is_in_the_area_of f
let p be Point of (TOP-REAL 2); ::_thesis: ( g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g implies L_Cut (g,p) is_in_the_area_of f )
assume that
A1: g is_in_the_area_of f and
A2: <*p*> is_in_the_area_of f and
A3: g is being_S-Seq ; ::_thesis: ( not p in L~ g or L_Cut (g,p) is_in_the_area_of f )
2 <= len g by A3, TOPREAL1:def_8;
then 1 <= len g by XXREAL_0:2;
then A4: len g in dom g by FINSEQ_3:25;
assume p in L~ g ; ::_thesis: L_Cut (g,p) is_in_the_area_of f
then Index (p,g) < len g by JORDAN3:8;
then A5: (Index (p,g)) + 1 <= len g by NAT_1:13;
1 <= (Index (p,g)) + 1 by NAT_1:11;
then A6: (Index (p,g)) + 1 in dom g by A5, FINSEQ_3:25;
percases ( p <> g . ((Index (p,g)) + 1) or p = g . ((Index (p,g)) + 1) ) ;
suppose p <> g . ((Index (p,g)) + 1) ; ::_thesis: L_Cut (g,p) is_in_the_area_of f
then A7: L_Cut (g,p) = <*p*> ^ (mid (g,((Index (p,g)) + 1),(len g))) by JORDAN3:def_3;
mid (g,((Index (p,g)) + 1),(len g)) is_in_the_area_of f by A1, A4, A6, SPRECT_2:22;
hence L_Cut (g,p) is_in_the_area_of f by A2, A7, SPRECT_2:24; ::_thesis: verum
end;
suppose p = g . ((Index (p,g)) + 1) ; ::_thesis: L_Cut (g,p) is_in_the_area_of f
then L_Cut (g,p) = mid (g,((Index (p,g)) + 1),(len g)) by JORDAN3:def_3;
hence L_Cut (g,p) is_in_the_area_of f by A1, A4, A6, SPRECT_2:22; ::_thesis: verum
end;
end;
end;