:: SPPOL_2 semantic presentation
begin
theorem :: SPPOL_2:1
for r1, r2, r19, r29 being real number st |[r1,r2]| = |[r19,r29]| holds
( r1 = r19 & r2 = r29 ) by FINSEQ_1:77;
theorem Th2: :: SPPOL_2:2
for f being FinSequence of (TOP-REAL 2)
for i, j being Nat st i + j = len f holds
LSeg (f,i) = LSeg ((Rev f),j)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, j being Nat st i + j = len f holds
LSeg (f,i) = LSeg ((Rev f),j)
let i, j be Nat; ::_thesis: ( i + j = len f implies LSeg (f,i) = LSeg ((Rev f),j) )
assume A1: i + j = len f ; ::_thesis: LSeg (f,i) = LSeg ((Rev f),j)
percases ( ( 1 <= i & i + 1 <= len f ) or not 1 <= i or not i + 1 <= len f ) ;
supposethat A2: 1 <= i and
A3: i + 1 <= len f ; ::_thesis: LSeg (f,i) = LSeg ((Rev f),j)
A4: i + (j + 1) = (len f) + 1 by A1;
A5: i in dom f by A2, A3, SEQ_4:134;
then j + 1 in dom (Rev f) by A4, FINSEQ_5:59;
then A6: j + 1 <= len (Rev f) by FINSEQ_3:25;
A7: (i + 1) + j = (len f) + 1 by A1;
A8: i + 1 in dom f by A2, A3, SEQ_4:134;
then j in dom (Rev f) by A7, FINSEQ_5:59;
then A9: 1 <= j by FINSEQ_3:25;
thus LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A2, A3, TOPREAL1:def_3
.= LSeg (((Rev f) /. (j + 1)),(f /. (i + 1))) by A5, A4, FINSEQ_5:66
.= LSeg (((Rev f) /. j),((Rev f) /. (j + 1))) by A8, A7, FINSEQ_5:66
.= LSeg ((Rev f),j) by A6, A9, TOPREAL1:def_3 ; ::_thesis: verum
end;
supposeA10: not 1 <= i ; ::_thesis: LSeg (f,i) = LSeg ((Rev f),j)
then i = 0 by NAT_1:14;
then not j + 1 <= len f by A1, NAT_1:13;
then A11: not j + 1 <= len (Rev f) by FINSEQ_5:def_3;
LSeg (f,i) = {} by A10, TOPREAL1:def_3;
hence LSeg (f,i) = LSeg ((Rev f),j) by A11, TOPREAL1:def_3; ::_thesis: verum
end;
supposeA12: not i + 1 <= len f ; ::_thesis: LSeg (f,i) = LSeg ((Rev f),j)
then A13: LSeg (f,i) = {} by TOPREAL1:def_3;
j < 1 by A1, A12, XREAL_1:6;
hence LSeg (f,i) = LSeg ((Rev f),j) by A13, TOPREAL1:def_3; ::_thesis: verum
end;
end;
end;
theorem Th3: :: SPPOL_2:3
for f being FinSequence of (TOP-REAL 2)
for i, n being Nat st i + 1 <= len (f | n) holds
LSeg ((f | n),i) = LSeg (f,i)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, n being Nat st i + 1 <= len (f | n) holds
LSeg ((f | n),i) = LSeg (f,i)
let i, n be Nat; ::_thesis: ( i + 1 <= len (f | n) implies LSeg ((f | n),i) = LSeg (f,i) )
assume A1: i + 1 <= len (f | n) ; ::_thesis: LSeg ((f | n),i) = LSeg (f,i)
percases ( i <> 0 or i = 0 ) ;
suppose i <> 0 ; ::_thesis: LSeg ((f | n),i) = LSeg (f,i)
then A2: 1 <= i by NAT_1:14;
then A3: i in dom (f | n) by A1, SEQ_4:134;
len (f | n) <= len f by FINSEQ_5:16;
then A4: i + 1 <= len f by A1, XXREAL_0:2;
A5: i + 1 in dom (f | n) by A1, A2, SEQ_4:134;
thus LSeg ((f | n),i) = LSeg (((f | n) /. i),((f | n) /. (i + 1))) by A1, A2, TOPREAL1:def_3
.= LSeg ((f /. i),((f | n) /. (i + 1))) by A3, FINSEQ_4:70
.= LSeg ((f /. i),(f /. (i + 1))) by A5, FINSEQ_4:70
.= LSeg (f,i) by A2, A4, TOPREAL1:def_3 ; ::_thesis: verum
end;
supposeA6: i = 0 ; ::_thesis: LSeg ((f | n),i) = LSeg (f,i)
hence LSeg ((f | n),i) = {} by TOPREAL1:def_3
.= LSeg (f,i) by A6, TOPREAL1:def_3 ;
::_thesis: verum
end;
end;
end;
theorem Th4: :: SPPOL_2:4
for f being FinSequence of (TOP-REAL 2)
for i, n being Nat st n <= len f & 1 <= i holds
LSeg ((f /^ n),i) = LSeg (f,(n + i))
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, n being Nat st n <= len f & 1 <= i holds
LSeg ((f /^ n),i) = LSeg (f,(n + i))
let i, n be Nat; ::_thesis: ( n <= len f & 1 <= i implies LSeg ((f /^ n),i) = LSeg (f,(n + i)) )
assume that
A1: n <= len f and
A2: 1 <= i ; ::_thesis: LSeg ((f /^ n),i) = LSeg (f,(n + i))
percases ( i + 1 <= (len f) - n or i + 1 > (len f) - n ) ;
supposeA3: i + 1 <= (len f) - n ; ::_thesis: LSeg ((f /^ n),i) = LSeg (f,(n + i))
1 <= i + 1 by NAT_1:11;
then 1 <= (len f) - n by A3, XXREAL_0:2;
then A4: 1 + n <= len f by XREAL_1:19;
n <= 1 + n by NAT_1:11;
then n <= len f by A4, XXREAL_0:2;
then A5: len (f /^ n) = (len f) - n by RFINSEQ:def_1;
then A6: i in dom (f /^ n) by A2, A3, SEQ_4:134;
A7: (i + 1) + n <= len f by A3, XREAL_1:19;
i <= i + n by NAT_1:11;
then A8: 1 <= i + n by A2, XXREAL_0:2;
A9: i + 1 in dom (f /^ n) by A2, A3, A5, SEQ_4:134;
thus LSeg ((f /^ n),i) = LSeg (((f /^ n) /. i),((f /^ n) /. (i + 1))) by A2, A3, A5, TOPREAL1:def_3
.= LSeg ((f /. (i + n)),((f /^ n) /. (i + 1))) by A6, FINSEQ_5:27
.= LSeg ((f /. (i + n)),(f /. ((i + 1) + n))) by A9, FINSEQ_5:27
.= LSeg ((f /. (i + n)),(f /. ((i + n) + 1)))
.= LSeg (f,(n + i)) by A8, A7, TOPREAL1:def_3 ; ::_thesis: verum
end;
supposeA10: i + 1 > (len f) - n ; ::_thesis: LSeg ((f /^ n),i) = LSeg (f,(n + i))
then n + (i + 1) > len f by XREAL_1:19;
then A11: (n + i) + 1 > len f ;
i + 1 > len (f /^ n) by A1, A10, RFINSEQ:def_1;
hence LSeg ((f /^ n),i) = {} by TOPREAL1:def_3
.= LSeg (f,(n + i)) by A11, TOPREAL1:def_3 ;
::_thesis: verum
end;
end;
end;
theorem Th5: :: SPPOL_2:5
for f being FinSequence of (TOP-REAL 2)
for i, n being Nat st 1 <= i & i + 1 <= (len f) - n holds
LSeg ((f /^ n),i) = LSeg (f,(n + i))
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, n being Nat st 1 <= i & i + 1 <= (len f) - n holds
LSeg ((f /^ n),i) = LSeg (f,(n + i))
let i, n be Nat; ::_thesis: ( 1 <= i & i + 1 <= (len f) - n implies LSeg ((f /^ n),i) = LSeg (f,(n + i)) )
assume A1: 1 <= i ; ::_thesis: ( not i + 1 <= (len f) - n or LSeg ((f /^ n),i) = LSeg (f,(n + i)) )
A2: n <= (i + 1) + n by NAT_1:11;
assume i + 1 <= (len f) - n ; ::_thesis: LSeg ((f /^ n),i) = LSeg (f,(n + i))
then (i + 1) + n <= len f by XREAL_1:19;
then n <= len f by A2, XXREAL_0:2;
hence LSeg ((f /^ n),i) = LSeg (f,(n + i)) by A1, Th4; ::_thesis: verum
end;
theorem Th6: :: SPPOL_2:6
for f, g being FinSequence of (TOP-REAL 2)
for i being Nat st i + 1 <= len f holds
LSeg ((f ^ g),i) = LSeg (f,i)
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: for i being Nat st i + 1 <= len f holds
LSeg ((f ^ g),i) = LSeg (f,i)
let i be Nat; ::_thesis: ( i + 1 <= len f implies LSeg ((f ^ g),i) = LSeg (f,i) )
assume A1: i + 1 <= len f ; ::_thesis: LSeg ((f ^ g),i) = LSeg (f,i)
percases ( i <> 0 or i = 0 ) ;
suppose i <> 0 ; ::_thesis: LSeg ((f ^ g),i) = LSeg (f,i)
then A2: 1 <= i by NAT_1:14;
then A3: i in dom f by A1, SEQ_4:134;
len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then len (f ^ g) >= len f by NAT_1:11;
then A4: i + 1 <= len (f ^ g) by A1, XXREAL_0:2;
A5: i + 1 in dom f by A1, A2, SEQ_4:134;
thus LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A1, A2, TOPREAL1:def_3
.= LSeg (((f ^ g) /. i),(f /. (i + 1))) by A3, FINSEQ_4:68
.= LSeg (((f ^ g) /. i),((f ^ g) /. (i + 1))) by A5, FINSEQ_4:68
.= LSeg ((f ^ g),i) by A2, A4, TOPREAL1:def_3 ; ::_thesis: verum
end;
supposeA6: i = 0 ; ::_thesis: LSeg ((f ^ g),i) = LSeg (f,i)
hence LSeg ((f ^ g),i) = {} by TOPREAL1:def_3
.= LSeg (f,i) by A6, TOPREAL1:def_3 ;
::_thesis: verum
end;
end;
end;
theorem Th7: :: SPPOL_2:7
for f, g being FinSequence of (TOP-REAL 2)
for i being Nat st 1 <= i holds
LSeg ((f ^ g),((len f) + i)) = LSeg (g,i)
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: for i being Nat st 1 <= i holds
LSeg ((f ^ g),((len f) + i)) = LSeg (g,i)
let i be Nat; ::_thesis: ( 1 <= i implies LSeg ((f ^ g),((len f) + i)) = LSeg (g,i) )
assume A1: 1 <= i ; ::_thesis: LSeg ((f ^ g),((len f) + i)) = LSeg (g,i)
percases ( i + 1 <= len g or i + 1 > len g ) ;
supposeA2: i + 1 <= len g ; ::_thesis: LSeg ((f ^ g),((len f) + i)) = LSeg (g,i)
(len f) + (i + 1) = ((len f) + i) + 1 ;
then ((len f) + i) + 1 <= (len f) + (len g) by A2, XREAL_1:6;
then A3: ((len f) + i) + 1 <= len (f ^ g) by FINSEQ_1:22;
i <= (len f) + i by NAT_1:11;
then A4: 1 <= (len f) + i by A1, XXREAL_0:2;
A5: i + 1 in dom g by A1, A2, SEQ_4:134;
A6: i in dom g by A1, A2, SEQ_4:134;
thus LSeg (g,i) = LSeg ((g /. i),(g /. (i + 1))) by A1, A2, TOPREAL1:def_3
.= LSeg (((f ^ g) /. ((len f) + i)),(g /. (i + 1))) by A6, FINSEQ_4:69
.= LSeg (((f ^ g) /. ((len f) + i)),((f ^ g) /. ((len f) + (i + 1)))) by A5, FINSEQ_4:69
.= LSeg ((f ^ g),((len f) + i)) by A4, A3, TOPREAL1:def_3 ; ::_thesis: verum
end;
supposeA7: i + 1 > len g ; ::_thesis: LSeg ((f ^ g),((len f) + i)) = LSeg (g,i)
then (len f) + (i + 1) > (len f) + (len g) by XREAL_1:6;
then ((len f) + i) + 1 > len (f ^ g) by FINSEQ_1:22;
hence LSeg ((f ^ g),((len f) + i)) = {} by TOPREAL1:def_3
.= LSeg (g,i) by A7, TOPREAL1:def_3 ;
::_thesis: verum
end;
end;
end;
theorem Th8: :: SPPOL_2:8
for f, g being FinSequence of (TOP-REAL 2) st not f is empty & not g is empty holds
LSeg ((f ^ g),(len f)) = LSeg ((f /. (len f)),(g /. 1))
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( not f is empty & not g is empty implies LSeg ((f ^ g),(len f)) = LSeg ((f /. (len f)),(g /. 1)) )
assume that
A1: not f is empty and
A2: not g is empty ; ::_thesis: LSeg ((f ^ g),(len f)) = LSeg ((f /. (len f)),(g /. 1))
A3: 1 in dom g by A2, FINSEQ_5:6;
then 1 <= len g by FINSEQ_3:25;
then (len f) + 1 <= (len f) + (len g) by XREAL_1:6;
then A4: (len f) + 1 <= len (f ^ g) by FINSEQ_1:22;
A5: len f in dom f by A1, FINSEQ_5:6;
then 1 <= len f by FINSEQ_3:25;
hence LSeg ((f ^ g),(len f)) = LSeg (((f ^ g) /. (len f)),((f ^ g) /. ((len f) + 1))) by A4, TOPREAL1:def_3
.= LSeg ((f /. (len f)),((f ^ g) /. ((len f) + 1))) by A5, FINSEQ_4:68
.= LSeg ((f /. (len f)),(g /. 1)) by A3, FINSEQ_4:69 ;
::_thesis: verum
end;
theorem Th9: :: SPPOL_2:9
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for i being Nat st i + 1 <= len (f -: p) holds
LSeg ((f -: p),i) = LSeg (f,i)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2)
for i being Nat st i + 1 <= len (f -: p) holds
LSeg ((f -: p),i) = LSeg (f,i)
let p be Point of (TOP-REAL 2); ::_thesis: for i being Nat st i + 1 <= len (f -: p) holds
LSeg ((f -: p),i) = LSeg (f,i)
let i be Nat; ::_thesis: ( i + 1 <= len (f -: p) implies LSeg ((f -: p),i) = LSeg (f,i) )
f -: p = f | (p .. f) by FINSEQ_5:def_1;
hence ( i + 1 <= len (f -: p) implies LSeg ((f -: p),i) = LSeg (f,i) ) by Th3; ::_thesis: verum
end;
theorem Th10: :: SPPOL_2:10
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for i being Nat st p in rng f holds
LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f)))
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2)
for i being Nat st p in rng f holds
LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f)))
let p be Point of (TOP-REAL 2); ::_thesis: for i being Nat st p in rng f holds
LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f)))
let i be Nat; ::_thesis: ( p in rng f implies LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f))) )
A1: 1 <= i + 1 by NAT_1:11;
assume A2: p in rng f ; ::_thesis: LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f)))
then A3: len (f :- p) = ((len f) - (p .. f)) + 1 by FINSEQ_5:50;
A4: i + (1 + 1) = (i + 1) + 1 ;
percases ( i + 2 <= len (f :- p) or i + 2 > len (f :- p) ) ;
supposeA5: i + 2 <= len (f :- p) ; ::_thesis: LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f)))
then i + 1 <= (len f) - (p .. f) by A4, A3, XREAL_1:6;
then A6: (i + 1) + (p .. f) <= len f by XREAL_1:19;
1 <= p .. f by A2, FINSEQ_4:21;
then i + 1 <= i + (p .. f) by XREAL_1:6;
then A7: 1 <= i + (p .. f) by A1, XXREAL_0:2;
A8: i + 1 in dom (f :- p) by A1, A4, A5, SEQ_4:134;
A9: (i + 1) + 1 in dom (f :- p) by A1, A5, SEQ_4:134;
thus LSeg ((f :- p),(i + 1)) = LSeg (((f :- p) /. (i + 1)),((f :- p) /. ((i + 1) + 1))) by A1, A5, TOPREAL1:def_3
.= LSeg ((f /. (i + (p .. f))),((f :- p) /. ((i + 1) + 1))) by A2, A8, FINSEQ_5:52
.= LSeg ((f /. (i + (p .. f))),(f /. ((i + 1) + (p .. f)))) by A2, A9, FINSEQ_5:52
.= LSeg ((f /. (i + (p .. f))),(f /. ((i + (p .. f)) + 1)))
.= LSeg (f,(i + (p .. f))) by A7, A6, TOPREAL1:def_3 ; ::_thesis: verum
end;
supposeA10: i + 2 > len (f :- p) ; ::_thesis: LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f)))
then i + 1 > (len f) - (p .. f) by A4, A3, XREAL_1:6;
then (p .. f) + (i + 1) > len f by XREAL_1:19;
then (i + (p .. f)) + 1 > len f ;
hence LSeg (f,(i + (p .. f))) = {} by TOPREAL1:def_3
.= LSeg ((f :- p),(i + 1)) by A4, A10, TOPREAL1:def_3 ;
::_thesis: verum
end;
end;
end;
theorem Th11: :: SPPOL_2:11
L~ (<*> the carrier of (TOP-REAL 2)) = {} by TOPREAL1:22;
theorem Th12: :: SPPOL_2:12
for p being Point of (TOP-REAL 2) holds L~ <*p*> = {}
proof
let p be Point of (TOP-REAL 2); ::_thesis: L~ <*p*> = {}
len <*p*> = 1 by FINSEQ_1:39;
hence L~ <*p*> = {} by TOPREAL1:22; ::_thesis: verum
end;
theorem Th13: :: SPPOL_2:13
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & p in LSeg (f,i) )
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds
ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & p in LSeg (f,i) )
let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & p in LSeg (f,i) ) )
set X = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
assume p in L~ f ; ::_thesis: ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & p in LSeg (f,i) )
then consider Y being set such that
A1: p in Y and
A2: Y in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by TARSKI:def_4;
ex i being Element of NAT st
( Y = LSeg (f,i) & 1 <= i & i + 1 <= len f ) by A2;
hence ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & p in LSeg (f,i) ) by A1; ::_thesis: verum
end;
theorem Th14: :: SPPOL_2:14
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 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
ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) )
let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) ) )
assume p in L~ f ; ::_thesis: ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) )
then consider i being Element of NAT such that
A1: 1 <= i and
A2: i + 1 <= len f and
A3: p in LSeg (f,i) by Th13;
take i ; ::_thesis: ( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) )
thus ( 1 <= i & i + 1 <= len f ) by A1, A2; ::_thesis: p in LSeg ((f /. i),(f /. (i + 1)))
thus p in LSeg ((f /. i),(f /. (i + 1))) by A1, A2, A3, TOPREAL1:def_3; ::_thesis: verum
end;
theorem Th15: :: SPPOL_2:15
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for i being Element of NAT st 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) holds
p in L~ f
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2)
for i being Element of NAT st 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) holds
p in L~ f
let p be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) holds
p in L~ f
let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) implies p in L~ f )
assume that
A1: 1 <= i and
A2: i + 1 <= len f and
A3: p in LSeg ((f /. i),(f /. (i + 1))) ; ::_thesis: p in L~ f
set X = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ;
A4: LSeg (f,i) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A1, A2;
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A1, A2, TOPREAL1:def_3;
hence p in L~ f by A3, A4, TARSKI:def_4; ::_thesis: verum
end;
theorem :: SPPOL_2:16
for f being FinSequence of (TOP-REAL 2)
for i being Element of NAT st 1 <= i & i + 1 <= len f holds
LSeg ((f /. i),(f /. (i + 1))) c= L~ f
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st 1 <= i & i + 1 <= len f holds
LSeg ((f /. i),(f /. (i + 1))) c= L~ f
let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len f implies LSeg ((f /. i),(f /. (i + 1))) c= L~ f )
assume that
A1: 1 <= i and
A2: i + 1 <= len f ; ::_thesis: LSeg ((f /. i),(f /. (i + 1))) c= L~ f
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A1, A2, TOPREAL1:def_3;
hence LSeg ((f /. i),(f /. (i + 1))) c= L~ f by TOPREAL3:19; ::_thesis: verum
end;
theorem :: SPPOL_2:17
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for i being Element of NAT st p in LSeg (f,i) holds
p in L~ f
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2)
for i being Element of NAT st p in LSeg (f,i) holds
p in L~ f
let p be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st p in LSeg (f,i) holds
p in L~ f
let i be Element of NAT ; ::_thesis: ( p in LSeg (f,i) implies p in L~ f )
LSeg (f,i) c= L~ f by TOPREAL3:19;
hence ( p in LSeg (f,i) implies p in L~ f ) ; ::_thesis: verum
end;
theorem Th18: :: SPPOL_2:18
for f being FinSequence of (TOP-REAL 2) st len f >= 2 holds
rng f c= L~ f
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( len f >= 2 implies rng f c= L~ f )
assume A1: len f >= 2 ; ::_thesis: rng f c= L~ f
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in L~ f )
assume x in rng f ; ::_thesis: x in L~ f
then consider i being Element of NAT such that
A2: i in dom f and
A3: f /. i = x by PARTFUN2:2;
A4: 1 <= i by A2, FINSEQ_3:25;
A5: i <= len f by A2, FINSEQ_3:25;
A6: f /. i in LSeg ((f /. i),(f /. (i + 1))) by RLTOPSP1:68;
percases ( i = len f or i <> len f ) ;
supposeA7: i = len f ; ::_thesis: x in L~ f
then consider j being Nat such that
A8: j + 1 = i by A1, NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
1 + 1 <= j + 1 by A1, A7, A8;
then A9: 1 <= j by XREAL_1:6;
f /. (j + 1) in LSeg ((f /. j),(f /. (j + 1))) by RLTOPSP1:68;
hence x in L~ f by A3, A7, A8, A9, Th15; ::_thesis: verum
end;
suppose i <> len f ; ::_thesis: x in L~ f
then i < len f by A5, XXREAL_0:1;
then i + 1 <= len f by NAT_1:13;
hence x in L~ f by A3, A4, A6, Th15; ::_thesis: verum
end;
end;
end;
theorem Th19: :: SPPOL_2:19
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st not f is empty holds
L~ (f ^ <*p*>) = (L~ f) \/ (LSeg ((f /. (len f)),p))
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st not f is empty holds
L~ (f ^ <*p*>) = (L~ f) \/ (LSeg ((f /. (len f)),p))
let p be Point of (TOP-REAL 2); ::_thesis: ( not f is empty implies L~ (f ^ <*p*>) = (L~ f) \/ (LSeg ((f /. (len f)),p)) )
set fp = f ^ <*p*>;
A1: (len f) + 1 <= len (f ^ <*p*>) by FINSEQ_2:16;
1 <= (len f) + 1 by NAT_1:11;
then A2: (len f) + 1 in dom (f ^ <*p*>) by A1, FINSEQ_3:25;
A3: (f ^ <*p*>) /. ((len f) + 1) = p by FINSEQ_4:67;
len (f ^ <*p*>) = (len f) + 1 by FINSEQ_2:16;
then A4: (f ^ <*p*>) | ((len f) + 1) = f ^ <*p*> by FINSEQ_1:58;
A5: dom f c= dom (f ^ <*p*>) by FINSEQ_1:26;
A6: (f ^ <*p*>) | (len f) = f by FINSEQ_5:23;
assume not f is empty ; ::_thesis: L~ (f ^ <*p*>) = (L~ f) \/ (LSeg ((f /. (len f)),p))
then A7: len f in dom f by FINSEQ_5:6;
then (f ^ <*p*>) /. (len f) = f /. (len f) by FINSEQ_4:68;
hence L~ (f ^ <*p*>) = (L~ f) \/ (LSeg ((f /. (len f)),p)) by A2, A7, A3, A4, A5, A6, TOPREAL3:38; ::_thesis: verum
end;
theorem Th20: :: SPPOL_2:20
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st not f is empty holds
L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st not f is empty holds
L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f)
let p be Point of (TOP-REAL 2); ::_thesis: ( not f is empty implies L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f) )
set q = f /. 1;
A1: len <*p*> = 1 by FINSEQ_1:39;
then A2: len (<*p*> ^ f) = 1 + (len f) by FINSEQ_1:22;
assume A3: not f is empty ; ::_thesis: L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f)
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (LSeg (p,(f /. 1))) \/ (L~ f) c= L~ (<*p*> ^ f)
let x be set ; ::_thesis: ( x in L~ (<*p*> ^ f) implies x in (LSeg (p,(f /. 1))) \/ (L~ f) )
assume A4: x in L~ (<*p*> ^ f) ; ::_thesis: x in (LSeg (p,(f /. 1))) \/ (L~ f)
then reconsider r = x as Point of (TOP-REAL 2) ;
consider i being Element of NAT such that
A5: 1 <= i and
A6: i + 1 <= len (<*p*> ^ f) and
A7: r in LSeg (((<*p*> ^ f) /. i),((<*p*> ^ f) /. (i + 1))) by A4, Th14;
now__::_thesis:_(_(_i_=_1_&_r_in_LSeg_(p,(f_/._1))_)_or_(_i_>_1_&_r_in_L~_f_)_)
percases ( i = 1 or i > 1 ) by A5, XXREAL_0:1;
caseA8: i = 1 ; ::_thesis: r in LSeg (p,(f /. 1))
then A9: p = (<*p*> ^ f) /. i by FINSEQ_5:15;
i in dom f by A3, A8, FINSEQ_5:6;
hence r in LSeg (p,(f /. 1)) by A1, A7, A8, A9, FINSEQ_4:69; ::_thesis: verum
end;
caseA10: i > 1 ; ::_thesis: r in L~ f
then consider j being Nat such that
A11: i = j + 1 by NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A12: 1 <= j by A10, A11, NAT_1:13;
A13: j + 1 <= len f by A2, A6, A11, XREAL_1:6;
then j + 1 in dom f by A12, SEQ_4:134;
then A14: (<*p*> ^ f) /. (i + 1) = f /. (j + 1) by A1, A11, FINSEQ_4:69;
j in dom f by A12, A13, SEQ_4:134;
then (<*p*> ^ f) /. i = f /. j by A1, A11, FINSEQ_4:69;
hence r in L~ f by A7, A12, A13, A14, Th15; ::_thesis: verum
end;
end;
end;
hence x in (LSeg (p,(f /. 1))) \/ (L~ f) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LSeg (p,(f /. 1))) \/ (L~ f) or x in L~ (<*p*> ^ f) )
assume A15: x in (LSeg (p,(f /. 1))) \/ (L~ f) ; ::_thesis: x in L~ (<*p*> ^ f)
then reconsider r = x as Point of (TOP-REAL 2) ;
percases ( r in LSeg (p,(f /. 1)) or r in L~ f ) by A15, XBOOLE_0:def_3;
supposeA16: r in LSeg (p,(f /. 1)) ; ::_thesis: x in L~ (<*p*> ^ f)
set i = 1;
1 <= len f by A3, NAT_1:14;
then A17: 1 + 1 <= len (<*p*> ^ f) by A2, XREAL_1:6;
1 in dom f by A3, FINSEQ_5:6;
then A18: f /. 1 = (<*p*> ^ f) /. (1 + 1) by A1, FINSEQ_4:69;
p = (<*p*> ^ f) /. 1 by FINSEQ_5:15;
hence x in L~ (<*p*> ^ f) by A16, A17, A18, Th15; ::_thesis: verum
end;
suppose r in L~ f ; ::_thesis: x in L~ (<*p*> ^ f)
then consider j being Element of NAT such that
A19: 1 <= j and
A20: j + 1 <= len f and
A21: r in LSeg ((f /. j),(f /. (j + 1))) by Th14;
set i = j + 1;
j in dom f by A19, A20, SEQ_4:134;
then A22: (<*p*> ^ f) /. (j + 1) = f /. j by A1, FINSEQ_4:69;
j + 1 in dom f by A19, A20, SEQ_4:134;
then A23: (<*p*> ^ f) /. ((j + 1) + 1) = f /. (j + 1) by A1, FINSEQ_4:69;
(j + 1) + 1 <= len (<*p*> ^ f) by A2, A20, XREAL_1:6;
hence x in L~ (<*p*> ^ f) by A21, A22, A23, Th15, NAT_1:12; ::_thesis: verum
end;
end;
end;
theorem Th21: :: SPPOL_2:21
for p, q being Point of (TOP-REAL 2) holds L~ <*p,q*> = LSeg (p,q)
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: L~ <*p,q*> = LSeg (p,q)
set f = <*p*>;
A1: len <*p*> = 1 by FINSEQ_1:39;
thus L~ <*p,q*> = L~ (<*p*> ^ <*q*>) by FINSEQ_1:def_9
.= (L~ <*p*>) \/ (LSeg ((<*p*> /. (len <*p*>)),q)) by Th19
.= (L~ <*p*>) \/ (LSeg (p,q)) by A1, FINSEQ_4:16
.= {} \/ (LSeg (p,q)) by A1, TOPREAL1:22
.= LSeg (p,q) ; ::_thesis: verum
end;
theorem Th22: :: SPPOL_2:22
for f being FinSequence of (TOP-REAL 2) holds L~ f = L~ (Rev f)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: L~ f = L~ (Rev f)
defpred S1[ FinSequence of (TOP-REAL 2)] means L~ $1 = L~ (Rev $1);
A1: for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st S1[f] holds
S1[f ^ <*p*>]
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st S1[f] holds
S1[f ^ <*p*>]
let p be Point of (TOP-REAL 2); ::_thesis: ( S1[f] implies S1[f ^ <*p*>] )
assume A2: S1[f] ; ::_thesis: S1[f ^ <*p*>]
percases ( f is empty or not f is empty ) ;
supposeA3: f is empty ; ::_thesis: S1[f ^ <*p*>]
hence L~ (f ^ <*p*>) = L~ <*p*> by FINSEQ_1:34
.= L~ (Rev <*p*>) by FINSEQ_5:60
.= L~ (Rev (f ^ <*p*>)) by A3, FINSEQ_1:34 ;
::_thesis: verum
end;
supposeA4: not f is empty ; ::_thesis: S1[f ^ <*p*>]
set q9 = (Rev f) /. 1;
set q = f /. (len f);
len f = len (Rev f) by FINSEQ_5:def_3;
then A5: not Rev f is empty by A4;
f /. (len f) = (Rev f) /. 1 by A4, FINSEQ_5:65;
hence L~ (f ^ <*p*>) = (LSeg (p,((Rev f) /. 1))) \/ (L~ (Rev f)) by A2, A4, Th19
.= L~ (<*p*> ^ (Rev f)) by A5, Th20
.= L~ (Rev (f ^ <*p*>)) by FINSEQ_5:63 ;
::_thesis: verum
end;
end;
end;
A6: S1[ <*> the carrier of (TOP-REAL 2)] ;
for f being FinSequence of (TOP-REAL 2) holds S1[f] from FINSEQ_2:sch_2(A6, A1);
hence L~ f = L~ (Rev f) ; ::_thesis: verum
end;
theorem Th23: :: SPPOL_2:23
for f1, f2 being FinSequence of (TOP-REAL 2) st not f1 is empty & not f2 is empty holds
L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2)
proof
let f1, f2 be FinSequence of (TOP-REAL 2); ::_thesis: ( not f1 is empty & not f2 is empty implies L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2) )
set p = f1 /. (len f1);
set q = f2 /. 1;
defpred S1[ FinSequence of (TOP-REAL 2)] means L~ ((f1 ^ <*(f2 /. 1)*>) ^ $1) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ $1));
assume A1: not f1 is empty ; ::_thesis: ( f2 is empty or L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2) )
A2: for f being FinSequence of (TOP-REAL 2)
for o being Point of (TOP-REAL 2) st S1[f] holds
S1[f ^ <*o*>]
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for o being Point of (TOP-REAL 2) st S1[f] holds
S1[f ^ <*o*>]
let o be Point of (TOP-REAL 2); ::_thesis: ( S1[f] implies S1[f ^ <*o*>] )
assume A3: S1[f] ; ::_thesis: S1[f ^ <*o*>]
percases ( f is empty or not f is empty ) ;
suppose f is empty ; ::_thesis: S1[f ^ <*o*>]
then A4: f ^ <*o*> = <*o*> by FINSEQ_1:34;
len (f1 ^ <*(f2 /. 1)*>) = (len f1) + 1 by FINSEQ_2:16;
then (f1 ^ <*(f2 /. 1)*>) /. (len (f1 ^ <*(f2 /. 1)*>)) = f2 /. 1 by FINSEQ_4:67;
hence L~ ((f1 ^ <*(f2 /. 1)*>) ^ (f ^ <*o*>)) = (L~ (f1 ^ <*(f2 /. 1)*>)) \/ (LSeg ((f2 /. 1),o)) by A4, Th19
.= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (LSeg ((f2 /. 1),o)) by A1, Th19
.= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ <*(f2 /. 1),o*>) by Th21
.= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ (f ^ <*o*>))) by A4, FINSEQ_1:def_9 ;
::_thesis: verum
end;
supposeA5: not f is empty ; ::_thesis: S1[f ^ <*o*>]
set g = (f1 ^ <*(f2 /. 1)*>) ^ f;
set h = <*(f2 /. 1)*> ^ f;
len f <> 0 by A5;
then consider f9 being FinSequence of (TOP-REAL 2), d being Point of (TOP-REAL 2) such that
A6: f = f9 ^ <*d*> by FINSEQ_2:19;
A7: <*(f2 /. 1)*> ^ f = (<*(f2 /. 1)*> ^ f9) ^ <*d*> by A6, FINSEQ_1:32;
then len (<*(f2 /. 1)*> ^ f) = (len (<*(f2 /. 1)*> ^ f9)) + 1 by FINSEQ_2:16;
then A8: (<*(f2 /. 1)*> ^ f) /. (len (<*(f2 /. 1)*> ^ f)) = d by A7, FINSEQ_4:67;
A9: (f1 ^ <*(f2 /. 1)*>) ^ f = ((f1 ^ <*(f2 /. 1)*>) ^ f9) ^ <*d*> by A6, FINSEQ_1:32;
then len ((f1 ^ <*(f2 /. 1)*>) ^ f) = (len ((f1 ^ <*(f2 /. 1)*>) ^ f9)) + 1 by FINSEQ_2:16;
then ((f1 ^ <*(f2 /. 1)*>) ^ f) /. (len ((f1 ^ <*(f2 /. 1)*>) ^ f)) = d by A9, FINSEQ_4:67;
then A10: (L~ (<*(f2 /. 1)*> ^ f)) \/ (LSeg ((((f1 ^ <*(f2 /. 1)*>) ^ f) /. (len ((f1 ^ <*(f2 /. 1)*>) ^ f))),o)) = L~ ((<*(f2 /. 1)*> ^ f) ^ <*o*>) by A8, Th19
.= L~ (<*(f2 /. 1)*> ^ (f ^ <*o*>)) by FINSEQ_1:32 ;
thus L~ ((f1 ^ <*(f2 /. 1)*>) ^ (f ^ <*o*>)) = L~ (((f1 ^ <*(f2 /. 1)*>) ^ f) ^ <*o*>) by FINSEQ_1:32
.= (L~ ((f1 ^ <*(f2 /. 1)*>) ^ f)) \/ (LSeg ((((f1 ^ <*(f2 /. 1)*>) ^ f) /. (len ((f1 ^ <*(f2 /. 1)*>) ^ f))),o)) by Th19
.= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ (f ^ <*o*>))) by A3, A10, XBOOLE_1:4 ; ::_thesis: verum
end;
end;
end;
assume not f2 is empty ; ::_thesis: L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2)
then A11: f2 = <*(f2 /. 1)*> ^ (f2 /^ 1) by FINSEQ_5:29;
A12: S1[ <*> the carrier of (TOP-REAL 2)]
proof
set O = <*> the carrier of (TOP-REAL 2);
thus L~ ((f1 ^ <*(f2 /. 1)*>) ^ (<*> the carrier of (TOP-REAL 2))) = L~ (f1 ^ <*(f2 /. 1)*>) by FINSEQ_1:34
.= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ {} by A1, Th19
.= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ <*(f2 /. 1)*>) by Th12
.= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ (<*> the carrier of (TOP-REAL 2)))) by FINSEQ_1:34 ; ::_thesis: verum
end;
for f being FinSequence of (TOP-REAL 2) holds S1[f] from FINSEQ_2:sch_2(A12, A2);
then L~ ((f1 ^ <*(f2 /. 1)*>) ^ (f2 /^ 1)) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ (f2 /^ 1))) ;
hence L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2) by A11, FINSEQ_1:32; ::_thesis: verum
end;
Lm1: for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT holds L~ (f | n) c= L~ f
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds L~ (f | n) c= L~ f
let n be Element of NAT ; ::_thesis: L~ (f | n) c= L~ f
now__::_thesis:_L~_(f_|_n)_c=_L~_f
percases ( n = 0 or n <> 0 ) ;
supposeA1: n = 0 ; ::_thesis: L~ (f | n) c= L~ f
f | 0 is empty ;
hence L~ (f | n) c= L~ f by A1, Th11, XBOOLE_1:2; ::_thesis: verum
end;
supposeA2: n <> 0 ; ::_thesis: L~ (f | n) c= L~ f
now__::_thesis:_L~_(f_|_n)_c=_L~_f
percases ( n < len f or n >= len f ) ;
supposeA3: n < len f ; ::_thesis: L~ (f | n) c= L~ f
then len (f /^ n) = (len f) - n by RFINSEQ:def_1;
then len (f /^ n) <> 0 by A3;
then A4: not f /^ n is empty ;
len (f | n) = n by A3, FINSEQ_1:59;
then A5: not f | n is empty by A2;
(f | n) ^ (f /^ n) = f by RFINSEQ:8;
then L~ f = ((L~ (f | n)) \/ (LSeg (((f | n) /. (len (f | n))),((f /^ n) /. 1)))) \/ (L~ (f /^ n)) by A5, A4, Th23
.= (L~ (f | n)) \/ ((LSeg (((f | n) /. (len (f | n))),((f /^ n) /. 1))) \/ (L~ (f /^ n))) by XBOOLE_1:4 ;
hence L~ (f | n) c= L~ f by XBOOLE_1:7; ::_thesis: verum
end;
suppose n >= len f ; ::_thesis: L~ (f | n) c= L~ f
hence L~ (f | n) c= L~ f by FINSEQ_1:58; ::_thesis: verum
end;
end;
end;
hence L~ (f | n) c= L~ f ; ::_thesis: verum
end;
end;
end;
hence L~ (f | n) c= L~ f ; ::_thesis: verum
end;
theorem Th24: :: SPPOL_2:24
for f being FinSequence of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st q in rng f holds
L~ f = (L~ (f -: q)) \/ (L~ (f :- q))
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) st q in rng f holds
L~ f = (L~ (f -: q)) \/ (L~ (f :- q))
let q be Point of (TOP-REAL 2); ::_thesis: ( q in rng f implies L~ f = (L~ (f -: q)) \/ (L~ (f :- q)) )
set n = q .. f;
assume A1: q in rng f ; ::_thesis: L~ f = (L~ (f -: q)) \/ (L~ (f :- q))
then A2: q .. f <= len f by FINSEQ_4:21;
percases ( q .. f < len f or q .. f = len f ) by A2, XXREAL_0:1;
supposeA3: q .. f < len f ; ::_thesis: L~ f = (L~ (f -: q)) \/ (L~ (f :- q))
then len (f /^ (q .. f)) = (len f) - (q .. f) by RFINSEQ:def_1;
then len (f /^ (q .. f)) <> 0 by A3;
then A4: not f /^ (q .. f) is empty ;
A5: len (f | (q .. f)) = q .. f by A3, FINSEQ_1:59;
f | (q .. f) = f -: q by FINSEQ_5:def_1;
then A6: (f | (q .. f)) /. (len (f | (q .. f))) = q by A1, A5, FINSEQ_5:45;
A7: (f | (q .. f)) ^ (f /^ (q .. f)) = f by RFINSEQ:8;
not f | (q .. f) is empty by A1, A5, FINSEQ_4:21;
hence L~ f = ((L~ (f | (q .. f))) \/ (LSeg (((f | (q .. f)) /. (len (f | (q .. f)))),((f /^ (q .. f)) /. 1)))) \/ (L~ (f /^ (q .. f))) by A4, A7, Th23
.= (L~ (f | (q .. f))) \/ ((LSeg (((f | (q .. f)) /. (len (f | (q .. f)))),((f /^ (q .. f)) /. 1))) \/ (L~ (f /^ (q .. f)))) by XBOOLE_1:4
.= (L~ (f | (q .. f))) \/ (L~ (<*((f | (q .. f)) /. (len (f | (q .. f))))*> ^ (f /^ (q .. f)))) by A4, Th20
.= (L~ (f | (q .. f))) \/ (L~ (f :- q)) by A6, FINSEQ_5:def_2
.= (L~ (f -: q)) \/ (L~ (f :- q)) by FINSEQ_5:def_1 ;
::_thesis: verum
end;
supposeA8: q .. f = len f ; ::_thesis: L~ f = (L~ (f -: q)) \/ (L~ (f :- q))
then len (f /^ (q .. f)) = (len f) - (q .. f) by RFINSEQ:def_1
.= 0 by A8 ;
then A9: f /^ (q .. f) is empty ;
f :- q = <*q*> ^ (f /^ (q .. f)) by FINSEQ_5:def_2
.= <*q*> by A9, FINSEQ_1:34 ;
then A10: L~ (f :- q) is empty by Th12;
L~ f = L~ (f | (q .. f)) by A8, FINSEQ_1:58
.= L~ (f -: q) by FINSEQ_5:def_1 ;
hence L~ f = (L~ (f -: q)) \/ (L~ (f :- q)) by A10; ::_thesis: verum
end;
end;
end;
theorem Th25: :: SPPOL_2:25
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for n being Element of NAT st p in LSeg (f,n) holds
L~ f = L~ (Ins (f,n,p))
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2)
for n being Element of NAT st p in LSeg (f,n) holds
L~ f = L~ (Ins (f,n,p))
let p be Point of (TOP-REAL 2); ::_thesis: for n being Element of NAT st p in LSeg (f,n) holds
L~ f = L~ (Ins (f,n,p))
let n be Element of NAT ; ::_thesis: ( p in LSeg (f,n) implies L~ f = L~ (Ins (f,n,p)) )
set f1 = f | n;
set g1 = (f | n) ^ <*p*>;
set f2 = f /^ n;
A1: ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = ((f | n) ^ <*p*>) /. ((len (f | n)) + 1) by FINSEQ_2:16
.= p by FINSEQ_4:67 ;
assume A2: p in LSeg (f,n) ; ::_thesis: L~ f = L~ (Ins (f,n,p))
then A3: n + 1 <= len f by TOPREAL1:def_3;
then A4: 1 <= (len f) - n by XREAL_1:19;
A5: n <= n + 1 by NAT_1:11;
then A6: len (f | n) = n by A3, FINSEQ_1:59, XXREAL_0:2;
then A7: not f | n is empty by A2, TOPREAL1:def_3;
A8: 1 <= n by A2, TOPREAL1:def_3;
then A9: n in dom (f | n) by A6, FINSEQ_3:25;
n <= len f by A3, A5, XXREAL_0:2;
then 1 <= len (f /^ n) by A4, RFINSEQ:def_1;
then A10: 1 in dom (f /^ n) by FINSEQ_3:25;
A11: LSeg (f,n) = LSeg ((f /. n),(f /. (n + 1))) by A8, A3, TOPREAL1:def_3
.= LSeg (((f | n) /. (len (f | n))),(f /. (n + 1))) by A6, A9, FINSEQ_4:70
.= LSeg (((f | n) /. (len (f | n))),((f /^ n) /. 1)) by A10, FINSEQ_5:27 ;
thus L~ (Ins (f,n,p)) = L~ (((f | n) ^ <*p*>) ^ (f /^ n)) by FINSEQ_5:def_4
.= ((L~ ((f | n) ^ <*p*>)) \/ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)))) \/ (L~ (f /^ n)) by A10, Th23, RELAT_1:38
.= (((L~ (f | n)) \/ (LSeg (((f | n) /. (len (f | n))),p))) \/ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)))) \/ (L~ (f /^ n)) by A9, Th19, RELAT_1:38
.= ((L~ (f | n)) \/ ((LSeg (((f | n) /. (len (f | n))),p)) \/ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))))) \/ (L~ (f /^ n)) by XBOOLE_1:4
.= ((L~ (f | n)) \/ (LSeg (((f | n) /. (len (f | n))),((f /^ n) /. 1)))) \/ (L~ (f /^ n)) by A2, A1, A11, TOPREAL1:5
.= L~ ((f | n) ^ (f /^ n)) by A7, A10, Th23, RELAT_1:38
.= L~ f by RFINSEQ:8 ; ::_thesis: verum
end;
begin
registration
clusterV15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like being_S-Seq for FinSequence of the carrier of (TOP-REAL 2);
existence
ex b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq
proof
set p = |[0,0]|;
set q = |[1,1]|;
A1: |[0,0]| `2 = 0 by EUCLID:52;
A2: |[1,1]| `1 = 1 by EUCLID:52;
A3: |[1,1]| `2 = 1 by EUCLID:52;
|[0,0]| `1 = 0 by EUCLID:52;
then <*|[0,0]|,|[(|[0,0]| `1),(|[1,1]| `2)]|,|[1,1]|*> is being_S-Seq by A1, A2, A3, TOPREAL3:34;
hence ex b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq ; ::_thesis: verum
end;
cluster being_S-Seq -> non trivial one-to-one special unfolded s.n.c. for FinSequence of the carrier of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq holds
( b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special & not b1 is trivial )
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq implies ( f is one-to-one & f is unfolded & f is s.n.c. & f is special & not f is trivial ) )
assume A4: f is being_S-Seq ; ::_thesis: ( f is one-to-one & f is unfolded & f is s.n.c. & f is special & not f is trivial )
then len f >= 2 by TOPREAL1:def_8;
hence ( f is one-to-one & f is unfolded & f is s.n.c. & f is special & not f is trivial ) by A4, NAT_D:60, TOPREAL1:def_8; ::_thesis: verum
end;
cluster non trivial one-to-one special unfolded s.n.c. -> being_S-Seq for FinSequence of the carrier of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special & not b1 is trivial holds
b1 is being_S-Seq
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is one-to-one & f is unfolded & f is s.n.c. & f is special & not f is trivial implies f is being_S-Seq )
assume A5: ( f is one-to-one & f is unfolded & f is s.n.c. & f is special ) ; ::_thesis: ( f is trivial or f is being_S-Seq )
assume not f is trivial ; ::_thesis: f is being_S-Seq
then len f >= 2 by NAT_D:60;
hence f is being_S-Seq by A5, TOPREAL1:def_8; ::_thesis: verum
end;
cluster being_S-Seq -> non empty for FinSequence of the carrier of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq holds
not b1 is empty by CARD_1:27, TOPREAL1:def_8;
end;
registration
cluster non trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like one-to-one V32() FinSequence-like FinSubsequence-like special unfolded s.n.c. for FinSequence of the carrier of (TOP-REAL 2);
existence
ex b1 being FinSequence of (TOP-REAL 2) st
( b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special & not b1 is trivial )
proof
set f = the being_S-Seq FinSequence of (TOP-REAL 2);
( the being_S-Seq FinSequence of (TOP-REAL 2) is one-to-one & the being_S-Seq FinSequence of (TOP-REAL 2) is unfolded & the being_S-Seq FinSequence of (TOP-REAL 2) is s.n.c. & the being_S-Seq FinSequence of (TOP-REAL 2) is special & not the being_S-Seq FinSequence of (TOP-REAL 2) is trivial ) ;
hence ex b1 being FinSequence of (TOP-REAL 2) st
( b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special & not b1 is trivial ) ; ::_thesis: verum
end;
end;
theorem Th26: :: SPPOL_2:26
for f being FinSequence of (TOP-REAL 2) st len f <= 2 holds
f is unfolded
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( len f <= 2 implies f is unfolded )
assume A1: len f <= 2 ; ::_thesis: f is unfolded
let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len f or (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} )
assume A2: 1 <= i ; ::_thesis: ( not i + 2 <= len f or (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} )
assume i + 2 <= len f ; ::_thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}
then i + 2 <= 2 by A1, XXREAL_0:2;
then i <= 2 - 2 by XREAL_1:19;
hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A2, XXREAL_0:2; ::_thesis: verum
end;
Lm2: for p, q being Point of (TOP-REAL 2) holds <*p,q*> is unfolded
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: <*p,q*> is unfolded
len <*p,q*> = 2 by FINSEQ_1:44;
hence <*p,q*> is unfolded by Th26; ::_thesis: verum
end;
Lm3: for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT st f is unfolded holds
f | n is unfolded
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is unfolded holds
f | n is unfolded
let n be Element of NAT ; ::_thesis: ( f is unfolded implies f | n is unfolded )
assume A1: f is unfolded ; ::_thesis: f | n is unfolded
set h = f | n;
let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len (f | n) or (LSeg ((f | n),i)) /\ (LSeg ((f | n),(i + 1))) = {((f | n) /. (i + 1))} )
assume that
A2: 1 <= i and
A3: i + 2 <= len (f | n) ; ::_thesis: (LSeg ((f | n),i)) /\ (LSeg ((f | n),(i + 1))) = {((f | n) /. (i + 1))}
A4: i + 1 in dom (f | n) by A2, A3, SEQ_4:135;
len (f | n) <= len f by FINSEQ_5:16;
then A5: i + 2 <= len f by A3, XXREAL_0:2;
A6: (i + 1) + 1 = i + (1 + 1) ;
i + 1 <= i + 2 by XREAL_1:6;
hence (LSeg ((f | n),i)) /\ (LSeg ((f | n),(i + 1))) = (LSeg (f,i)) /\ (LSeg ((f | n),(i + 1))) by A3, Th3, XXREAL_0:2
.= (LSeg (f,i)) /\ (LSeg (f,(i + 1))) by A3, A6, Th3
.= {(f /. (i + 1))} by A1, A2, A5, TOPREAL1:def_6
.= {((f | n) /. (i + 1))} by A4, FINSEQ_4:70 ;
::_thesis: verum
end;
Lm4: for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT st f is unfolded holds
f /^ n is unfolded
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is unfolded holds
f /^ n is unfolded
let n be Element of NAT ; ::_thesis: ( f is unfolded implies f /^ n is unfolded )
assume A1: f is unfolded ; ::_thesis: f /^ n is unfolded
percases ( n <= len f or n > len f ) ;
supposeA2: n <= len f ; ::_thesis: f /^ n is unfolded
set h = f /^ n;
let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len (f /^ n) or (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),(i + 1))) = {((f /^ n) /. (i + 1))} )
assume that
A3: 1 <= i and
A4: i + 2 <= len (f /^ n) ; ::_thesis: (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),(i + 1))) = {((f /^ n) /. (i + 1))}
A5: i + 1 in dom (f /^ n) by A3, A4, SEQ_4:135;
A6: len (f /^ n) = (len f) - n by A2, RFINSEQ:def_1;
then n + (i + 2) <= len f by A4, XREAL_1:19;
then A7: (n + i) + 2 <= len f ;
i <= n + i by NAT_1:11;
then A8: 1 <= n + i by A3, XXREAL_0:2;
A9: (i + 1) + 1 = i + (1 + 1) ;
i + 1 <= i + 2 by XREAL_1:6;
then i + 1 <= len (f /^ n) by A4, XXREAL_0:2;
hence (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),(i + 1))) = (LSeg (f,(n + i))) /\ (LSeg ((f /^ n),(i + 1))) by A3, A6, Th5
.= (LSeg (f,(n + i))) /\ (LSeg (f,(n + (i + 1)))) by A4, A9, A6, Th5, NAT_1:11
.= {(f /. ((n + i) + 1))} by A1, A7, A8, TOPREAL1:def_6
.= {(f /. (n + (i + 1)))}
.= {((f /^ n) /. (i + 1))} by A5, FINSEQ_5:27 ;
::_thesis: verum
end;
suppose n > len f ; ::_thesis: f /^ n is unfolded
then f /^ n = <*> the carrier of (TOP-REAL 2) by RFINSEQ:def_1;
then len (f /^ n) = 0 ;
hence f /^ n is unfolded by Th26; ::_thesis: verum
end;
end;
end;
registration
let f be unfolded FinSequence of (TOP-REAL 2);
let n be Element of NAT ;
clusterf | n -> unfolded for FinSequence of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 = f | n holds
b1 is unfolded by Lm3;
clusterf /^ n -> unfolded for FinSequence of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 = f /^ n holds
b1 is unfolded by Lm4;
end;
theorem Th27: :: SPPOL_2:27
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in rng f & f is unfolded holds
f :- p is unfolded
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in rng f & f is unfolded holds
f :- p is unfolded
let p be Point of (TOP-REAL 2); ::_thesis: ( p in rng f & f is unfolded implies f :- p is unfolded )
assume p in rng f ; ::_thesis: ( not f is unfolded or f :- p is unfolded )
then ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i ) by FINSEQ_5:49;
hence ( not f is unfolded or f :- p is unfolded ) ; ::_thesis: verum
end;
Lm5: for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is unfolded holds
f -: p is unfolded
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is unfolded holds
f -: p is unfolded
let p be Point of (TOP-REAL 2); ::_thesis: ( f is unfolded implies f -: p is unfolded )
f -: p = f | (p .. f) by FINSEQ_5:def_1;
hence ( f is unfolded implies f -: p is unfolded ) ; ::_thesis: verum
end;
registration
let f be unfolded FinSequence of (TOP-REAL 2);
let p be Point of (TOP-REAL 2);
clusterf -: p -> unfolded ;
coherence
f -: p is unfolded by Lm5;
end;
theorem Th28: :: SPPOL_2:28
for f being FinSequence of (TOP-REAL 2) st f is unfolded holds
Rev f is unfolded
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is unfolded implies Rev f is unfolded )
assume A1: f is unfolded ; ::_thesis: Rev f is unfolded
A2: dom f = Seg (len f) by FINSEQ_1:def_3;
let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len (Rev f) or (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),(i + 1))) = {((Rev f) /. (i + 1))} )
assume that
A3: 1 <= i and
A4: i + 2 <= len (Rev f) ; ::_thesis: (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),(i + 1))) = {((Rev f) /. (i + 1))}
A5: len (Rev f) = len f by FINSEQ_5:def_3;
then A6: i + 1 in dom f by A3, A4, SEQ_4:135;
i + 1 <= (i + 1) + 1 by NAT_1:11;
then reconsider j9 = (len f) - (i + 1) as Element of NAT by A4, A5, INT_1:5, XXREAL_0:2;
i <= i + 2 by NAT_1:11;
then reconsider j = (len f) - i as Element of NAT by A4, A5, INT_1:5, XXREAL_0:2;
A7: j9 + (i + 1) = len f ;
i in dom f by A3, A4, A5, SEQ_4:135;
then j + 1 in dom f by A2, FINSEQ_5:2;
then A8: j9 + 2 <= len f by FINSEQ_3:25;
A9: j + (i + 1) = (len f) + 1 ;
i + (1 + 1) = (i + 1) + 1 ;
then A10: 1 <= j9 by A4, A5, XREAL_1:19;
j + i = len f ;
hence (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),(i + 1))) = (LSeg (f,j)) /\ (LSeg ((Rev f),(i + 1))) by Th2
.= (LSeg (f,(j9 + 1))) /\ (LSeg (f,j9)) by A7, Th2
.= {(f /. (j9 + 1))} by A1, A10, A8, TOPREAL1:def_6
.= {((Rev f) /. (i + 1))} by A9, A2, A6, FINSEQ_5:2, FINSEQ_5:66 ;
::_thesis: verum
end;
theorem Th29: :: SPPOL_2:29
for g being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st g is unfolded & (LSeg (p,(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} holds
<*p*> ^ g is unfolded
proof
let g be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st g is unfolded & (LSeg (p,(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} holds
<*p*> ^ g is unfolded
let p be Point of (TOP-REAL 2); ::_thesis: ( g is unfolded & (LSeg (p,(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} implies <*p*> ^ g is unfolded )
set f = <*p*>;
A1: len <*p*> = 1 by FINSEQ_1:39;
A2: <*p*> /. 1 = p by FINSEQ_4:16;
A3: len (<*p*> ^ g) = (len <*p*>) + (len g) by FINSEQ_1:22;
assume that
A4: g is unfolded and
A5: (LSeg (p,(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} ; ::_thesis: <*p*> ^ g is unfolded
let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len (<*p*> ^ g) or (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))} )
assume that
A6: 1 <= i and
A7: i + 2 <= len (<*p*> ^ g) ; ::_thesis: (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))}
A8: i + (1 + 1) = (i + 1) + 1 ;
percases ( i = len <*p*> or i <> len <*p*> ) ;
supposeA9: i = len <*p*> ; ::_thesis: (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))}
then A10: LSeg ((<*p*> ^ g),(i + 1)) = LSeg (g,1) by Th7;
now__::_thesis:_not_len_g_=_0
i <= i + 1 by NAT_1:11;
then A11: i < i + (1 + 1) by A8, NAT_1:13;
assume len g = 0 ; ::_thesis: contradiction
hence contradiction by A1, A6, A7, A3, A11, XXREAL_0:2; ::_thesis: verum
end;
then 1 <= len g by NAT_1:14;
then A12: 1 in dom g by FINSEQ_3:25;
then LSeg ((<*p*> ^ g),i) = LSeg ((<*p*> /. (len <*p*>)),(g /. 1)) by A9, Th8, RELAT_1:38;
hence (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))} by A1, A5, A2, A9, A12, A10, FINSEQ_4:69; ::_thesis: verum
end;
supposeA13: i <> len <*p*> ; ::_thesis: (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))}
reconsider j = i - (len <*p*>) as Element of NAT by A1, A6, INT_1:5;
i > len <*p*> by A1, A6, A13, XXREAL_0:1;
then (len <*p*>) + 1 <= i by NAT_1:13;
then A14: 1 <= j by XREAL_1:19;
A15: (i + 2) - (len <*p*>) <= len g by A7, A3, XREAL_1:20;
then A16: j + (1 + 1) <= len g ;
j + 1 <= (j + 1) + 1 by NAT_1:11;
then j + 1 <= len g by A15, XXREAL_0:2;
then A17: j + 1 in dom g by A14, SEQ_4:134;
A18: (len <*p*>) + (j + 1) = i + 1 ;
(len <*p*>) + j = i ;
hence (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = (LSeg (g,j)) /\ (LSeg ((<*p*> ^ g),(i + 1))) by A14, Th7
.= (LSeg (g,j)) /\ (LSeg (g,(j + 1))) by A18, Th7, NAT_1:11
.= {(g /. (j + 1))} by A4, A14, A16, TOPREAL1:def_6
.= {((<*p*> ^ g) /. (i + 1))} by A18, A17, FINSEQ_4:69 ;
::_thesis: verum
end;
end;
end;
theorem Th30: :: SPPOL_2:30
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for k being Element of NAT st f is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} holds
f ^ <*p*> is unfolded
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2)
for k being Element of NAT st f is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} holds
f ^ <*p*> is unfolded
let p be Point of (TOP-REAL 2); ::_thesis: for k being Element of NAT st f is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} holds
f ^ <*p*> is unfolded
let k be Element of NAT ; ::_thesis: ( f is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} implies f ^ <*p*> is unfolded )
set g = <*p*>;
assume that
A1: f is unfolded and
A2: k + 1 = len f and
A3: (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} ; ::_thesis: f ^ <*p*> is unfolded
A4: len <*p*> = 1 by FINSEQ_1:39;
A5: <*p*> /. 1 = p by FINSEQ_4:16;
A6: len (f ^ <*p*>) = (len f) + (len <*p*>) by FINSEQ_1:22;
let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len (f ^ <*p*>) or (LSeg ((f ^ <*p*>),i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) = {((f ^ <*p*>) /. (i + 1))} )
assume that
A7: 1 <= i and
A8: i + 2 <= len (f ^ <*p*>) ; ::_thesis: (LSeg ((f ^ <*p*>),i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) = {((f ^ <*p*>) /. (i + 1))}
A9: i + (1 + 1) = (i + 1) + 1 ;
percases ( i + 2 <= len f or i + 2 > len f ) ;
supposeA10: i + 2 <= len f ; ::_thesis: (LSeg ((f ^ <*p*>),i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) = {((f ^ <*p*>) /. (i + 1))}
then A11: i + 1 in dom f by A7, SEQ_4:135;
i + 1 <= (i + 1) + 1 by NAT_1:11;
hence (LSeg ((f ^ <*p*>),i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) = (LSeg (f,i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) by A10, Th6, XXREAL_0:2
.= (LSeg (f,i)) /\ (LSeg (f,(i + 1))) by A9, A10, Th6
.= {(f /. (i + 1))} by A1, A7, A10, TOPREAL1:def_6
.= {((f ^ <*p*>) /. (i + 1))} by A11, FINSEQ_4:68 ;
::_thesis: verum
end;
suppose i + 2 > len f ; ::_thesis: (LSeg ((f ^ <*p*>),i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) = {((f ^ <*p*>) /. (i + 1))}
then A12: len f <= i + 1 by A9, NAT_1:13;
A13: not f is empty by A4, A8, A6, A9, XREAL_1:6;
then A14: len f in dom f by FINSEQ_5:6;
i + 1 <= len f by A4, A8, A6, A9, XREAL_1:6;
then A15: i + 1 = len f by A12, XXREAL_0:1;
then A16: LSeg ((f ^ <*p*>),(i + 1)) = LSeg ((f /. (len f)),(<*p*> /. 1)) by A13, Th8;
LSeg ((f ^ <*p*>),i) = LSeg (f,k) by A2, A15, Th6;
hence (LSeg ((f ^ <*p*>),i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) = {((f ^ <*p*>) /. (i + 1))} by A3, A5, A15, A16, A14, FINSEQ_4:68; ::_thesis: verum
end;
end;
end;
theorem Th31: :: SPPOL_2:31
for f, g being FinSequence of (TOP-REAL 2)
for k being Element of NAT st f is unfolded & g is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {(f /. (len f))} & (LSeg ((f /. (len f)),(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} holds
f ^ g is unfolded
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: for k being Element of NAT st f is unfolded & g is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {(f /. (len f))} & (LSeg ((f /. (len f)),(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} holds
f ^ g is unfolded
let k be Element of NAT ; ::_thesis: ( f is unfolded & g is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {(f /. (len f))} & (LSeg ((f /. (len f)),(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} implies f ^ g is unfolded )
assume that
A1: f is unfolded and
A2: g is unfolded and
A3: k + 1 = len f and
A4: (LSeg (f,k)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {(f /. (len f))} and
A5: (LSeg ((f /. (len f)),(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} ; ::_thesis: f ^ g is unfolded
let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len (f ^ g) or (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} )
assume that
A6: 1 <= i and
A7: i + 2 <= len (f ^ g) ; ::_thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))}
A8: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
percases ( i + 2 <= len f or i + 2 > len f ) ;
supposeA9: i + 2 <= len f ; ::_thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))}
then A10: i + 1 in dom f by A6, SEQ_4:135;
A11: i + (1 + 1) = (i + 1) + 1 ;
i + 1 <= (i + 1) + 1 by NAT_1:11;
hence (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = (LSeg (f,i)) /\ (LSeg ((f ^ g),(i + 1))) by A9, Th6, XXREAL_0:2
.= (LSeg (f,i)) /\ (LSeg (f,(i + 1))) by A9, A11, Th6
.= {(f /. (i + 1))} by A1, A6, A9, TOPREAL1:def_6
.= {((f ^ g) /. (i + 1))} by A10, FINSEQ_4:68 ;
::_thesis: verum
end;
supposeA12: i + 2 > len f ; ::_thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))}
A13: i + (1 + 1) = (i + 1) + 1 ;
now__::_thesis:_(LSeg_((f_^_g),i))_/\_(LSeg_((f_^_g),(i_+_1)))_=_{((f_^_g)_/._(i_+_1))}
percases ( i <= len f or i > len f ) ;
supposeA14: i <= len f ; ::_thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))}
len g <> 0 by A7, A8, A12;
then 1 <= len g by NAT_1:14;
then A15: 1 in dom g by FINSEQ_3:25;
A16: not f is empty by A6, A14;
now__::_thesis:_(LSeg_((f_^_g),i))_/\_(LSeg_((f_^_g),(i_+_1)))_=_{((f_^_g)_/._(i_+_1))}
percases ( i = len f or i <> len f ) ;
supposeA17: i = len f ; ::_thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))}
then A18: LSeg ((f ^ g),(i + 1)) = LSeg (g,1) by Th7;
LSeg ((f ^ g),i) = LSeg ((f /. (len f)),(g /. 1)) by A16, A15, A17, Th8, RELAT_1:38;
hence (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} by A5, A15, A17, A18, FINSEQ_4:69; ::_thesis: verum
end;
suppose i <> len f ; ::_thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))}
then i < len f by A14, XXREAL_0:1;
then A19: i + 1 <= len f by NAT_1:13;
len f <= i + 1 by A12, A13, NAT_1:13;
then A20: i + 1 = len f by A19, XXREAL_0:1;
then A21: LSeg ((f ^ g),i) = LSeg (f,k) by A3, Th6;
A22: len f in dom f by A16, FINSEQ_5:6;
LSeg ((f ^ g),(i + 1)) = LSeg ((f /. (len f)),(g /. 1)) by A16, A15, A20, Th8, RELAT_1:38;
hence (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} by A4, A20, A21, A22, FINSEQ_4:68; ::_thesis: verum
end;
end;
end;
hence (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} ; ::_thesis: verum
end;
supposeA23: i > len f ; ::_thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))}
then reconsider j = i - (len f) as Element of NAT by INT_1:5;
(len f) + 1 <= i by A23, NAT_1:13;
then A24: 1 <= j by XREAL_1:19;
A25: (i + 2) - (len f) <= len g by A7, A8, XREAL_1:20;
then A26: j + (1 + 1) <= len g ;
j + 1 <= (j + 1) + 1 by NAT_1:11;
then j + 1 <= len g by A25, XXREAL_0:2;
then A27: j + 1 in dom g by A24, SEQ_4:134;
A28: (len f) + (j + 1) = i + 1 ;
(len f) + j = i ;
hence (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = (LSeg (g,j)) /\ (LSeg ((f ^ g),(i + 1))) by A24, Th7
.= (LSeg (g,j)) /\ (LSeg (g,(j + 1))) by A28, Th7, NAT_1:11
.= {(g /. (j + 1))} by A2, A24, A26, TOPREAL1:def_6
.= {((f ^ g) /. (i + 1))} by A28, A27, FINSEQ_4:69 ;
::_thesis: verum
end;
end;
end;
hence (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} ; ::_thesis: verum
end;
end;
end;
theorem Th32: :: SPPOL_2:32
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for n being Element of NAT st f is unfolded & p in LSeg (f,n) holds
Ins (f,n,p) is unfolded
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2)
for n being Element of NAT st f is unfolded & p in LSeg (f,n) holds
Ins (f,n,p) is unfolded
let p be Point of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is unfolded & p in LSeg (f,n) holds
Ins (f,n,p) is unfolded
let n be Element of NAT ; ::_thesis: ( f is unfolded & p in LSeg (f,n) implies Ins (f,n,p) is unfolded )
assume that
A1: f is unfolded and
A2: p in LSeg (f,n) ; ::_thesis: Ins (f,n,p) is unfolded
set f1 = f | n;
set g1 = (f | n) ^ <*p*>;
set f2 = f /^ n;
A3: n + 1 <= len f by A2, TOPREAL1:def_3;
A4: n <= n + 1 by NAT_1:11;
then A5: len (f | n) = n by A3, FINSEQ_1:59, XXREAL_0:2;
then A6: n + 1 = len ((f | n) ^ <*p*>) by FINSEQ_2:16;
A7: n <= len f by A3, A4, XXREAL_0:2;
1 <= (len f) - n by A3, XREAL_1:19;
then A8: 1 <= len (f /^ n) by A7, RFINSEQ:def_1;
then 1 in dom (f /^ n) by FINSEQ_3:25;
then A9: f /. (n + 1) = (f /^ n) /. 1 by FINSEQ_5:27;
A10: 1 <= n by A2, TOPREAL1:def_3;
then A11: LSeg (f,n) = LSeg ((f /. n),(f /. (n + 1))) by A3, TOPREAL1:def_3;
A12: n in dom (f | n) by A10, A5, FINSEQ_3:25;
then A13: f /. n = (f | n) /. (len (f | n)) by A5, FINSEQ_4:70;
A14: ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = ((f | n) ^ <*p*>) /. ((len (f | n)) + 1) by FINSEQ_2:16
.= p by FINSEQ_4:67 ;
then A15: (LSeg (((f | n) /. (len (f | n))),p)) \/ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) = LSeg (((f | n) /. (len (f | n))),((f /^ n) /. 1)) by A2, A11, A13, A9, TOPREAL1:5;
A16: now__::_thesis:_(f_|_n)_^_<*p*>_is_unfolded
len (f | n) <> 0 by A2, A5, TOPREAL1:def_3;
then consider k being Nat such that
A17: k + 1 = len (f | n) by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A18: k + (1 + 1) <= len f by A3, A5, A17;
percases ( k <> 0 or k = 0 ) ;
suppose k <> 0 ; ::_thesis: (f | n) ^ <*p*> is unfolded
then A19: 1 <= k by NAT_1:14;
LSeg ((f | n),k) = LSeg (f,k) by A17, Th3;
then A20: (LSeg ((f | n),k)) /\ (LSeg (f,n)) = {(f /. n)} by A1, A5, A17, A18, A19, TOPREAL1:def_6;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(LSeg_((f_|_n),k))_/\_(LSeg_(((f_|_n)_/._(len_(f_|_n))),p))_implies_x_=_f_/._n_)_&_(_x_=_f_/._n_implies_x_in_(LSeg_((f_|_n),k))_/\_(LSeg_(((f_|_n)_/._(len_(f_|_n))),p))_)_)
let x be set ; ::_thesis: ( ( x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) implies x = f /. n ) & ( x = f /. n implies x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) ) )
hereby ::_thesis: ( x = f /. n implies x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) )
assume A21: x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) ; ::_thesis: x = f /. n
then x in LSeg (((f | n) /. (len (f | n))),p) by XBOOLE_0:def_4;
then A22: x in LSeg (f,n) by A11, A13, A9, A15, XBOOLE_0:def_3;
x in LSeg ((f | n),k) by A21, XBOOLE_0:def_4;
then x in (LSeg ((f | n),k)) /\ (LSeg (f,n)) by A22, XBOOLE_0:def_4;
hence x = f /. n by A20, TARSKI:def_1; ::_thesis: verum
end;
assume A23: x = f /. n ; ::_thesis: x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p))
then x in (LSeg ((f | n),k)) /\ (LSeg (f,n)) by A20, TARSKI:def_1;
then A24: x in LSeg ((f | n),k) by XBOOLE_0:def_4;
x in LSeg (((f | n) /. (len (f | n))),p) by A13, A23, RLTOPSP1:68;
hence x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) by A24, XBOOLE_0:def_4; ::_thesis: verum
end;
then (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) = {((f | n) /. (len (f | n)))} by A13, TARSKI:def_1;
hence (f | n) ^ <*p*> is unfolded by A1, A17, Th30; ::_thesis: verum
end;
suppose k = 0 ; ::_thesis: (f | n) ^ <*p*> is unfolded
then len ((f | n) ^ <*p*>) = 1 + 1 by A17, FINSEQ_2:16;
hence (f | n) ^ <*p*> is unfolded by Th26; ::_thesis: verum
end;
end;
end;
(f | n) /. (len (f | n)) = ((f | n) ^ <*p*>) /. n by A5, A12, FINSEQ_4:68;
then LSeg (((f | n) ^ <*p*>),n) = LSeg (((f | n) /. (len (f | n))),(((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)))) by A10, A6, TOPREAL1:def_3;
then A25: (LSeg (((f | n) ^ <*p*>),n)) /\ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) = {(((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)))} by A2, A14, A11, A13, A9, TOPREAL1:8;
now__::_thesis:_((f_|_n)_^_<*p*>)_^_(f_/^_n)_is_unfolded
percases ( len (f /^ n) = 1 or len (f /^ n) <> 1 ) ;
suppose len (f /^ n) = 1 ; ::_thesis: ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded
then f /^ n = <*((f /^ n) /. 1)*> by FINSEQ_5:14;
hence ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded by A16, A6, A25, Th30; ::_thesis: verum
end;
suppose len (f /^ n) <> 1 ; ::_thesis: ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded
then len (f /^ n) > 1 by A8, XXREAL_0:1;
then A26: 1 + 1 <= len (f /^ n) by NAT_1:13;
then LSeg ((f /^ n),1) = LSeg (((f /^ n) /. 1),((f /^ n) /. (1 + 1))) by TOPREAL1:def_3;
then A27: (f /^ n) /. 1 in LSeg ((f /^ n),1) by RLTOPSP1:68;
A28: 1 + 1 <= (len f) - n by A7, A26, RFINSEQ:def_1;
then n + (1 + 1) <= len f by XREAL_1:19;
then A29: {(f /. (n + 1))} = (LSeg (f,n)) /\ (LSeg (f,(n + 1))) by A1, A10, TOPREAL1:def_6
.= (LSeg (f,n)) /\ (LSeg ((f /^ n),1)) by A28, Th5 ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(LSeg_((((f_|_n)_^_<*p*>)_/._(len_((f_|_n)_^_<*p*>))),((f_/^_n)_/._1)))_/\_(LSeg_((f_/^_n),1))_implies_x_=_(f_/^_n)_/._1_)_&_(_x_=_(f_/^_n)_/._1_implies_x_in_(LSeg_((((f_|_n)_^_<*p*>)_/._(len_((f_|_n)_^_<*p*>))),((f_/^_n)_/._1)))_/\_(LSeg_((f_/^_n),1))_)_)
let x be set ; ::_thesis: ( ( x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) implies x = (f /^ n) /. 1 ) & ( x = (f /^ n) /. 1 implies x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) ) )
hereby ::_thesis: ( x = (f /^ n) /. 1 implies x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) )
assume A30: x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) ; ::_thesis: x = (f /^ n) /. 1
then x in LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)) by XBOOLE_0:def_4;
then A31: x in LSeg (f,n) by A11, A13, A9, A15, XBOOLE_0:def_3;
x in LSeg ((f /^ n),1) by A30, XBOOLE_0:def_4;
then x in (LSeg (f,n)) /\ (LSeg ((f /^ n),1)) by A31, XBOOLE_0:def_4;
hence x = (f /^ n) /. 1 by A9, A29, TARSKI:def_1; ::_thesis: verum
end;
assume A32: x = (f /^ n) /. 1 ; ::_thesis: x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1))
then x in LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)) by RLTOPSP1:68;
hence x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) by A27, A32, XBOOLE_0:def_4; ::_thesis: verum
end;
then (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) = {((f /^ n) /. 1)} by TARSKI:def_1;
hence ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded by A1, A16, A6, A25, Th31; ::_thesis: verum
end;
end;
end;
hence Ins (f,n,p) is unfolded by FINSEQ_5:def_4; ::_thesis: verum
end;
theorem Th33: :: SPPOL_2:33
for f being FinSequence of (TOP-REAL 2) st len f <= 2 holds
f is s.n.c.
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( len f <= 2 implies f is s.n.c. )
assume A1: len f <= 2 ; ::_thesis: f is s.n.c.
let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg (f,i) misses LSeg (f,j) )
assume A2: i + 1 < j ; ::_thesis: LSeg (f,i) misses LSeg (f,j)
now__::_thesis:_(_1_<=_i_&_i_+_1_<=_len_f_&_1_<=_j_implies_not_j_+_1_<=_len_f_)
assume that
A3: 1 <= i and
A4: i + 1 <= len f and
A5: 1 <= j and
A6: j + 1 <= len f ; ::_thesis: contradiction
j + 1 <= 1 + 1 by A1, A6, XXREAL_0:2;
then j <= 1 by XREAL_1:6;
then A7: j = 1 by A5, XXREAL_0:1;
i + 1 <= 1 + 1 by A1, A4, XXREAL_0:2;
then i <= 1 by XREAL_1:6;
then i = 1 by A3, XXREAL_0:1;
hence contradiction by A2, A7; ::_thesis: verum
end;
then ( LSeg (f,i) = {} or LSeg (f,j) = {} ) by TOPREAL1:def_3;
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
Lm6: for p, q being Point of (TOP-REAL 2) holds <*p,q*> is s.n.c.
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: <*p,q*> is s.n.c.
len <*p,q*> = 2 by FINSEQ_1:44;
hence <*p,q*> is s.n.c. by Th33; ::_thesis: verum
end;
Lm7: for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT st f is s.n.c. holds
f | n is s.n.c.
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is s.n.c. holds
f | n is s.n.c.
let n be Element of NAT ; ::_thesis: ( f is s.n.c. implies f | n is s.n.c. )
assume A1: f is s.n.c. ; ::_thesis: f | n is s.n.c.
let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg ((f | n),i) misses LSeg ((f | n),j) )
assume A2: i + 1 < j ; ::_thesis: LSeg ((f | n),i) misses LSeg ((f | n),j)
percases ( i = 0 or j + 1 > len (f | n) or ( i <> 0 & j + 1 <= len (f | n) ) ) ;
supposeA3: ( i = 0 or j + 1 > len (f | n) ) ; ::_thesis: LSeg ((f | n),i) misses LSeg ((f | n),j)
now__::_thesis:_(_(_i_=_0_&_LSeg_((f_|_n),i)_=_{}_)_or_(_j_+_1_>_len_(f_|_n)_&_LSeg_((f_|_n),j)_=_{}_)_)
percases ( i = 0 or j + 1 > len (f | n) ) by A3;
case i = 0 ; ::_thesis: LSeg ((f | n),i) = {}
hence LSeg ((f | n),i) = {} by TOPREAL1:def_3; ::_thesis: verum
end;
case j + 1 > len (f | n) ; ::_thesis: LSeg ((f | n),j) = {}
hence LSeg ((f | n),j) = {} by TOPREAL1:def_3; ::_thesis: verum
end;
end;
end;
then (LSeg ((f | n),i)) /\ (LSeg ((f | n),j)) = {} ;
hence LSeg ((f | n),i) misses LSeg ((f | n),j) by XBOOLE_0:def_7; ::_thesis: verum
end;
supposethat i <> 0 and
A4: j + 1 <= len (f | n) ; ::_thesis: LSeg ((f | n),i) misses LSeg ((f | n),j)
A5: LSeg (f,i) misses LSeg (f,j) by A1, A2, TOPREAL1:def_7;
j <= j + 1 by NAT_1:11;
then i + 1 < j + 1 by A2, XXREAL_0:2;
then (LSeg ((f | n),i)) /\ (LSeg ((f | n),j)) = (LSeg (f,i)) /\ (LSeg ((f | n),j)) by A4, Th3, XXREAL_0:2
.= (LSeg (f,i)) /\ (LSeg (f,j)) by A4, Th3
.= {} by A5, XBOOLE_0:def_7 ;
hence LSeg ((f | n),i) misses LSeg ((f | n),j) by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
Lm8: for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT st f is s.n.c. holds
f /^ n is s.n.c.
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is s.n.c. holds
f /^ n is s.n.c.
let n be Element of NAT ; ::_thesis: ( f is s.n.c. implies f /^ n is s.n.c. )
assume A1: f is s.n.c. ; ::_thesis: f /^ n is s.n.c.
percases ( n <= len f or n > len f ) ;
supposeA2: n <= len f ; ::_thesis: f /^ n is s.n.c.
let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) )
assume A3: i + 1 < j ; ::_thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j)
now__::_thesis:_LSeg_((f_/^_n),i)_misses_LSeg_((f_/^_n),j)
percases ( i = 0 or j + 1 > len (f /^ n) or ( i <> 0 & j + 1 <= len (f /^ n) ) ) ;
supposeA4: ( i = 0 or j + 1 > len (f /^ n) ) ; ::_thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j)
now__::_thesis:_(_(_i_=_0_&_LSeg_((f_/^_n),i)_=_{}_)_or_(_j_+_1_>_len_(f_/^_n)_&_LSeg_((f_/^_n),j)_=_{}_)_)
percases ( i = 0 or j + 1 > len (f /^ n) ) by A4;
case i = 0 ; ::_thesis: LSeg ((f /^ n),i) = {}
hence LSeg ((f /^ n),i) = {} by TOPREAL1:def_3; ::_thesis: verum
end;
case j + 1 > len (f /^ n) ; ::_thesis: LSeg ((f /^ n),j) = {}
hence LSeg ((f /^ n),j) = {} by TOPREAL1:def_3; ::_thesis: verum
end;
end;
end;
then (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),j)) = {} ;
hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) by XBOOLE_0:def_7; ::_thesis: verum
end;
supposethat A5: i <> 0 and
A6: j + 1 <= len (f /^ n) ; ::_thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j)
A7: i <= j by A3, NAT_1:13;
1 <= i by A5, NAT_1:14;
then A8: 1 <= j by A7, XXREAL_0:2;
n + (i + 1) < n + j by A3, XREAL_1:6;
then (n + i) + 1 < n + j ;
then A9: LSeg (f,(n + i)) misses LSeg (f,(n + j)) by A1, TOPREAL1:def_7;
A10: len (f /^ n) = (len f) - n by A2, RFINSEQ:def_1;
j <= j + 1 by NAT_1:11;
then i + 1 < j + 1 by A3, XXREAL_0:2;
then i + 1 <= len (f /^ n) by A6, XXREAL_0:2;
then (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),j)) = (LSeg (f,(n + i))) /\ (LSeg ((f /^ n),j)) by A5, A10, Th5, NAT_1:14
.= (LSeg (f,(n + i))) /\ (LSeg (f,(n + j))) by A6, A10, A8, Th5
.= {} by A9, XBOOLE_0:def_7 ;
hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) ; ::_thesis: verum
end;
suppose n > len f ; ::_thesis: f /^ n is s.n.c.
then f /^ n = <*> the carrier of (TOP-REAL 2) by RFINSEQ:def_1;
then len (f /^ n) = 0 ;
hence f /^ n is s.n.c. by Th33; ::_thesis: verum
end;
end;
end;
registration
let f be s.n.c. FinSequence of (TOP-REAL 2);
let n be Element of NAT ;
clusterf | n -> s.n.c. for FinSequence of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 = f | n holds
b1 is s.n.c. by Lm7;
clusterf /^ n -> s.n.c. for FinSequence of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 = f /^ n holds
b1 is s.n.c. by Lm8;
end;
Lm9: for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is s.n.c. holds
f -: p is s.n.c.
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is s.n.c. holds
f -: p is s.n.c.
let p be Point of (TOP-REAL 2); ::_thesis: ( f is s.n.c. implies f -: p is s.n.c. )
f -: p = f | (p .. f) by FINSEQ_5:def_1;
hence ( f is s.n.c. implies f -: p is s.n.c. ) ; ::_thesis: verum
end;
registration
let f be s.n.c. FinSequence of (TOP-REAL 2);
let p be Point of (TOP-REAL 2);
clusterf -: p -> s.n.c. ;
coherence
f -: p is s.n.c. by Lm9;
end;
theorem Th34: :: SPPOL_2:34
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in rng f & f is s.n.c. holds
f :- p is s.n.c.
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in rng f & f is s.n.c. holds
f :- p is s.n.c.
let p be Point of (TOP-REAL 2); ::_thesis: ( p in rng f & f is s.n.c. implies f :- p is s.n.c. )
assume p in rng f ; ::_thesis: ( not f is s.n.c. or f :- p is s.n.c. )
then ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i ) by FINSEQ_5:49;
hence ( not f is s.n.c. or f :- p is s.n.c. ) ; ::_thesis: verum
end;
theorem Th35: :: SPPOL_2:35
for f being FinSequence of (TOP-REAL 2) st f is s.n.c. holds
Rev f is s.n.c.
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is s.n.c. implies Rev f is s.n.c. )
assume A1: f is s.n.c. ; ::_thesis: Rev f is s.n.c.
let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg ((Rev f),i) misses LSeg ((Rev f),j) )
assume A2: i + 1 < j ; ::_thesis: LSeg ((Rev f),i) misses LSeg ((Rev f),j)
percases ( i = 0 or j + 1 > len (Rev f) or ( i <> 0 & j + 1 <= len (Rev f) ) ) ;
supposeA3: ( i = 0 or j + 1 > len (Rev f) ) ; ::_thesis: LSeg ((Rev f),i) misses LSeg ((Rev f),j)
now__::_thesis:_(_(_i_=_0_&_LSeg_((Rev_f),i)_=_{}_)_or_(_j_+_1_>_len_(Rev_f)_&_LSeg_((Rev_f),j)_=_{}_)_)
percases ( i = 0 or j + 1 > len (Rev f) ) by A3;
case i = 0 ; ::_thesis: LSeg ((Rev f),i) = {}
hence LSeg ((Rev f),i) = {} by TOPREAL1:def_3; ::_thesis: verum
end;
case j + 1 > len (Rev f) ; ::_thesis: LSeg ((Rev f),j) = {}
hence LSeg ((Rev f),j) = {} by TOPREAL1:def_3; ::_thesis: verum
end;
end;
end;
then (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),j)) = {} ;
hence LSeg ((Rev f),i) misses LSeg ((Rev f),j) by XBOOLE_0:def_7; ::_thesis: verum
end;
supposethat i <> 0 and
A4: j + 1 <= len (Rev f) ; ::_thesis: LSeg ((Rev f),i) misses LSeg ((Rev f),j)
A5: j <= j + 1 by NAT_1:11;
i <= i + 1 by NAT_1:11;
then A6: i < j by A2, XXREAL_0:2;
A7: len (Rev f) = len f by FINSEQ_5:def_3;
then reconsider j9 = (len f) - j as Element of NAT by A4, A5, INT_1:5, XXREAL_0:2;
j <= len f by A4, A7, A5, XXREAL_0:2;
then reconsider i9 = (len f) - i as Element of NAT by A6, INT_1:5, XXREAL_0:2;
A8: j9 + j = len f ;
(len f) - (i + 1) > j9 by A2, XREAL_1:10;
then (i9 - 1) + 1 > j9 + 1 by XREAL_1:6;
then A9: LSeg (f,i9) misses LSeg (f,j9) by A1, TOPREAL1:def_7;
i9 + i = len f ;
hence (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),j)) = (LSeg (f,i9)) /\ (LSeg ((Rev f),j)) by Th2
.= (LSeg (f,i9)) /\ (LSeg (f,j9)) by A8, Th2
.= {} by A9, XBOOLE_0:def_7 ;
:: according to XBOOLE_0:def_7 ::_thesis: verum
end;
end;
end;
theorem Th36: :: SPPOL_2:36
for f, g being FinSequence of (TOP-REAL 2) st f is s.n.c. & g is s.n.c. & L~ f misses L~ g & ( for i being Element of NAT st 1 <= i & i + 2 <= len f holds
LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) ) & ( for i being Element of NAT st 2 <= i & i + 1 <= len g holds
LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1)) ) holds
f ^ g is s.n.c.
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( f is s.n.c. & g is s.n.c. & L~ f misses L~ g & ( for i being Element of NAT st 1 <= i & i + 2 <= len f holds
LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) ) & ( for i being Element of NAT st 2 <= i & i + 1 <= len g holds
LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1)) ) implies f ^ g is s.n.c. )
assume that
A1: f is s.n.c. and
A2: g is s.n.c. and
A3: (L~ f) /\ (L~ g) = {} and
A4: for i being Element of NAT st 1 <= i & i + 2 <= len f holds
LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) and
A5: for i being Element of NAT st 2 <= i & i + 1 <= len g holds
LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1)) ; :: according to XBOOLE_0:def_7 ::_thesis: f ^ g is s.n.c.
let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) )
assume A6: i + 1 < j ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
percases ( i = 0 or j + 1 > len (f ^ g) or ( i <> 0 & j + 1 <= len (f ^ g) ) ) ;
supposeA7: ( i = 0 or j + 1 > len (f ^ g) ) ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
now__::_thesis:_(_(_i_=_0_&_LSeg_((f_^_g),i)_=_{}_)_or_(_j_+_1_>_len_(f_^_g)_&_LSeg_((f_^_g),j)_=_{}_)_)
percases ( i = 0 or j + 1 > len (f ^ g) ) by A7;
case i = 0 ; ::_thesis: LSeg ((f ^ g),i) = {}
hence LSeg ((f ^ g),i) = {} by TOPREAL1:def_3; ::_thesis: verum
end;
case j + 1 > len (f ^ g) ; ::_thesis: LSeg ((f ^ g),j) = {}
hence LSeg ((f ^ g),j) = {} by TOPREAL1:def_3; ::_thesis: verum
end;
end;
end;
then (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),j)) = {} ;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by XBOOLE_0:def_7; ::_thesis: verum
end;
supposethat A8: i <> 0 and
A9: j + 1 <= len (f ^ g) ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
A10: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
i <= i + 1 by NAT_1:11;
then A11: i < j by A6, XXREAL_0:2;
A12: 1 <= i by A8, NAT_1:14;
now__::_thesis:_LSeg_((f_^_g),i)_misses_LSeg_((f_^_g),j)
percases ( j + 1 <= len f or j + 1 > len f ) ;
supposeA13: j + 1 <= len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
j <= j + 1 by NAT_1:11;
then i < j + 1 by A11, XXREAL_0:2;
then i < len f by A13, XXREAL_0:2;
then i + 1 <= len f by NAT_1:13;
then A14: LSeg ((f ^ g),i) = LSeg (f,i) by Th6;
LSeg ((f ^ g),j) = LSeg (f,j) by A13, Th6;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A1, A6, A14, TOPREAL1:def_7; ::_thesis: verum
end;
suppose j + 1 > len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
then A15: len f <= j by NAT_1:13;
then reconsider j9 = j - (len f) as Element of NAT by INT_1:5;
(j + 1) - (len f) <= len g by A9, A10, XREAL_1:20;
then A16: j9 + 1 <= len g ;
A17: (len f) + j9 = j ;
now__::_thesis:_LSeg_((f_^_g),i)_misses_LSeg_((f_^_g),j)
percases ( i <= len f or i > len f ) ;
supposeA18: i <= len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
then A19: not f is empty by A12;
now__::_thesis:_LSeg_((f_^_g),i)_misses_LSeg_((f_^_g),j)
percases ( i = len f or i <> len f ) ;
supposeA20: i = len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
not g is empty by A16;
then A21: LSeg ((f ^ g),i) = LSeg ((f /. (len f)),(g /. 1)) by A19, A20, Th8;
((len f) + 1) + 1 <= j by A6, A20, NAT_1:13;
then (len f) + (1 + 1) <= j ;
then A22: 1 + 1 <= j9 by XREAL_1:19;
then LSeg ((f ^ g),j) = LSeg (g,j9) by A17, Th7, XXREAL_0:2;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A5, A16, A22, A21; ::_thesis: verum
end;
suppose i <> len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
then i < len f by A18, XXREAL_0:1;
then i + 1 <= len f by NAT_1:13;
then A23: LSeg ((f ^ g),i) = LSeg (f,i) by Th6;
now__::_thesis:_LSeg_((f_^_g),i)_misses_LSeg_((f_^_g),j)
percases ( j = len f or j <> len f ) ;
supposeA24: j = len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
then (i + 1) + 1 <= len f by A6, NAT_1:13;
then A25: i + (1 + 1) <= len f ;
not g is empty by A9, A10, A24, XREAL_1:6;
then A26: LSeg ((f ^ g),j) = LSeg ((f /. (len f)),(g /. 1)) by A19, A24, Th8;
i in NAT by ORDINAL1:def_12;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A4, A8, A23, A25, A26, NAT_1:14; ::_thesis: verum
end;
suppose j <> len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
then len f < j by A15, XXREAL_0:1;
then (len f) + 1 <= j by NAT_1:13;
then 1 <= j9 by XREAL_1:19;
then LSeg ((f ^ g),((len f) + j9)) = LSeg (g,j9) by Th7;
then A27: LSeg ((f ^ g),j) c= L~ g by TOPREAL3:19;
LSeg ((f ^ g),i) c= L~ f by A23, TOPREAL3:19;
then (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),j)) = {} by A3, A27, XBOOLE_1:3, XBOOLE_1:27;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) ; ::_thesis: verum
end;
end;
end;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) ; ::_thesis: verum
end;
supposeA28: i > len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
then j <> len f by A6, NAT_1:13;
then len f < j by A15, XXREAL_0:1;
then (len f) + 1 <= j by NAT_1:13;
then 1 <= j9 by XREAL_1:19;
then A29: LSeg ((f ^ g),((len f) + j9)) = LSeg (g,j9) by Th7;
reconsider i9 = i - (len f) as Element of NAT by A28, INT_1:5;
(len f) + 1 <= i by A28, NAT_1:13;
then 1 <= i9 by XREAL_1:19;
then A30: LSeg ((f ^ g),((len f) + i9)) = LSeg (g,i9) by Th7;
(i + 1) - (len f) < j9 by A6, XREAL_1:9;
then i9 + 1 < j9 ;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A2, A30, A29, TOPREAL1:def_7; ::_thesis: verum
end;
end;
end;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) ; ::_thesis: verum
end;
end;
end;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) ; ::_thesis: verum
end;
end;
end;
theorem Th37: :: SPPOL_2:37
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for n being Element of NAT st f is unfolded & f is s.n.c. & p in LSeg (f,n) & not p in rng f holds
Ins (f,n,p) is s.n.c.
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2)
for n being Element of NAT st f is unfolded & f is s.n.c. & p in LSeg (f,n) & not p in rng f holds
Ins (f,n,p) is s.n.c.
let p be Point of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is unfolded & f is s.n.c. & p in LSeg (f,n) & not p in rng f holds
Ins (f,n,p) is s.n.c.
let n be Element of NAT ; ::_thesis: ( f is unfolded & f is s.n.c. & p in LSeg (f,n) & not p in rng f implies Ins (f,n,p) is s.n.c. )
assume that
A1: f is unfolded and
A2: f is s.n.c. and
A3: p in LSeg (f,n) and
A4: not p in rng f ; ::_thesis: Ins (f,n,p) is s.n.c.
set fp = Ins (f,n,p);
let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) )
assume A5: i + 1 < j ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
percases ( i = 0 or j + 1 > len (Ins (f,n,p)) or ( i <> 0 & j + 1 <= len (Ins (f,n,p)) ) ) ;
supposeA6: ( i = 0 or j + 1 > len (Ins (f,n,p)) ) ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
now__::_thesis:_(_(_i_=_0_&_LSeg_((Ins_(f,n,p)),i)_=_{}_)_or_(_j_+_1_>_len_(Ins_(f,n,p))_&_LSeg_((Ins_(f,n,p)),j)_=_{}_)_)
percases ( i = 0 or j + 1 > len (Ins (f,n,p)) ) by A6;
case i = 0 ; ::_thesis: LSeg ((Ins (f,n,p)),i) = {}
hence LSeg ((Ins (f,n,p)),i) = {} by TOPREAL1:def_3; ::_thesis: verum
end;
case j + 1 > len (Ins (f,n,p)) ; ::_thesis: LSeg ((Ins (f,n,p)),j) = {}
hence LSeg ((Ins (f,n,p)),j) = {} by TOPREAL1:def_3; ::_thesis: verum
end;
end;
end;
then (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) = {} ;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by XBOOLE_0:def_7; ::_thesis: verum
end;
supposethat A7: i <> 0 and
A8: j + 1 <= len (Ins (f,n,p)) ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
A9: 1 <= i by A7, NAT_1:14;
set f1 = f | n;
set g1 = (f | n) ^ <*p*>;
set f2 = f /^ n;
A10: Ins (f,n,p) = ((f | n) ^ <*p*>) ^ (f /^ n) by FINSEQ_5:def_4;
i <= i + 1 by NAT_1:11;
then A11: i < j by A5, XXREAL_0:2;
A12: i + 1 <= (i + 1) + 1 by NAT_1:11;
A13: len (Ins (f,n,p)) = (len f) + 1 by FINSEQ_5:69;
A14: 1 <= n by A3, TOPREAL1:def_3;
A15: n + 1 <= len f by A3, TOPREAL1:def_3;
A16: len ((f | n) ^ <*p*>) = (len (f | n)) + 1 by FINSEQ_2:16;
then A17: ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = p by FINSEQ_4:67;
A18: n <= n + 1 by NAT_1:11;
then A19: n <= len f by A15, XXREAL_0:2;
A20: len (f | n) = n by A15, A18, FINSEQ_1:59, XXREAL_0:2;
(i + 1) + 1 <= j by A5, NAT_1:13;
then ((i + 1) + 1) + 1 <= j + 1 by XREAL_1:6;
then A21: ((i + 1) + 1) + 1 <= (len f) + 1 by A8, A13, XXREAL_0:2;
then (i + 1) + 1 <= len f by XREAL_1:6;
then A22: i + 1 <= len f by A12, XXREAL_0:2;
now__::_thesis:_LSeg_((Ins_(f,n,p)),i)_misses_LSeg_((Ins_(f,n,p)),j)
percases ( j + 1 <= n or j + 1 > n ) ;
supposeA23: j + 1 <= n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
then A24: LSeg ((Ins (f,n,p)),j) = LSeg (((f | n) ^ <*p*>),j) by A10, A16, A18, A20, Th6, XXREAL_0:2
.= LSeg ((f | n),j) by A20, A23, Th6
.= LSeg (f,j) by A20, A23, Th3 ;
j <= j + 1 by NAT_1:11;
then i < j + 1 by A11, XXREAL_0:2;
then i < n by A23, XXREAL_0:2;
then A25: i + 1 <= n by NAT_1:13;
then LSeg ((Ins (f,n,p)),i) = LSeg (((f | n) ^ <*p*>),i) by A10, A16, A18, A20, Th6, XXREAL_0:2
.= LSeg ((f | n),i) by A20, A25, Th6
.= LSeg (f,i) by A20, A25, Th3 ;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by A2, A5, A24, TOPREAL1:def_7; ::_thesis: verum
end;
suppose j + 1 > n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
then A26: n <= j by NAT_1:13;
now__::_thesis:_LSeg_((Ins_(f,n,p)),i)_misses_LSeg_((Ins_(f,n,p)),j)
percases ( i <= n + 1 or i > n + 1 ) ;
supposeA27: i <= n + 1 ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
A28: 1 <= n + 1 by NAT_1:11;
1 <= (len f) - n by A15, XREAL_1:19;
then 1 <= len (f /^ n) by A19, RFINSEQ:def_1;
then 1 in dom (f /^ n) by FINSEQ_3:25;
then A29: f /. (n + 1) = (f /^ n) /. 1 by FINSEQ_5:27;
len ((f | n) ^ <*p*>) in dom ((f | n) ^ <*p*>) by FINSEQ_5:6;
then A30: (Ins (f,n,p)) /. (n + 1) = ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) by A10, A16, A20, FINSEQ_4:68;
A31: (Ins (f,n,p)) /. ((n + 1) + 1) = f /. (n + 1) by A15, FINSEQ_5:74;
A32: n in dom (f | n) by A14, A20, FINSEQ_3:25;
then A33: f /. n = (f | n) /. (len (f | n)) by A20, FINSEQ_4:70;
(n + 1) + 1 <= len (Ins (f,n,p)) by A13, A15, XREAL_1:6;
then A34: LSeg ((Ins (f,n,p)),(n + 1)) = LSeg (p,((f /^ n) /. 1)) by A17, A29, A31, A28, A30, TOPREAL1:def_3;
A35: (f | n) /. (len (f | n)) = ((f | n) ^ <*p*>) /. (len (f | n)) by A20, A32, FINSEQ_4:68;
A36: LSeg ((Ins (f,n,p)),n) = LSeg (((f | n) ^ <*p*>),n) by A10, A16, A20, Th6
.= LSeg (((f | n) /. (len (f | n))),p) by A16, A17, A14, A20, A35, TOPREAL1:def_3 ;
A37: LSeg (f,n) = LSeg ((f /. n),(f /. (n + 1))) by A14, A15, TOPREAL1:def_3;
then A38: (LSeg (((f | n) /. (len (f | n))),p)) \/ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) = LSeg (((f | n) /. (len (f | n))),((f /^ n) /. 1)) by A3, A17, A33, A29, TOPREAL1:5;
A39: (LSeg (((f | n) /. (len (f | n))),p)) /\ (LSeg (p,((f /^ n) /. 1))) = {p} by A3, A37, A33, A29, TOPREAL1:8;
now__::_thesis:_LSeg_((Ins_(f,n,p)),i)_misses_LSeg_((Ins_(f,n,p)),j)
percases ( i < n or i = n or i > n ) by XXREAL_0:1;
suppose i < n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
then A40: i + 1 <= n by NAT_1:13;
then A41: LSeg ((Ins (f,n,p)),i) = LSeg (((f | n) ^ <*p*>),i) by A10, A16, A18, A20, Th6, XXREAL_0:2
.= LSeg ((f | n),i) by A20, A40, Th6
.= LSeg (f,i) by A20, A40, Th3 ;
now__::_thesis:_LSeg_((Ins_(f,n,p)),i)_misses_LSeg_((Ins_(f,n,p)),j)
percases ( j = n or j <> n ) ;
supposeA42: j = n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
then A43: LSeg (f,i) misses LSeg (f,n) by A2, A5, TOPREAL1:def_7;
(LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) c= (LSeg (f,i)) /\ (LSeg (f,n)) by A37, A33, A29, A38, A36, A41, A42, XBOOLE_1:7, XBOOLE_1:26;
then (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) c= {} by A43, XBOOLE_0:def_7;
then (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) = {} by XBOOLE_1:3;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by XBOOLE_0:def_7; ::_thesis: verum
end;
suppose j <> n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
then n < j by A26, XXREAL_0:1;
then A44: n + 1 <= j by NAT_1:13;
now__::_thesis:_LSeg_((Ins_(f,n,p)),i)_misses_LSeg_((Ins_(f,n,p)),j)
percases ( j = n + 1 or j <> n + 1 ) ;
supposeA45: j = n + 1 ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
now__::_thesis:_LSeg_((Ins_(f,n,p)),i)_misses_LSeg_((Ins_(f,n,p)),j)
percases ( i + 1 = n or i + 1 <> n ) ;
supposeA46: i + 1 = n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
A47: i + (1 + 1) <= len f by A21, XREAL_1:6;
LSeg ((Ins (f,n,p)),i) = LSeg (((f | n) ^ <*p*>),i) by A10, A16, A20, A46, Th6, NAT_1:11
.= LSeg ((f | n),i) by A20, A46, Th6
.= LSeg (f,i) by A20, A46, Th3 ;
then A48: (LSeg ((Ins (f,n,p)),i)) /\ (LSeg (f,n)) = {(f /. n)} by A1, A9, A46, A47, TOPREAL1:def_6;
assume not LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: contradiction
then consider x being set such that
A49: x in (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) by XBOOLE_0:4;
A50: x in LSeg ((Ins (f,n,p)),i) by A49, XBOOLE_0:def_4;
A51: x in LSeg ((Ins (f,n,p)),j) by A49, XBOOLE_0:def_4;
then x in LSeg (f,n) by A17, A37, A33, A29, A38, A34, A45, XBOOLE_0:def_3;
then x in {(f /. n)} by A48, A50, XBOOLE_0:def_4;
then A52: x = f /. n by TARSKI:def_1;
then x in LSeg ((Ins (f,n,p)),n) by A33, A36, RLTOPSP1:68;
then x in (LSeg ((Ins (f,n,p)),n)) /\ (LSeg ((Ins (f,n,p)),(n + 1))) by A45, A51, XBOOLE_0:def_4;
then A53: p = f /. n by A36, A34, A39, A52, TARSKI:def_1;
n in dom f by A14, A15, SEQ_4:134;
hence contradiction by A4, A53, PARTFUN2:2; ::_thesis: verum
end;
suppose i + 1 <> n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
then i + 1 < n by A40, XXREAL_0:1;
then A54: LSeg (f,i) misses LSeg (f,n) by A2, TOPREAL1:def_7;
(LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) c= (LSeg (f,i)) /\ (LSeg (f,n)) by A17, A37, A33, A29, A38, A34, A41, A45, XBOOLE_1:7, XBOOLE_1:26;
then (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) c= {} by A54, XBOOLE_0:def_7;
then (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) = {} by XBOOLE_1:3;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: verum
end;
supposeA55: j <> n + 1 ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
reconsider nj = j - (n + 1) as Element of NAT by A44, INT_1:5;
A56: n + 1 < j by A44, A55, XXREAL_0:1;
then (n + 1) + 1 <= j by NAT_1:13;
then A57: 1 <= nj by XREAL_1:19;
reconsider j9 = j - 1 as Element of NAT by A9, A11, INT_1:5, XXREAL_0:2;
A58: n + nj = j9 ;
(i + 1) + 1 <= n + 1 by A40, XREAL_1:6;
then (i + 1) + 1 < j by A56, XXREAL_0:2;
then A59: i + 1 < j9 by XREAL_1:20;
j = nj + (n + 1) ;
then LSeg ((Ins (f,n,p)),j) = LSeg ((f /^ n),nj) by A10, A16, A20, A57, Th7
.= LSeg (f,j9) by A19, A57, A58, Th4 ;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by A2, A41, A59, TOPREAL1:def_7; ::_thesis: verum
end;
end;
end;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: verum
end;
end;
end;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: verum
end;
supposeA60: i = n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
then reconsider nj = j - (n + 1) as Element of NAT by A5, INT_1:5;
A61: (n + 1) + 1 <= j by A5, A60, NAT_1:13;
then A62: 1 <= nj by XREAL_1:19;
reconsider j9 = j - 1 as Element of NAT by A9, A11, INT_1:5, XXREAL_0:2;
A63: n + nj = j9 ;
j = nj + (n + 1) ;
then A64: LSeg ((Ins (f,n,p)),j) = LSeg ((f /^ n),nj) by A10, A16, A20, A62, Th7
.= LSeg (f,j9) by A19, A62, A63, Th4 ;
now__::_thesis:_LSeg_((Ins_(f,n,p)),i)_misses_LSeg_((Ins_(f,n,p)),j)
percases ( j <> (n + 1) + 1 or j = (n + 1) + 1 ) ;
suppose j <> (n + 1) + 1 ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
then (n + 1) + 1 < j by A61, XXREAL_0:1;
then i + 1 < j9 by A60, XREAL_1:20;
then A65: LSeg (f,i) misses LSeg (f,j9) by A2, TOPREAL1:def_7;
(LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) c= (LSeg (f,i)) /\ (LSeg (f,j9)) by A37, A33, A29, A38, A36, A60, A64, XBOOLE_1:7, XBOOLE_1:26;
then (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) c= {} by A65, XBOOLE_0:def_7;
then (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) = {} by XBOOLE_1:3;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by XBOOLE_0:def_7; ::_thesis: verum
end;
supposeA66: j = (n + 1) + 1 ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
then n + (1 + 1) <= len f by A8, A13, XREAL_1:6;
then A67: (LSeg (f,n)) /\ (LSeg (f,j9)) = {(f /. j9)} by A1, A14, A66, TOPREAL1:def_6;
assume not LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: contradiction
then consider x being set such that
A68: x in (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) by XBOOLE_0:4;
A69: x in LSeg ((Ins (f,n,p)),j) by A68, XBOOLE_0:def_4;
A70: x in LSeg ((Ins (f,n,p)),i) by A68, XBOOLE_0:def_4;
then x in LSeg (f,n) by A37, A33, A29, A38, A36, A60, XBOOLE_0:def_3;
then x in {(f /. (n + 1))} by A64, A66, A67, A69, XBOOLE_0:def_4;
then A71: x = f /. (n + 1) by TARSKI:def_1;
then x in LSeg ((Ins (f,n,p)),(n + 1)) by A29, A34, RLTOPSP1:68;
then x in (LSeg ((Ins (f,n,p)),n)) /\ (LSeg ((Ins (f,n,p)),(n + 1))) by A60, A70, XBOOLE_0:def_4;
then A72: p = f /. (n + 1) by A36, A34, A39, A71, TARSKI:def_1;
n + 1 in dom f by A14, A15, SEQ_4:134;
hence contradiction by A4, A72, PARTFUN2:2; ::_thesis: verum
end;
end;
end;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: verum
end;
supposeA73: i > n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
reconsider j9 = j - 1 as Element of NAT by A9, A11, INT_1:5, XXREAL_0:2;
i >= n + 1 by A73, NAT_1:13;
then A74: i = n + 1 by A27, XXREAL_0:1;
then n + 1 < j9 by A5, XREAL_1:20;
then A75: LSeg (f,n) misses LSeg (f,j9) by A2, TOPREAL1:def_7;
n + 1 <= (n + 1) + 1 by NAT_1:11;
then reconsider nj = j - (n + 1) as Element of NAT by A5, A74, INT_1:5, XXREAL_0:2;
A76: 1 <= nj by A5, A74, XREAL_1:19;
A77: n + nj = j9 ;
j = nj + (n + 1) ;
then LSeg ((Ins (f,n,p)),j) = LSeg ((f /^ n),nj) by A10, A16, A20, A76, Th7
.= LSeg (f,j9) by A19, A76, A77, Th4 ;
then (LSeg ((Ins (f,n,p)),(n + 1))) /\ (LSeg ((Ins (f,n,p)),j)) c= (LSeg (f,n)) /\ (LSeg (f,j9)) by A17, A37, A33, A29, A38, A34, XBOOLE_1:7, XBOOLE_1:26;
then (LSeg ((Ins (f,n,p)),(n + 1))) /\ (LSeg ((Ins (f,n,p)),j)) c= {} by A75, XBOOLE_0:def_7;
then (LSeg ((Ins (f,n,p)),(n + 1))) /\ (LSeg ((Ins (f,n,p)),j)) = {} by XBOOLE_1:3;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by A74, XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: verum
end;
supposeA78: i > n + 1 ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
then reconsider nj = j - (n + 1) as Element of NAT by A11, INT_1:5, XXREAL_0:2;
n + 1 < j by A11, A78, XXREAL_0:2;
then (n + 1) + 1 <= j by NAT_1:13;
then A79: 1 <= nj by XREAL_1:19;
reconsider ni = i - (n + 1) as Element of NAT by A78, INT_1:5;
(n + 1) + 1 <= i by A78, NAT_1:13;
then A80: 1 <= ni by XREAL_1:19;
len f <= (len f) + 1 by NAT_1:11;
then i + 1 <= (len f) + 1 by A22, XXREAL_0:2;
then (i + 1) - (n + 1) <= ((len f) + 1) - (n + 1) by XREAL_1:9;
then A81: ni + 1 <= (len f) - n ;
reconsider i9 = i - 1 as Element of NAT by A7, INT_1:5, NAT_1:14;
reconsider j9 = j - 1 as Element of NAT by A9, A11, INT_1:5, XXREAL_0:2;
A82: n + ni = i9 ;
(i + 1) - 1 < j9 by A5, XREAL_1:9;
then A83: i9 + 1 < j9 ;
A84: n + nj = j9 ;
j = nj + (n + 1) ;
then A85: LSeg ((Ins (f,n,p)),j) = LSeg ((f /^ n),nj) by A10, A16, A20, A79, Th7
.= LSeg (f,j9) by A19, A79, A84, Th4 ;
i = ni + (n + 1) ;
then LSeg ((Ins (f,n,p)),i) = LSeg ((f /^ n),ni) by A10, A16, A20, A80, Th7
.= LSeg (f,i9) by A80, A81, A82, Th5 ;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by A2, A83, A85, TOPREAL1:def_7; ::_thesis: verum
end;
end;
end;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: verum
end;
end;
end;
hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: verum
end;
end;
end;
registration
cluster <*> the carrier of (TOP-REAL 2) -> special ;
coherence
<*> the carrier of (TOP-REAL 2) is special
proof
set f = <*> the carrier of (TOP-REAL 2);
let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len (<*> the carrier of (TOP-REAL 2)) or ((<*> the carrier of (TOP-REAL 2)) /. i) `1 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `1 or ((<*> the carrier of (TOP-REAL 2)) /. i) `2 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `2 )
assume that
1 <= i and
A1: i + 1 <= len (<*> the carrier of (TOP-REAL 2)) ; ::_thesis: ( ((<*> the carrier of (TOP-REAL 2)) /. i) `1 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `1 or ((<*> the carrier of (TOP-REAL 2)) /. i) `2 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `2 )
thus ( ((<*> the carrier of (TOP-REAL 2)) /. i) `1 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `1 or ((<*> the carrier of (TOP-REAL 2)) /. i) `2 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `2 ) by A1; ::_thesis: verum
end;
end;
registration
let p be Point of (TOP-REAL 2);
cluster<*p*> -> special for FinSequence of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 = <*p*> holds
b1 is special
proof
set f = <*p*>;
<*p*> is special
proof
let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len <*p*> or (<*p*> /. i) `1 = (<*p*> /. (i + 1)) `1 or (<*p*> /. i) `2 = (<*p*> /. (i + 1)) `2 )
assume that
A1: 1 <= i and
A2: i + 1 <= len <*p*> ; ::_thesis: ( (<*p*> /. i) `1 = (<*p*> /. (i + 1)) `1 or (<*p*> /. i) `2 = (<*p*> /. (i + 1)) `2 )
len <*p*> = 0 + 1 by FINSEQ_1:39;
hence ( (<*p*> /. i) `1 = (<*p*> /. (i + 1)) `1 or (<*p*> /. i) `2 = (<*p*> /. (i + 1)) `2 ) by A1, A2, XREAL_1:6; ::_thesis: verum
end;
hence for b1 being FinSequence of (TOP-REAL 2) st b1 = <*p*> holds
b1 is special ; ::_thesis: verum
end;
end;
theorem Th38: :: SPPOL_2:38
for p, q being Point of (TOP-REAL 2) st ( p `1 = q `1 or p `2 = q `2 ) holds
<*p,q*> is special
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: ( ( p `1 = q `1 or p `2 = q `2 ) implies <*p,q*> is special )
assume A1: ( p `1 = q `1 or p `2 = q `2 ) ; ::_thesis: <*p,q*> is special
set f = <*p,q*>;
let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len <*p,q*> or (<*p,q*> /. i) `1 = (<*p,q*> /. (i + 1)) `1 or (<*p,q*> /. i) `2 = (<*p,q*> /. (i + 1)) `2 )
assume that
A2: 1 <= i and
A3: i + 1 <= len <*p,q*> ; ::_thesis: ( (<*p,q*> /. i) `1 = (<*p,q*> /. (i + 1)) `1 or (<*p,q*> /. i) `2 = (<*p,q*> /. (i + 1)) `2 )
len <*p,q*> = 1 + 1 by FINSEQ_1:44;
then i <= 1 by A3, XREAL_1:6;
then A4: i = 1 by A2, XXREAL_0:1;
then <*p,q*> /. i = p by FINSEQ_4:17;
hence ( (<*p,q*> /. i) `1 = (<*p,q*> /. (i + 1)) `1 or (<*p,q*> /. i) `2 = (<*p,q*> /. (i + 1)) `2 ) by A1, A4, FINSEQ_4:17; ::_thesis: verum
end;
Lm10: for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT st f is special holds
f | n is special
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is special holds
f | n is special
let n be Element of NAT ; ::_thesis: ( f is special implies f | n is special )
assume A1: f is special ; ::_thesis: f | n is special
let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len (f | n) or ((f | n) /. i) `1 = ((f | n) /. (i + 1)) `1 or ((f | n) /. i) `2 = ((f | n) /. (i + 1)) `2 )
assume that
A2: 1 <= i and
A3: i + 1 <= len (f | n) ; ::_thesis: ( ((f | n) /. i) `1 = ((f | n) /. (i + 1)) `1 or ((f | n) /. i) `2 = ((f | n) /. (i + 1)) `2 )
i in dom (f | n) by A2, A3, SEQ_4:134;
then A4: (f | n) /. i = f /. i by FINSEQ_4:70;
i + 1 in dom (f | n) by A2, A3, SEQ_4:134;
then A5: (f | n) /. (i + 1) = f /. (i + 1) by FINSEQ_4:70;
len (f | n) <= len f by FINSEQ_5:16;
then i + 1 <= len f by A3, XXREAL_0:2;
hence ( ((f | n) /. i) `1 = ((f | n) /. (i + 1)) `1 or ((f | n) /. i) `2 = ((f | n) /. (i + 1)) `2 ) by A1, A2, A4, A5, TOPREAL1:def_5; ::_thesis: verum
end;
Lm11: for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT st f is special holds
f /^ n is special
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is special holds
f /^ n is special
let n be Element of NAT ; ::_thesis: ( f is special implies f /^ n is special )
assume A1: f is special ; ::_thesis: f /^ n is special
percases ( n <= len f or n > len f ) ;
supposeA2: n <= len f ; ::_thesis: f /^ n is special
let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len (f /^ n) or ((f /^ n) /. i) `1 = ((f /^ n) /. (i + 1)) `1 or ((f /^ n) /. i) `2 = ((f /^ n) /. (i + 1)) `2 )
assume that
A3: 1 <= i and
A4: i + 1 <= len (f /^ n) ; ::_thesis: ( ((f /^ n) /. i) `1 = ((f /^ n) /. (i + 1)) `1 or ((f /^ n) /. i) `2 = ((f /^ n) /. (i + 1)) `2 )
i in dom (f /^ n) by A3, A4, SEQ_4:134;
then A5: (f /^ n) /. i = f /. (n + i) by FINSEQ_5:27;
i <= n + i by NAT_1:11;
then A6: 1 <= n + i by A3, XXREAL_0:2;
i + 1 in dom (f /^ n) by A3, A4, SEQ_4:134;
then A7: (f /^ n) /. (i + 1) = f /. (n + (i + 1)) by FINSEQ_5:27
.= f /. ((n + i) + 1) ;
len (f /^ n) = (len f) - n by A2, RFINSEQ:def_1;
then n + (i + 1) <= len f by A4, XREAL_1:19;
hence ( ((f /^ n) /. i) `1 = ((f /^ n) /. (i + 1)) `1 or ((f /^ n) /. i) `2 = ((f /^ n) /. (i + 1)) `2 ) by A1, A5, A7, A6, TOPREAL1:def_5; ::_thesis: verum
end;
suppose n > len f ; ::_thesis: f /^ n is special
then f /^ n = <*> the carrier of (TOP-REAL 2) by RFINSEQ:def_1;
hence f /^ n is special ; ::_thesis: verum
end;
end;
end;
registration
let f be special FinSequence of (TOP-REAL 2);
let n be Element of NAT ;
clusterf | n -> special for FinSequence of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 = f | n holds
b1 is special by Lm10;
clusterf /^ n -> special for FinSequence of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 = f /^ n holds
b1 is special by Lm11;
end;
theorem Th39: :: SPPOL_2:39
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in rng f & f is special holds
f :- p is special
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in rng f & f is special holds
f :- p is special
let p be Point of (TOP-REAL 2); ::_thesis: ( p in rng f & f is special implies f :- p is special )
assume p in rng f ; ::_thesis: ( not f is special or f :- p is special )
then ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i ) by FINSEQ_5:49;
hence ( not f is special or f :- p is special ) ; ::_thesis: verum
end;
Lm12: for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is special holds
f -: p is special
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is special holds
f -: p is special
let p be Point of (TOP-REAL 2); ::_thesis: ( f is special implies f -: p is special )
f -: p = f | (p .. f) by FINSEQ_5:def_1;
hence ( f is special implies f -: p is special ) ; ::_thesis: verum
end;
registration
let f be special FinSequence of (TOP-REAL 2);
let p be Point of (TOP-REAL 2);
clusterf -: p -> special ;
coherence
f -: p is special by Lm12;
end;
theorem Th40: :: SPPOL_2:40
for f being FinSequence of (TOP-REAL 2) st f is special holds
Rev f is special
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is special implies Rev f is special )
assume A1: f is special ; ::_thesis: Rev f is special
A2: len (Rev f) = len f by FINSEQ_5:def_3;
let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len (Rev f) or ((Rev f) /. i) `1 = ((Rev f) /. (i + 1)) `1 or ((Rev f) /. i) `2 = ((Rev f) /. (i + 1)) `2 )
assume that
A3: 1 <= i and
A4: i + 1 <= len (Rev f) ; ::_thesis: ( ((Rev f) /. i) `1 = ((Rev f) /. (i + 1)) `1 or ((Rev f) /. i) `2 = ((Rev f) /. (i + 1)) `2 )
i <= i + 1 by NAT_1:11;
then reconsider j = (len f) - i as Element of NAT by A4, A2, INT_1:5, XXREAL_0:2;
j <= (len f) - 1 by A3, XREAL_1:10;
then A5: j + 1 <= ((len f) - 1) + 1 by XREAL_1:6;
A6: (1 + i) + j = (len f) + 1 ;
A7: (i + 1) - i <= j by A4, A2, XREAL_1:9;
then j in dom f by A5, SEQ_4:134;
then A8: (Rev f) /. (i + 1) = f /. j by A6, FINSEQ_5:66;
A9: i + (j + 1) = (len f) + 1 ;
j + 1 in dom f by A5, A7, SEQ_4:134;
then (Rev f) /. i = f /. (j + 1) by A9, FINSEQ_5:66;
hence ( ((Rev f) /. i) `1 = ((Rev f) /. (i + 1)) `1 or ((Rev f) /. i) `2 = ((Rev f) /. (i + 1)) `2 ) by A1, A5, A7, A8, TOPREAL1:def_5; ::_thesis: verum
end;
Lm13: for f, g being FinSequence of (TOP-REAL 2) st f is special & g is special & ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) holds
f ^ g is special
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( f is special & g is special & ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) implies f ^ g is special )
assume that
A1: f is special and
A2: g is special and
A3: ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) ; ::_thesis: f ^ g is special
let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len (f ^ g) or ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 )
assume that
A4: 1 <= i and
A5: i + 1 <= len (f ^ g) ; ::_thesis: ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 )
A6: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
percases ( i < len f or i = len f or i > len f ) by XXREAL_0:1;
suppose i < len f ; ::_thesis: ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 )
then A7: i + 1 <= len f by NAT_1:13;
then i + 1 in dom f by A4, SEQ_4:134;
then A8: (f ^ g) /. (i + 1) = f /. (i + 1) by FINSEQ_4:68;
i in dom f by A4, A7, SEQ_4:134;
then (f ^ g) /. i = f /. i by FINSEQ_4:68;
hence ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 ) by A1, A4, A7, A8, TOPREAL1:def_5; ::_thesis: verum
end;
supposeA9: i = len f ; ::_thesis: ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 )
then i in dom f by A4, FINSEQ_3:25;
then A10: (f ^ g) /. i = f /. i by FINSEQ_4:68;
1 <= len g by A5, A6, A9, XREAL_1:6;
then 1 in dom g by FINSEQ_3:25;
hence ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 ) by A3, A9, A10, FINSEQ_4:69; ::_thesis: verum
end;
supposeA11: i > len f ; ::_thesis: ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 )
then reconsider j = i - (len f) as Element of NAT by INT_1:5;
(len f) + 1 <= i by A11, NAT_1:13;
then A12: 1 <= j by XREAL_1:19;
A13: (len f) + (j + 1) = i + 1 ;
A14: (i + 1) - (len f) <= len g by A5, A6, XREAL_1:20;
then j + 1 in dom g by A12, SEQ_4:134;
then A15: (f ^ g) /. (i + 1) = g /. (j + 1) by A13, FINSEQ_4:69;
A16: (len f) + j = i ;
j + 1 <= len g by A14;
then j in dom g by A12, SEQ_4:134;
then (f ^ g) /. i = g /. j by A16, FINSEQ_4:69;
hence ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 ) by A2, A12, A14, A15, TOPREAL1:def_5; ::_thesis: verum
end;
end;
end;
theorem Th41: :: SPPOL_2:41
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for n being Element of NAT st f is special & p in LSeg (f,n) holds
Ins (f,n,p) is special
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2)
for n being Element of NAT st f is special & p in LSeg (f,n) holds
Ins (f,n,p) is special
let p be Point of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is special & p in LSeg (f,n) holds
Ins (f,n,p) is special
let n be Element of NAT ; ::_thesis: ( f is special & p in LSeg (f,n) implies Ins (f,n,p) is special )
assume that
A1: f is special and
A2: p in LSeg (f,n) ; ::_thesis: Ins (f,n,p) is special
A3: n + 1 <= len f by A2, TOPREAL1:def_3;
then A4: 1 <= (len f) - n by XREAL_1:19;
A5: 1 <= n by A2, TOPREAL1:def_3;
then A6: LSeg (f,n) = LSeg ((f /. n),(f /. (n + 1))) by A3, TOPREAL1:def_3;
set f1 = f | n;
set g1 = (f | n) ^ <*p*>;
set f2 = f /^ n;
set p1 = (f | n) /. (len (f | n));
set p2 = (f /^ n) /. 1;
A7: (f | n) /. (len (f | n)) = |[(((f | n) /. (len (f | n))) `1),(((f | n) /. (len (f | n))) `2)]| by EUCLID:53;
A8: n <= n + 1 by NAT_1:11;
then n <= len f by A3, XXREAL_0:2;
then 1 <= len (f /^ n) by A4, RFINSEQ:def_1;
then 1 in dom (f /^ n) by FINSEQ_3:25;
then A9: f /. (n + 1) = (f /^ n) /. 1 by FINSEQ_5:27;
A10: len (f | n) = n by A3, A8, FINSEQ_1:59, XXREAL_0:2;
then n in dom (f | n) by A5, FINSEQ_3:25;
then A11: f /. n = (f | n) /. (len (f | n)) by A10, FINSEQ_4:70;
then A12: ( ((f | n) /. (len (f | n))) `1 = ((f /^ n) /. 1) `1 or ((f | n) /. (len (f | n))) `2 = ((f /^ n) /. 1) `2 ) by A1, A5, A3, A9, TOPREAL1:def_5;
set q1 = ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>));
A13: (f /^ n) /. 1 = |[(((f /^ n) /. 1) `1),(((f /^ n) /. 1) `2)]| by EUCLID:53;
<*p*> /. 1 = p by FINSEQ_4:16;
then ( ((f | n) /. (len (f | n))) `1 = (<*p*> /. 1) `1 or ((f | n) /. (len (f | n))) `2 = (<*p*> /. 1) `2 ) by A2, A6, A11, A9, A12, A7, A13, TOPREAL3:11, TOPREAL3:12;
then A14: (f | n) ^ <*p*> is special by A1, Lm13;
((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = ((f | n) ^ <*p*>) /. ((len (f | n)) + 1) by FINSEQ_2:16
.= p by FINSEQ_4:67 ;
then ( (((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))) `1 = ((f /^ n) /. 1) `1 or (((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))) `2 = ((f /^ n) /. 1) `2 ) by A2, A6, A11, A9, A12, A7, A13, TOPREAL3:11, TOPREAL3:12;
then ((f | n) ^ <*p*>) ^ (f /^ n) is special by A1, A14, Lm13;
hence Ins (f,n,p) is special by FINSEQ_5:def_4; ::_thesis: verum
end;
theorem Th42: :: SPPOL_2:42
for f being FinSequence of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. holds
(L~ (f -: q)) /\ (L~ (f :- q)) = {q}
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) st q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. holds
(L~ (f -: q)) /\ (L~ (f :- q)) = {q}
let q be Point of (TOP-REAL 2); ::_thesis: ( q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. implies (L~ (f -: q)) /\ (L~ (f :- q)) = {q} )
assume that
A1: q in rng f and
A2: 1 <> q .. f and
A3: q .. f <> len f and
A4: f is unfolded and
A5: f is s.n.c. ; ::_thesis: (L~ (f -: q)) /\ (L~ (f :- q)) = {q}
A6: (f :- q) /. 1 = q by FINSEQ_5:53;
q .. f <= len f by A1, FINSEQ_4:21;
then q .. f < len f by A3, XXREAL_0:1;
then (q .. f) + 1 <= len f by NAT_1:13;
then A7: 1 <= (len f) - (q .. f) by XREAL_1:19;
len (f :- q) = ((len f) - (q .. f)) + 1 by A1, FINSEQ_5:50;
then 1 + 1 <= len (f :- q) by A7, XREAL_1:6;
then A8: rng (f :- q) c= L~ (f :- q) by Th18;
1 in dom (f :- q) by FINSEQ_5:6;
then A9: q in rng (f :- q) by A6, PARTFUN2:2;
not f -: q is empty by A1, FINSEQ_5:47;
then A10: len (f -: q) in dom (f -: q) by FINSEQ_5:6;
A11: len (f -: q) = q .. f by A1, FINSEQ_5:42;
thus (L~ (f -: q)) /\ (L~ (f :- q)) c= {q} :: according to XBOOLE_0:def_10 ::_thesis: {q} c= (L~ (f -: q)) /\ (L~ (f :- q))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (L~ (f -: q)) /\ (L~ (f :- q)) or x in {q} )
assume A12: x in (L~ (f -: q)) /\ (L~ (f :- q)) ; ::_thesis: x in {q}
then reconsider p = x as Point of (TOP-REAL 2) ;
p in L~ (f -: q) by A12, XBOOLE_0:def_4;
then consider i being Element of NAT such that
A13: 1 <= i and
A14: i + 1 <= len (f -: q) and
A15: p in LSeg ((f -: q),i) by Th13;
A16: LSeg ((f -: q),i) = LSeg (f,i) by A14, Th9;
p in L~ (f :- q) by A12, XBOOLE_0:def_4;
then consider j being Element of NAT such that
A17: 1 <= j and
j + 1 <= len (f :- q) and
A18: p in LSeg ((f :- q),j) by Th13;
consider j9 being Nat such that
A19: j = j9 + 1 by A17, NAT_1:6;
reconsider j9 = j9 as Element of NAT by ORDINAL1:def_12;
A20: LSeg ((f :- q),j) = LSeg (f,(j9 + (q .. f))) by A1, A19, Th10;
percases ( ( i + 1 = len (f -: q) & j9 = 0 ) or ( i + 1 = len (f -: q) & j9 <> 0 ) or i + 1 <> len (f -: q) ) ;
supposethat A21: i + 1 = len (f -: q) and
A22: j9 = 0 ; ::_thesis: x in {q}
q .. f <= len f by A1, FINSEQ_4:21;
then q .. f < len f by A3, XXREAL_0:1;
then (i + 1) + 1 <= len f by A11, A21, NAT_1:13;
then i + (1 + 1) <= len f ;
then (LSeg ((f -: q),i)) /\ (LSeg ((f :- q),j)) = {(f /. (q .. f))} by A4, A11, A13, A16, A20, A21, A22, TOPREAL1:def_6
.= {q} by A1, FINSEQ_5:38 ;
hence x in {q} by A15, A18, XBOOLE_0:def_4; ::_thesis: verum
end;
supposethat A23: i + 1 = len (f -: q) and
A24: j9 <> 0 ; ::_thesis: x in {q}
1 <= j9 by A24, NAT_1:14;
then (i + 1) + 1 <= j9 + (q .. f) by A11, A23, XREAL_1:7;
then i + 1 < j9 + (q .. f) by NAT_1:13;
then LSeg ((f -: q),i) misses LSeg ((f :- q),j) by A5, A16, A20, TOPREAL1:def_7;
then (LSeg ((f -: q),i)) /\ (LSeg ((f :- q),j)) = {} by XBOOLE_0:def_7;
hence x in {q} by A15, A18, XBOOLE_0:def_4; ::_thesis: verum
end;
supposeA25: i + 1 <> len (f -: q) ; ::_thesis: x in {q}
A26: q .. f <= j9 + (q .. f) by NAT_1:11;
i + 1 < q .. f by A11, A14, A25, XXREAL_0:1;
then i + 1 < j9 + (q .. f) by A26, XXREAL_0:2;
then LSeg ((f -: q),i) misses LSeg ((f :- q),j) by A5, A16, A20, TOPREAL1:def_7;
then (LSeg ((f -: q),i)) /\ (LSeg ((f :- q),j)) = {} by XBOOLE_0:def_7;
hence x in {q} by A15, A18, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
1 <= q .. f by A1, FINSEQ_4:21;
then 1 < q .. f by A2, XXREAL_0:1;
then 1 + 1 <= q .. f by NAT_1:13;
then A27: rng (f -: q) c= L~ (f -: q) by A11, Th18;
(f -: q) /. (q .. f) = q by A1, FINSEQ_5:45;
then q in rng (f -: q) by A11, A10, PARTFUN2:2;
then q in (L~ (f -: q)) /\ (L~ (f :- q)) by A27, A9, A8, XBOOLE_0:def_4;
hence {q} c= (L~ (f -: q)) /\ (L~ (f :- q)) by ZFMISC_1:31; ::_thesis: verum
end;
theorem Th43: :: SPPOL_2:43
for p, q being Point of (TOP-REAL 2) st p <> q & ( p `1 = q `1 or p `2 = q `2 ) holds
<*p,q*> is being_S-Seq
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q & ( p `1 = q `1 or p `2 = q `2 ) implies <*p,q*> is being_S-Seq )
assume that
A1: p <> q and
A2: ( p `1 = q `1 or p `2 = q `2 ) ; ::_thesis: <*p,q*> is being_S-Seq
set f = <*p,q*>;
thus <*p,q*> is one-to-one by A1, FINSEQ_3:94; :: according to TOPREAL1:def_8 ::_thesis: ( 2 <= len <*p,q*> & <*p,q*> is unfolded & <*p,q*> is s.n.c. & <*p,q*> is special )
thus len <*p,q*> >= 2 by FINSEQ_1:44; ::_thesis: ( <*p,q*> is unfolded & <*p,q*> is s.n.c. & <*p,q*> is special )
thus ( <*p,q*> is unfolded & <*p,q*> is s.n.c. & <*p,q*> is special ) by A2, Lm2, Lm6, Th38; ::_thesis: verum
end;
definition
mode S-Sequence_in_R2 is being_S-Seq FinSequence of (TOP-REAL 2);
end;
registration
let f be S-Sequence_in_R2;
cluster Rev f -> being_S-Seq for FinSequence of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 = Rev f holds
b1 is being_S-Seq
proof
set g = Rev f;
Rev f is being_S-Seq
proof
thus Rev f is one-to-one ; :: according to TOPREAL1:def_8 ::_thesis: ( 2 <= len (Rev f) & Rev f is unfolded & Rev f is s.n.c. & Rev f is special )
len (Rev f) = len f by FINSEQ_5:def_3;
hence len (Rev f) >= 2 by TOPREAL1:def_8; ::_thesis: ( Rev f is unfolded & Rev f is s.n.c. & Rev f is special )
thus ( Rev f is unfolded & Rev f is s.n.c. & Rev f is special ) by Th28, Th35, Th40; ::_thesis: verum
end;
hence for b1 being FinSequence of (TOP-REAL 2) st b1 = Rev f holds
b1 is being_S-Seq ; ::_thesis: verum
end;
end;
theorem :: SPPOL_2:44
for i being Element of NAT
for f being S-Sequence_in_R2 st i in dom f holds
f /. i in L~ f
proof
let i be Element of NAT ; ::_thesis: for f being S-Sequence_in_R2 st i in dom f holds
f /. i in L~ f
let f be S-Sequence_in_R2; ::_thesis: ( i in dom f implies f /. i in L~ f )
len f >= 2 by TOPREAL1:def_8;
hence ( i in dom f implies f /. i in L~ f ) by GOBOARD1:1; ::_thesis: verum
end;
theorem :: SPPOL_2:45
for p, q being Point of (TOP-REAL 2) st p <> q & ( p `1 = q `1 or p `2 = q `2 ) holds
LSeg (p,q) is being_S-P_arc
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q & ( p `1 = q `1 or p `2 = q `2 ) implies LSeg (p,q) is being_S-P_arc )
assume that
A1: p <> q and
A2: ( p `1 = q `1 or p `2 = q `2 ) ; ::_thesis: LSeg (p,q) is being_S-P_arc
take f = <*p,q*>; :: according to TOPREAL1:def_9 ::_thesis: ( f is being_S-Seq & LSeg (p,q) = L~ f )
thus f is being_S-Seq by A1, A2, Th43; ::_thesis: LSeg (p,q) = L~ f
thus LSeg (p,q) = L~ f by Th21; ::_thesis: verum
end;
Lm14: for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in rng f holds
L~ (f -: p) c= L~ f
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in rng f holds
L~ (f -: p) c= L~ f
let p be Point of (TOP-REAL 2); ::_thesis: ( p in rng f implies L~ (f -: p) c= L~ f )
assume p in rng f ; ::_thesis: L~ (f -: p) c= L~ f
then L~ f = (L~ (f -: p)) \/ (L~ (f :- p)) by Th24;
hence L~ (f -: p) c= L~ f by XBOOLE_1:7; ::_thesis: verum
end;
Lm15: for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in rng f holds
L~ (f :- p) c= L~ f
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in rng f holds
L~ (f :- p) c= L~ f
let p be Point of (TOP-REAL 2); ::_thesis: ( p in rng f implies L~ (f :- p) c= L~ f )
assume p in rng f ; ::_thesis: L~ (f :- p) c= L~ f
then L~ f = (L~ (f -: p)) \/ (L~ (f :- p)) by Th24;
hence L~ (f :- p) c= L~ f by XBOOLE_1:7; ::_thesis: verum
end;
theorem Th46: :: SPPOL_2:46
for p being Point of (TOP-REAL 2)
for f being S-Sequence_in_R2 st p in rng f & p .. f <> 1 holds
f -: p is being_S-Seq
proof
let p be Point of (TOP-REAL 2); ::_thesis: for f being S-Sequence_in_R2 st p in rng f & p .. f <> 1 holds
f -: p is being_S-Seq
let f be S-Sequence_in_R2; ::_thesis: ( p in rng f & p .. f <> 1 implies f -: p is being_S-Seq )
assume that
A1: p in rng f and
A2: p .. f <> 1 ; ::_thesis: f -: p is being_S-Seq
thus f -: p is one-to-one ; :: according to TOPREAL1:def_8 ::_thesis: ( 2 <= len (f -: p) & f -: p is unfolded & f -: p is s.n.c. & f -: p is special )
1 <= p .. f by A1, FINSEQ_4:21;
then 1 < p .. f by A2, XXREAL_0:1;
then 1 + 1 <= p .. f by NAT_1:13;
hence len (f -: p) >= 2 by A1, FINSEQ_5:42; ::_thesis: ( f -: p is unfolded & f -: p is s.n.c. & f -: p is special )
thus ( f -: p is unfolded & f -: p is s.n.c. & f -: p is special ) ; ::_thesis: verum
end;
theorem :: SPPOL_2:47
for p being Point of (TOP-REAL 2)
for f being S-Sequence_in_R2 st p in rng f & p .. f <> len f holds
f :- p is being_S-Seq
proof
let p be Point of (TOP-REAL 2); ::_thesis: for f being S-Sequence_in_R2 st p in rng f & p .. f <> len f holds
f :- p is being_S-Seq
let f be S-Sequence_in_R2; ::_thesis: ( p in rng f & p .. f <> len f implies f :- p is being_S-Seq )
assume that
A1: p in rng f and
A2: p .. f <> len f ; ::_thesis: f :- p is being_S-Seq
thus f :- p is one-to-one by A1, FINSEQ_5:56; :: according to TOPREAL1:def_8 ::_thesis: ( 2 <= len (f :- p) & f :- p is unfolded & f :- p is s.n.c. & f :- p is special )
hereby ::_thesis: ( f :- p is unfolded & f :- p is s.n.c. & f :- p is special )
p .. f <= len f by A1, FINSEQ_4:21;
then p .. f < len f by A2, XXREAL_0:1;
then 1 + (p .. f) <= len f by NAT_1:13;
then A3: (len f) - (p .. f) >= 1 by XREAL_1:19;
assume len (f :- p) < 2 ; ::_thesis: contradiction
then ((len f) - (p .. f)) + 1 < 1 + 1 by A1, FINSEQ_5:50;
hence contradiction by A3, XREAL_1:6; ::_thesis: verum
end;
thus ( f :- p is unfolded & f :- p is s.n.c. & f :- p is special ) by A1, Th27, Th34, Th39; ::_thesis: verum
end;
theorem Th48: :: SPPOL_2:48
for p being Point of (TOP-REAL 2)
for i being Element of NAT
for f being S-Sequence_in_R2 st p in LSeg (f,i) & not p in rng f holds
Ins (f,i,p) is being_S-Seq
proof
let p be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT
for f being S-Sequence_in_R2 st p in LSeg (f,i) & not p in rng f holds
Ins (f,i,p) is being_S-Seq
let i be Element of NAT ; ::_thesis: for f being S-Sequence_in_R2 st p in LSeg (f,i) & not p in rng f holds
Ins (f,i,p) is being_S-Seq
let f be S-Sequence_in_R2; ::_thesis: ( p in LSeg (f,i) & not p in rng f implies Ins (f,i,p) is being_S-Seq )
assume that
A1: p in LSeg (f,i) and
A2: not p in rng f ; ::_thesis: Ins (f,i,p) is being_S-Seq
set g = Ins (f,i,p);
thus Ins (f,i,p) is one-to-one by A2, FINSEQ_5:76; :: according to TOPREAL1:def_8 ::_thesis: ( 2 <= len (Ins (f,i,p)) & Ins (f,i,p) is unfolded & Ins (f,i,p) is s.n.c. & Ins (f,i,p) is special )
len (Ins (f,i,p)) = (len f) + 1 by FINSEQ_5:69;
then A3: len (Ins (f,i,p)) >= len f by NAT_1:11;
len f >= 2 by TOPREAL1:def_8;
hence len (Ins (f,i,p)) >= 2 by A3, XXREAL_0:2; ::_thesis: ( Ins (f,i,p) is unfolded & Ins (f,i,p) is s.n.c. & Ins (f,i,p) is special )
thus Ins (f,i,p) is unfolded by A1, Th32; ::_thesis: ( Ins (f,i,p) is s.n.c. & Ins (f,i,p) is special )
thus Ins (f,i,p) is s.n.c. by A1, A2, Th37; ::_thesis: Ins (f,i,p) is special
thus Ins (f,i,p) is special by A1, Th41; ::_thesis: verum
end;
begin
registration
cluster being_S-P_arc for Element of bool the carrier of (TOP-REAL 2);
existence
ex b1 being Subset of (TOP-REAL 2) st b1 is being_S-P_arc
proof
set p = |[0,0]|;
set q = |[1,1]|;
set f = <*|[0,0]|,|[(|[0,0]| `1),(|[1,1]| `2)]|,|[1,1]|*>;
A1: |[0,0]| `2 = 0 by EUCLID:52;
A2: |[1,1]| `1 = 1 by EUCLID:52;
A3: |[1,1]| `2 = 1 by EUCLID:52;
|[0,0]| `1 = 0 by EUCLID:52;
then <*|[0,0]|,|[(|[0,0]| `1),(|[1,1]| `2)]|,|[1,1]|*> is being_S-Seq by A1, A2, A3, TOPREAL3:34;
then L~ <*|[0,0]|,|[(|[0,0]| `1),(|[1,1]| `2)]|,|[1,1]|*> is being_S-P_arc by TOPREAL1:def_9;
hence ex b1 being Subset of (TOP-REAL 2) st b1 is being_S-P_arc ; ::_thesis: verum
end;
end;
theorem :: SPPOL_2:49
for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_S-P_arc_joining p1,p2 holds
P is_S-P_arc_joining p2,p1
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_S-P_arc_joining p1,p2 holds
P is_S-P_arc_joining p2,p1
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_S-P_arc_joining p1,p2 implies P is_S-P_arc_joining p2,p1 )
given f being FinSequence of (TOP-REAL 2) such that A1: f is being_S-Seq and
A2: P = L~ f and
A3: p1 = f /. 1 and
A4: p2 = f /. (len f) ; :: according to TOPREAL4:def_1 ::_thesis: P is_S-P_arc_joining p2,p1
take g = Rev f; :: according to TOPREAL4:def_1 ::_thesis: ( g is being_S-Seq & P = L~ g & p2 = g /. 1 & p1 = g /. (len g) )
thus ( g is being_S-Seq & P = L~ g ) by A1, A2, Th22; ::_thesis: ( p2 = g /. 1 & p1 = g /. (len g) )
len g = len f by FINSEQ_5:def_3;
hence ( p2 = g /. 1 & p1 = g /. (len g) ) by A1, A3, A4, FINSEQ_5:65; ::_thesis: verum
end;
definition
let p1, p2 be Point of (TOP-REAL 2);
let P be Subset of (TOP-REAL 2);
predp1,p2 split P means :Def1: :: SPPOL_2:def 1
( p1 <> p2 & ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) ) );
end;
:: deftheorem Def1 defines split SPPOL_2:def_1_:_
for p1, p2 being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) holds
( p1,p2 split P iff ( p1 <> p2 & ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) ) ) );
theorem Th50: :: SPPOL_2:50
for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P holds
p2,p1 split P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P holds
p2,p1 split P
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1,p2 split P implies p2,p1 split P )
assume A1: p1 <> p2 ; :: according to SPPOL_2:def_1 ::_thesis: ( for f1, f2 being S-Sequence_in_R2 holds
( not p1 = f1 /. 1 or not p1 = f2 /. 1 or not p2 = f1 /. (len f1) or not p2 = f2 /. (len f2) or not (L~ f1) /\ (L~ f2) = {p1,p2} or not P = (L~ f1) \/ (L~ f2) ) or p2,p1 split P )
given f1, f2 being S-Sequence_in_R2 such that A2: p1 = f1 /. 1 and
A3: p1 = f2 /. 1 and
A4: p2 = f1 /. (len f1) and
A5: p2 = f2 /. (len f2) and
A6: (L~ f1) /\ (L~ f2) = {p1,p2} and
A7: P = (L~ f1) \/ (L~ f2) ; ::_thesis: p2,p1 split P
thus p2 <> p1 by A1; :: according to SPPOL_2:def_1 ::_thesis: ex f1, f2 being S-Sequence_in_R2 st
( p2 = f1 /. 1 & p2 = f2 /. 1 & p1 = f1 /. (len f1) & p1 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p2,p1} & P = (L~ f1) \/ (L~ f2) )
reconsider g1 = Rev f1, g2 = Rev f2 as S-Sequence_in_R2 ;
take g1 ; ::_thesis: ex f2 being S-Sequence_in_R2 st
( p2 = g1 /. 1 & p2 = f2 /. 1 & p1 = g1 /. (len g1) & p1 = f2 /. (len f2) & (L~ g1) /\ (L~ f2) = {p2,p1} & P = (L~ g1) \/ (L~ f2) )
take g2 ; ::_thesis: ( p2 = g1 /. 1 & p2 = g2 /. 1 & p1 = g1 /. (len g1) & p1 = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p2,p1} & P = (L~ g1) \/ (L~ g2) )
A8: len g2 = len f2 by FINSEQ_5:def_3;
len g1 = len f1 by FINSEQ_5:def_3;
hence ( p2 = g1 /. 1 & p2 = g2 /. 1 & p1 = g1 /. (len g1) & p1 = g2 /. (len g2) ) by A2, A3, A4, A5, A8, FINSEQ_5:65; ::_thesis: ( (L~ g1) /\ (L~ g2) = {p2,p1} & P = (L~ g1) \/ (L~ g2) )
L~ g1 = L~ f1 by Th22;
hence ( (L~ g1) /\ (L~ g2) = {p2,p1} & P = (L~ g1) \/ (L~ g2) ) by A6, A7, Th22; ::_thesis: verum
end;
Lm16: for P being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2)
for f1, f2 being S-Sequence_in_R2 st p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) & q <> p1 & q in rng f1 holds
ex g1, g2 being S-Sequence_in_R2 st
( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2)
for f1, f2 being S-Sequence_in_R2 st p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) & q <> p1 & q in rng f1 holds
ex g1, g2 being S-Sequence_in_R2 st
( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )
let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: for f1, f2 being S-Sequence_in_R2 st p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) & q <> p1 & q in rng f1 holds
ex g1, g2 being S-Sequence_in_R2 st
( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )
let f1, f2 be S-Sequence_in_R2; ::_thesis: ( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) & q <> p1 & q in rng f1 implies ex g1, g2 being S-Sequence_in_R2 st
( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) ) )
assume that
A1: p1 = f1 /. 1 and
A2: p1 = f2 /. 1 and
A3: p2 = f1 /. (len f1) and
A4: p2 = f2 /. (len f2) and
A5: (L~ f1) /\ (L~ f2) = {p1,p2} and
A6: P = (L~ f1) \/ (L~ f2) and
A7: q <> p1 and
A8: q in rng f1 ; ::_thesis: ex g1, g2 being S-Sequence_in_R2 st
( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )
set f19 = Rev (f1 :- q);
A9: 1 <= q .. f1 by A8, FINSEQ_4:21;
A10: now__::_thesis:_not_1_=_q_.._f1
assume A11: 1 = q .. f1 ; ::_thesis: contradiction
then A12: 1 in dom f1 by A8, FINSEQ_4:20;
f1 . 1 = q by A8, A11, FINSEQ_4:19;
hence contradiction by A1, A7, A12, PARTFUN1:def_6; ::_thesis: verum
end;
then reconsider g1 = f1 -: q as S-Sequence_in_R2 by A8, Th46;
A13: 1 in dom g1 by FINSEQ_5:6;
1 in dom f2 by FINSEQ_5:6;
then 1 <= len f2 by FINSEQ_3:25;
then reconsider l = (len f2) - 1 as Element of NAT by INT_1:5;
set f29 = f2 | l;
A14: l + 1 = len f2 ;
rng (Rev (f1 :- q)) = rng (f1 :- q) by FINSEQ_5:57;
then A15: rng (Rev (f1 :- q)) c= rng f1 by A8, FINSEQ_5:55;
len f2 >= 2 by TOPREAL1:def_8;
then A16: rng f2 c= L~ f2 by Th18;
len f1 >= 2 by TOPREAL1:def_8;
then rng f1 c= L~ f1 by Th18;
then A17: (rng f2) /\ (rng f1) c= (L~ f1) /\ (L~ f2) by A16, XBOOLE_1:27;
set g2 = (f2 | l) ^ (Rev (f1 :- q));
A18: dom (f2 | l) = Seg (len (f2 | l)) by FINSEQ_1:def_3;
len (f1 :- q) >= 1 by NAT_1:14;
then A19: len (Rev (f1 :- q)) >= 1 by FINSEQ_5:def_3;
then A20: len (Rev (f1 :- q)) in dom (Rev (f1 :- q)) by FINSEQ_3:25;
A21: l < len f2 by XREAL_1:44;
then A22: len (f2 | l) = l by FINSEQ_1:59;
len f2 >= 2 by TOPREAL1:def_8;
then A23: (len f2) - 1 >= (1 + 1) - 1 by XREAL_1:9;
then A24: l in dom (f2 | l) by A22, FINSEQ_3:25;
then A25: (f2 | l) /. (len (f2 | l)) = f2 /. l by A22, FINSEQ_4:70;
A26: (Rev (f1 :- q)) /. 1 = (f1 :- q) /. (len (f1 :- q)) by FINSEQ_5:65
.= f2 /. (len f2) by A3, A4, A8, FINSEQ_5:54 ;
then A27: LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) = LSeg (f2,l) by A23, A14, A25, TOPREAL1:def_3;
A28: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_+_2_<=_len_(f2_|_l)_holds_
LSeg_((f2_|_l),i)_misses_LSeg_(((f2_|_l)_/._(len_(f2_|_l))),((Rev_(f1_:-_q))_/._1))
let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 2 <= len (f2 | l) implies LSeg ((f2 | l),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) )
assume that
1 <= i and
A29: i + 2 <= len (f2 | l) ; ::_thesis: LSeg ((f2 | l),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))
(i + 1) + 1 <= len (f2 | l) by A29;
then A30: i + 1 < len (f2 | l) by NAT_1:13;
then LSeg ((f2 | l),i) = LSeg (f2,i) by Th3;
hence LSeg ((f2 | l),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) by A22, A27, A30, TOPREAL1:def_7; ::_thesis: verum
end;
A31: 1 in dom f1 by FINSEQ_5:6;
A32: now__::_thesis:_not_p1_in_L~_(Rev_(f1_:-_q))
A33: 1 + 1 <= len f1 by TOPREAL1:def_8;
p1 in LSeg ((f1 /. 1),(f1 /. (1 + 1))) by A1, RLTOPSP1:68;
then A34: p1 in LSeg (f1,1) by A33, TOPREAL1:def_3;
assume p1 in L~ (Rev (f1 :- q)) ; ::_thesis: contradiction
then A35: p1 in L~ (f1 :- q) by Th22;
then consider i being Element of NAT such that
A36: 1 <= i and
i + 1 <= len (f1 :- q) and
A37: p1 in LSeg ((f1 :- q),i) by Th13;
consider j being Nat such that
A38: i = j + 1 by A36, NAT_1:6;
A39: 1 < q .. f1 by A10, A9, XXREAL_0:1;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A40: LSeg ((f1 :- q),i) = LSeg (f1,(j + (q .. f1))) by A8, A38, Th10;
then p1 in (LSeg (f1,1)) /\ (LSeg (f1,(j + (q .. f1)))) by A37, A34, XBOOLE_0:def_4;
then A41: LSeg (f1,1) meets LSeg (f1,(j + (q .. f1))) by XBOOLE_0:4;
percases ( j = 0 or j <> 0 ) ;
supposeA42: j = 0 ; ::_thesis: contradiction
A43: 1 + 1 <= q .. f1 by A39, NAT_1:13;
now__::_thesis:_contradiction
percases ( q .. f1 = 2 or q .. f1 > 2 ) by A43, XXREAL_0:1;
supposeA44: q .. f1 = 2 ; ::_thesis: contradiction
A45: q .. f1 <= len f1 by A8, FINSEQ_4:21;
now__::_thesis:_contradiction
percases ( len f1 = 2 or len f1 > 2 ) by A44, A45, XXREAL_0:1;
suppose len f1 = 2 ; ::_thesis: contradiction
then len (f1 :- q) = ((len f1) - (len f1)) + 1 by A8, A44, FINSEQ_5:50;
hence contradiction by A35, TOPREAL1:22; ::_thesis: verum
end;
suppose len f1 > 2 ; ::_thesis: contradiction
then 1 + 2 <= len f1 by NAT_1:13;
then (LSeg (f1,1)) /\ (LSeg (f1,(1 + 1))) = {(f1 /. (1 + 1))} by TOPREAL1:def_6;
then p1 in {(f1 /. 2)} by A37, A34, A40, A42, A44, XBOOLE_0:def_4;
then A46: p1 = f1 /. 2 by TARSKI:def_1;
2 in dom f1 by A8, A44, FINSEQ_4:20;
hence contradiction by A1, A31, A46, PARTFUN2:10; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
suppose q .. f1 > 2 ; ::_thesis: contradiction
then 1 + 1 < j + (q .. f1) by A42;
hence contradiction by A41, TOPREAL1:def_7; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
suppose j <> 0 ; ::_thesis: contradiction
then 1 + 1 < j + (q .. f1) by A39, NAT_1:14, XREAL_1:8;
hence contradiction by A41, TOPREAL1:def_7; ::_thesis: verum
end;
end;
end;
A47: now__::_thesis:_for_i_being_Element_of_NAT_st_2_<=_i_&_i_+_1_<=_len_(Rev_(f1_:-_q))_holds_
LSeg_((Rev_(f1_:-_q)),i)_misses_LSeg_(((f2_|_l)_/._(len_(f2_|_l))),((Rev_(f1_:-_q))_/._1))
let i be Element of NAT ; ::_thesis: ( 2 <= i & i + 1 <= len (Rev (f1 :- q)) implies LSeg ((Rev (f1 :- q)),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) )
assume that
A48: 2 <= i and
A49: i + 1 <= len (Rev (f1 :- q)) ; ::_thesis: LSeg ((Rev (f1 :- q)),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))
reconsider m = (len (Rev (f1 :- q))) - (i + 1) as Element of NAT by A49, INT_1:5;
(m + 1) + i = len (f1 :- q) by FINSEQ_5:def_3;
then A50: LSeg ((Rev (f1 :- q)),i) = LSeg ((f1 :- q),(m + 1)) by Th2
.= LSeg (f1,(m + (q .. f1))) by A8, Th10 ;
then A51: LSeg ((Rev (f1 :- q)),i) c= L~ f1 by TOPREAL3:19;
A52: now__::_thesis:_not_p2_in_LSeg_((Rev_(f1_:-_q)),i)
A53: len f1 >= 1 + 1 by TOPREAL1:def_8;
then reconsider k = (len f1) - 1 as Element of NAT by INT_1:5, XXREAL_0:2;
A54: p2 in LSeg ((f1 /. k),(f1 /. (len f1))) by A3, RLTOPSP1:68;
A55: k + 1 = len f1 ;
then 1 <= k by A53, XREAL_1:6;
then A56: p2 in LSeg (f1,k) by A55, A54, TOPREAL1:def_3;
A57: len (Rev (f1 :- q)) = len (f1 :- q) by FINSEQ_5:def_3;
A58: (len f1) - i = (((((len f1) - (q .. f1)) + 1) - 1) + (q .. f1)) - i
.= (((len (Rev (f1 :- q))) - 1) + (q .. f1)) - i by A8, A57, FINSEQ_5:50
.= m + (q .. f1) ;
percases ( i = 1 + 1 or i <> 2 ) ;
supposeA59: i = 1 + 1 ; ::_thesis: not p2 in LSeg ((Rev (f1 :- q)),i)
A60: q .. f1 <= m + (q .. f1) by NAT_1:11;
1 <= q .. f1 by A8, FINSEQ_4:21;
then A61: 1 <= m + (q .. f1) by A60, XXREAL_0:2;
assume A62: p2 in LSeg ((Rev (f1 :- q)),i) ; ::_thesis: contradiction
A63: (m + (q .. f1)) + (1 + 1) = len f1 by A58, A59;
A64: 1 <= k by A53, XREAL_1:19;
p2 in LSeg ((f1 /. k),(f1 /. (k + 1))) by A3, RLTOPSP1:68;
then A65: p2 in LSeg (f1,k) by A64, TOPREAL1:def_3;
(m + (q .. f1)) + 1 = k by A58, A59;
then (LSeg (f1,(m + (q .. f1)))) /\ (LSeg (f1,k)) = {(f1 /. k)} by A61, A63, TOPREAL1:def_6;
then p2 in {(f1 /. k)} by A50, A65, A62, XBOOLE_0:def_4;
then A66: f1 /. (len f1) = f1 /. k by A3, TARSKI:def_1;
k <= len f1 by A55, NAT_1:11;
then A67: k in dom f1 by A64, FINSEQ_3:25;
len f1 in dom f1 by FINSEQ_5:6;
then (len f1) - k = (len f1) - (len f1) by A67, A66, PARTFUN2:10
.= 0 ;
hence contradiction ; ::_thesis: verum
end;
suppose i <> 2 ; ::_thesis: not p2 in LSeg ((Rev (f1 :- q)),i)
then 2 < i by A48, XXREAL_0:1;
then 2 + 1 <= i by NAT_1:13;
then (len f1) - i <= (len f1) - (1 + 2) by XREAL_1:10;
then (len f1) - i <= ((len f1) - 1) - 2 ;
then A68: ((len f1) - i) + (1 + 1) <= k by XREAL_1:19;
((len f1) - i) + (1 + 1) = ((m + (q .. f1)) + 1) + 1 by A58;
then (m + (q .. f1)) + 1 < k by A68, NAT_1:13;
then LSeg (f1,k) misses LSeg (f1,(m + (q .. f1))) by TOPREAL1:def_7;
then (LSeg (f1,k)) /\ (LSeg (f1,(m + (q .. f1)))) = {} by XBOOLE_0:def_7;
hence not p2 in LSeg ((Rev (f1 :- q)),i) by A50, A56, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
LSeg ((Rev (f1 :- q)),i) c= L~ (Rev (f1 :- q)) by TOPREAL3:19;
then A69: not p1 in LSeg ((Rev (f1 :- q)),i) by A32;
LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) c= L~ f2 by A27, TOPREAL3:19;
then A70: (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),i)) c= {p1,p2} by A5, A51, XBOOLE_1:27;
now__::_thesis:_for_x_being_set_holds_not_x_in_(LSeg_(((f2_|_l)_/._(len_(f2_|_l))),((Rev_(f1_:-_q))_/._1)))_/\_(LSeg_((Rev_(f1_:-_q)),i))
given x being set such that A71: x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),i)) ; ::_thesis: contradiction
( x = p1 or x = p2 ) by A70, A71, TARSKI:def_2;
hence contradiction by A69, A52, A71, XBOOLE_0:def_4; ::_thesis: verum
end;
then (LSeg ((Rev (f1 :- q)),i)) /\ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) = {} by XBOOLE_0:def_1;
hence LSeg ((Rev (f1 :- q)),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) by XBOOLE_0:def_7; ::_thesis: verum
end;
A72: now__::_thesis:_(_len_(Rev_(f1_:-_q))_<>_1_implies_(LSeg_(((f2_|_l)_/._(len_(f2_|_l))),((Rev_(f1_:-_q))_/._1)))_/\_(LSeg_((Rev_(f1_:-_q)),1))_=_{((Rev_(f1_:-_q))_/._1)}_)
assume len (Rev (f1 :- q)) <> 1 ; ::_thesis: (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) = {((Rev (f1 :- q)) /. 1)}
then 1 < len (Rev (f1 :- q)) by A19, XXREAL_0:1;
then A73: 1 + 1 <= len (Rev (f1 :- q)) by NAT_1:13;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(LSeg_(((f2_|_l)_/._(len_(f2_|_l))),((Rev_(f1_:-_q))_/._1)))_/\_(LSeg_((Rev_(f1_:-_q)),1))_implies_x_=_(Rev_(f1_:-_q))_/._1_)_&_(_x_=_(Rev_(f1_:-_q))_/._1_implies_x_in_(LSeg_(((f2_|_l)_/._(len_(f2_|_l))),((Rev_(f1_:-_q))_/._1)))_/\_(LSeg_((Rev_(f1_:-_q)),1))_)_)
let x be set ; ::_thesis: ( ( x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) implies x = (Rev (f1 :- q)) /. 1 ) & ( x = (Rev (f1 :- q)) /. 1 implies x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) ) )
hereby ::_thesis: ( x = (Rev (f1 :- q)) /. 1 implies x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) )
reconsider m = (len (Rev (f1 :- q))) - 2 as Element of NAT by A73, INT_1:5;
LSeg ((Rev (f1 :- q)),1) c= L~ (Rev (f1 :- q)) by TOPREAL3:19;
then not p1 in LSeg ((Rev (f1 :- q)),1) by A32;
then A74: not p1 in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) by XBOOLE_0:def_4;
(m + 1) + 1 = len (f1 :- q) by FINSEQ_5:def_3;
then LSeg ((Rev (f1 :- q)),1) = LSeg ((f1 :- q),(m + 1)) by Th2
.= LSeg (f1,(m + (q .. f1))) by A8, Th10 ;
then A75: LSeg ((Rev (f1 :- q)),1) c= L~ f1 by TOPREAL3:19;
LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) c= L~ f2 by A27, TOPREAL3:19;
then A76: (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) c= {p1,p2} by A5, A75, XBOOLE_1:27;
assume x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) ; ::_thesis: x = (Rev (f1 :- q)) /. 1
hence x = (Rev (f1 :- q)) /. 1 by A4, A26, A76, A74, TARSKI:def_2; ::_thesis: verum
end;
assume A77: x = (Rev (f1 :- q)) /. 1 ; ::_thesis: x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1))
then x in LSeg (((Rev (f1 :- q)) /. 1),((Rev (f1 :- q)) /. (1 + 1))) by RLTOPSP1:68;
then A78: x in LSeg ((Rev (f1 :- q)),1) by A73, TOPREAL1:def_3;
x in LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) by A77, RLTOPSP1:68;
hence x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) by A78, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) = {((Rev (f1 :- q)) /. 1)} by TARSKI:def_1; ::_thesis: verum
end;
A79: len (f2 | l) >= 1 by A21, A23, FINSEQ_1:59;
then A80: not f2 | l is empty ;
f1 :- q is unfolded by A8, Th27;
then A81: Rev (f1 :- q) is unfolded by Th28;
A82: now__::_thesis:_(f2_|_l)_^_(Rev_(f1_:-_q))_is_unfolded
percases ( ( len (f2 | l) = 1 & len (Rev (f1 :- q)) = 1 ) or ( len (f2 | l) <> 1 & len (Rev (f1 :- q)) = 1 ) or ( len (f2 | l) = 1 & len (Rev (f1 :- q)) <> 1 ) or ( len (f2 | l) <> 1 & len (Rev (f1 :- q)) <> 1 ) ) ;
suppose ( len (f2 | l) = 1 & len (Rev (f1 :- q)) = 1 ) ; ::_thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded
then len ((f2 | l) ^ (Rev (f1 :- q))) = 1 + 1 by FINSEQ_1:22;
hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by Th26; ::_thesis: verum
end;
supposethat A83: len (f2 | l) <> 1 and
A84: len (Rev (f1 :- q)) = 1 ; ::_thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded
consider k being Nat such that
A85: k + 1 = len (f2 | l) by A79, NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A86: LSeg ((f2 | l),k) = LSeg (f2,k) by A85, Th3;
len (f2 | l) > 1 by A22, A23, A83, XXREAL_0:1;
then A87: 1 <= k by A85, NAT_1:13;
A88: Rev (f1 :- q) = <*((Rev (f1 :- q)) /. 1)*> by A84, FINSEQ_5:14;
k + (1 + 1) <= len f2 by A22, A85;
then (LSeg ((f2 | l),k)) /\ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) = {((f2 | l) /. (len (f2 | l)))} by A22, A25, A27, A85, A87, A86, TOPREAL1:def_6;
hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A85, A88, Th30; ::_thesis: verum
end;
supposethat A89: len (f2 | l) = 1 and
A90: len (Rev (f1 :- q)) <> 1 ; ::_thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded
f2 | l = <*((f2 | l) /. (len (f2 | l)))*> by A89, FINSEQ_5:14;
hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A81, A72, A90, Th29; ::_thesis: verum
end;
supposethat A91: len (f2 | l) <> 1 and
A92: len (Rev (f1 :- q)) <> 1 ; ::_thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded
consider k being Nat such that
A93: k + 1 = len (f2 | l) by A79, NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A94: k + (1 + 1) <= len f2 by A22, A93;
A95: LSeg ((f2 | l),k) = LSeg (f2,k) by A93, Th3;
len (f2 | l) > 1 by A22, A23, A91, XXREAL_0:1;
then 1 <= k by A93, NAT_1:13;
then (LSeg ((f2 | l),k)) /\ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) = {((f2 | l) /. (len (f2 | l)))} by A22, A25, A27, A93, A94, A95, TOPREAL1:def_6;
hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A81, A72, A92, A93, Th31; ::_thesis: verum
end;
end;
end;
len g1 >= 2 by TOPREAL1:def_8;
then A96: rng g1 c= L~ g1 by Th18;
set Z = (rng (f2 | l)) /\ (rng (Rev (f1 :- q)));
A97: 1 in dom (f2 | l) by A22, A23, FINSEQ_3:25;
A98: len f2 in dom f2 by FINSEQ_5:6;
then A99: p2 .. f2 = len f2 by A4, FINSEQ_5:41;
now__::_thesis:_not_p2_in_rng_(f2_|_l)
assume A100: p2 in rng (f2 | l) ; ::_thesis: contradiction
then p2 .. (f2 | l) = p2 .. f2 by FINSEQ_5:40;
hence contradiction by A22, A99, A100, FINSEQ_4:21, XREAL_1:44; ::_thesis: verum
end;
then A101: not p2 in (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) by XBOOLE_0:def_4;
then A102: (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) <> {p1,p2} by TARSKI:def_2;
dom f2 = Seg (len f2) by FINSEQ_1:def_3;
then A103: len (f2 | l) in dom f2 by A22, A14, A24, A18, FINSEQ_2:8;
now__::_thesis:_not_p2_in_L~_(f2_|_l)
p2 in LSeg ((f2 /. (len (f2 | l))),p2) by RLTOPSP1:68;
then A104: p2 in LSeg (f2,(len (f2 | l))) by A4, A22, A23, A14, TOPREAL1:def_3;
assume p2 in L~ (f2 | l) ; ::_thesis: contradiction
then consider i being Element of NAT such that
A105: 1 <= i and
A106: i + 1 <= len (f2 | l) and
A107: p2 in LSeg ((f2 | l),i) by Th13;
LSeg ((f2 | l),i) = LSeg (f2,i) by A106, Th3;
then A108: p2 in (LSeg (f2,i)) /\ (LSeg (f2,(len (f2 | l)))) by A107, A104, XBOOLE_0:def_4;
then A109: LSeg (f2,i) meets LSeg (f2,(len (f2 | l))) by XBOOLE_0:4;
A110: len f2 <> len (f2 | l) by A21, FINSEQ_1:59;
percases ( i + 1 = len (f2 | l) or i + 1 <> len (f2 | l) ) ;
supposeA111: i + 1 = len (f2 | l) ; ::_thesis: contradiction
then i + (1 + 1) = len f2 by A22;
then (LSeg (f2,i)) /\ (LSeg (f2,(len (f2 | l)))) = {(f2 /. (len (f2 | l)))} by A105, A111, TOPREAL1:def_6;
then p2 = f2 /. (len (f2 | l)) by A108, TARSKI:def_1;
hence contradiction by A4, A98, A103, A110, PARTFUN2:10; ::_thesis: verum
end;
suppose i + 1 <> len (f2 | l) ; ::_thesis: contradiction
then i + 1 < len (f2 | l) by A106, XXREAL_0:1;
hence contradiction by A109, TOPREAL1:def_7; ::_thesis: verum
end;
end;
end;
then A112: not p2 in (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) by XBOOLE_0:def_4;
L~ (f1 :- q) c= L~ f1 by A8, Lm15;
then A113: L~ (Rev (f1 :- q)) c= L~ f1 by Th22;
L~ (f2 | l) c= L~ f2 by Lm1;
then (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) c= {p1,p2} by A5, A113, XBOOLE_1:27;
then A114: ( (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {} or (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {p1} or (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {p2} or (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {p1,p2} ) by ZFMISC_1:36;
f1 :- q is special by A8, Th39;
then A115: Rev (f1 :- q) is special by Th40;
A116: 1 in dom (f1 :- q) by FINSEQ_5:6;
now__::_thesis:_not_p1_in_rng_(f1_:-_q)
set l = p1 .. (f1 :- q);
assume A117: p1 in rng (f1 :- q) ; ::_thesis: contradiction
then A118: (f1 :- q) . (p1 .. (f1 :- q)) = p1 by FINSEQ_4:19;
p1 .. (f1 :- q) <> 0 by A117, FINSEQ_4:21;
then consider j being Nat such that
A119: p1 .. (f1 :- q) = j + 1 by NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A120: p1 .. (f1 :- q) in dom (f1 :- q) by A117, FINSEQ_4:20;
then A121: j + (q .. f1) in dom f1 by A8, A119, FINSEQ_5:51;
(f1 :- q) /. (p1 .. (f1 :- q)) = f1 /. (j + (q .. f1)) by A8, A120, A119, FINSEQ_5:52;
then j + (q .. f1) = 1 by A1, A31, A120, A118, A121, PARTFUN1:def_6, PARTFUN2:10;
then A122: q .. f1 <= 1 by NAT_1:11;
1 <= q .. f1 by A8, FINSEQ_4:21;
hence contradiction by A10, A122, XXREAL_0:1; ::_thesis: verum
end;
then not p1 in rng (Rev (f1 :- q)) by FINSEQ_5:57;
then not p1 in (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) by XBOOLE_0:def_4;
then A123: (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) <> {p1} by TARSKI:def_1;
rng (f2 | l) c= rng f2 by FINSEQ_5:19;
then (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) c= (rng f2) /\ (rng f1) by A15, XBOOLE_1:27;
then A124: (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) c= {p1,p2} by A5, A17, XBOOLE_1:1;
reconsider f1q = f1 :- q as one-to-one FinSequence of (TOP-REAL 2) by A8, FINSEQ_5:56;
A125: Rev f1q is one-to-one ;
f1 :- q is s.n.c. by A8, Th34;
then A126: Rev (f1 :- q) is s.n.c. by Th35;
( ((f2 | l) /. (len (f2 | l))) `1 = ((Rev (f1 :- q)) /. 1) `1 or ((f2 | l) /. (len (f2 | l))) `2 = ((Rev (f1 :- q)) /. 1) `2 ) by A23, A14, A25, A26, TOPREAL1:def_5;
then A127: (f2 | l) ^ (Rev (f1 :- q)) is special by A115, Lm13;
(len (f2 | l)) + (len (Rev (f1 :- q))) >= 1 + 1 by A22, A19, A23, XREAL_1:7;
then A128: len ((f2 | l) ^ (Rev (f1 :- q))) >= 2 by FINSEQ_1:22;
(rng (f2 | l)) /\ (rng (Rev (f1 :- q))) <> {p2} by A101, TARSKI:def_1;
then (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) = {} by A123, A102, A124, ZFMISC_1:36;
then rng (f2 | l) misses rng (Rev (f1 :- q)) by XBOOLE_0:def_7;
then A129: (f2 | l) ^ (Rev (f1 :- q)) is one-to-one by A125, FINSEQ_3:91;
not p1 in (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) by A32, XBOOLE_0:def_4;
then L~ (f2 | l) misses L~ (Rev (f1 :- q)) by A114, A112, TARSKI:def_1, TARSKI:def_2, XBOOLE_0:def_7;
then (f2 | l) ^ (Rev (f1 :- q)) is s.n.c. by A126, A28, A47, Th36;
then reconsider g2 = (f2 | l) ^ (Rev (f1 :- q)) as S-Sequence_in_R2 by A129, A128, A82, A127, TOPREAL1:def_8;
A130: (L~ f2) \/ (L~ (Rev (f1 :- q))) = (L~ ((f2 | l) ^ <*p2*>)) \/ (L~ (Rev (f1 :- q))) by A4, A14, FINSEQ_5:21
.= ((L~ (f2 | l)) \/ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)))) \/ (L~ (Rev (f1 :- q))) by A4, A97, A26, Th19, RELAT_1:38
.= L~ g2 by A20, A80, Th23, RELAT_1:38 ;
take g1 ; ::_thesis: ex g2 being S-Sequence_in_R2 st
( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )
take g2 ; ::_thesis: ( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )
thus A131: p1 = g1 /. 1 by A1, A8, FINSEQ_5:44; ::_thesis: ( p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )
A132: 1 in dom g2 by FINSEQ_5:6;
hence A133: g2 /. 1 = g2 . 1 by PARTFUN1:def_6
.= (f2 | l) . 1 by A97, FINSEQ_1:def_7
.= (f2 | l) /. 1 by A97, PARTFUN1:def_6
.= p1 by A2, A97, FINSEQ_4:70 ;
::_thesis: ( q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )
thus A134: q = g1 /. (q .. f1) by A8, FINSEQ_5:45
.= g1 /. (len g1) by A8, FINSEQ_5:42 ; ::_thesis: ( q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )
A135: len g2 in dom g2 by FINSEQ_5:6;
hence A136: g2 /. (len g2) = g2 . (len g2) by PARTFUN1:def_6
.= g2 . ((len (f2 | l)) + (len (Rev (f1 :- q)))) by FINSEQ_1:22
.= (Rev (f1 :- q)) . (len (Rev (f1 :- q))) by A20, FINSEQ_1:def_7
.= (Rev (f1 :- q)) . (len (f1 :- q)) by FINSEQ_5:def_3
.= (f1 :- q) . 1 by FINSEQ_5:62
.= (f1 :- q) /. 1 by A116, PARTFUN1:def_6
.= q by FINSEQ_5:53 ;
::_thesis: ( (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )
len g2 >= 2 by TOPREAL1:def_8;
then A137: rng g2 c= L~ g2 by Th18;
A138: len g1 in dom g1 by FINSEQ_5:6;
thus {p1,q} = (L~ g1) /\ (L~ g2) ::_thesis: P = (L~ g1) \/ (L~ g2)
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (L~ g1) /\ (L~ g2) c= {p1,q}
let x be set ; ::_thesis: ( x in {p1,q} implies b1 in (L~ g1) /\ (L~ g2) )
assume A139: x in {p1,q} ; ::_thesis: b1 in (L~ g1) /\ (L~ g2)
percases ( x = p1 or x = q ) by A139, TARSKI:def_2;
supposeA140: x = p1 ; ::_thesis: b1 in (L~ g1) /\ (L~ g2)
A141: p1 in rng g2 by A132, A133, PARTFUN2:2;
p1 in rng g1 by A131, A13, PARTFUN2:2;
hence x in (L~ g1) /\ (L~ g2) by A96, A137, A140, A141, XBOOLE_0:def_4; ::_thesis: verum
end;
supposeA142: x = q ; ::_thesis: b1 in (L~ g1) /\ (L~ g2)
A143: q in rng g2 by A135, A136, PARTFUN2:2;
q in rng g1 by A134, A138, PARTFUN2:2;
hence x in (L~ g1) /\ (L~ g2) by A96, A137, A142, A143, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
A144: len f1 in dom f1 by FINSEQ_5:6;
A145: (L~ g1) /\ (L~ g2) = ((L~ g1) /\ (L~ f2)) \/ ((L~ g1) /\ (L~ (Rev (f1 :- q)))) by A130, XBOOLE_1:23;
A146: q .. f1 in dom f1 by A8, FINSEQ_4:20;
A147: q = f1 . (q .. f1) by A8, FINSEQ_4:19
.= f1 /. (q .. f1) by A146, PARTFUN1:def_6 ;
A148: len g1 = q .. f1 by A8, FINSEQ_5:42;
percases ( q <> p2 or q = p2 ) ;
supposeA149: q <> p2 ; ::_thesis: (L~ g1) /\ (L~ g2) c= {p1,q}
now__::_thesis:_not_p2_in_L~_g1
A150: q .. f1 <= len f1 by A8, FINSEQ_4:21;
then reconsider j = (len f1) - 1 as Element of NAT by A9, INT_1:5, XXREAL_0:2;
A151: j + 1 = len f1 ;
A152: p2 in LSeg ((f1 /. j),(f1 /. (j + 1))) by A3, RLTOPSP1:68;
1 < q .. f1 by A10, A9, XXREAL_0:1;
then 1 < len f1 by A150, XXREAL_0:2;
then 1 <= j by A151, NAT_1:13;
then A153: p2 in LSeg (f1,j) by A152, TOPREAL1:def_3;
assume p2 in L~ g1 ; ::_thesis: contradiction
then consider i being Element of NAT such that
A154: 1 <= i and
A155: i + 1 <= len g1 and
A156: p2 in LSeg (g1,i) by Th13;
A157: p2 in LSeg (f1,i) by A155, A156, Th9;
q .. f1 < len f1 by A3, A147, A149, A150, XXREAL_0:1;
then A158: q .. f1 <= j by A151, NAT_1:13;
then A159: i + 1 <= j by A148, A155, XXREAL_0:2;
percases ( i + 1 = j or i + 1 <> j ) ;
supposeA160: i + 1 = j ; ::_thesis: contradiction
then i + (1 + 1) = j + 1 ;
then (LSeg (f1,i)) /\ (LSeg (f1,(i + 1))) = {(f1 /. (i + 1))} by A154, TOPREAL1:def_6;
then p2 in {(f1 /. (i + 1))} by A157, A153, A160, XBOOLE_0:def_4;
then p2 = f1 /. (i + 1) by TARSKI:def_1;
hence contradiction by A148, A147, A149, A155, A158, A160, XXREAL_0:1; ::_thesis: verum
end;
suppose i + 1 <> j ; ::_thesis: contradiction
then i + 1 < j by A159, XXREAL_0:1;
then LSeg (f1,i) misses LSeg (f1,j) by TOPREAL1:def_7;
then (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} by XBOOLE_0:def_7;
hence contradiction by A157, A153, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
then A161: not p2 in (L~ g1) /\ (L~ f2) by XBOOLE_0:def_4;
(L~ g1) /\ (L~ f2) c= {p1,p2} by A5, A8, Lm14, XBOOLE_1:26;
then ( (L~ g1) /\ (L~ f2) = {} or (L~ g1) /\ (L~ f2) = {p1} or (L~ g1) /\ (L~ f2) = {p2} or (L~ g1) /\ (L~ f2) = {p1,p2} ) by ZFMISC_1:36;
then A162: (L~ g1) /\ (L~ f2) c= {p1} by A161, TARSKI:def_1, TARSKI:def_2, ZFMISC_1:33;
(L~ g1) /\ (L~ (Rev (f1 :- q))) = (L~ g1) /\ (L~ (f1 :- q)) by Th22
.= {q} by A3, A8, A10, A147, A149, Th42 ;
then (L~ g1) /\ (L~ g2) c= {p1} \/ {q} by A145, A162, XBOOLE_1:9;
hence (L~ g1) /\ (L~ g2) c= {p1,q} by ENUMSET1:1; ::_thesis: verum
end;
supposeA163: q = p2 ; ::_thesis: (L~ g1) /\ (L~ g2) c= {p1,q}
p2 .. f1 = len f1 by A3, A144, FINSEQ_5:41;
then A164: len (f1 :- q) = ((len f1) - (len f1)) + 1 by A8, A163, FINSEQ_5:50
.= 0 + 1 ;
(L~ g1) /\ (L~ (Rev (f1 :- q))) = (L~ g1) /\ (L~ (f1 :- q)) by Th22
.= (L~ g1) /\ {} by A164, TOPREAL1:22
.= {} ;
hence (L~ g1) /\ (L~ g2) c= {p1,q} by A5, A8, A145, A163, Lm14, XBOOLE_1:26; ::_thesis: verum
end;
end;
end;
thus P = ((L~ (f1 -: q)) \/ (L~ (f1 :- q))) \/ (L~ f2) by A6, A8, Th24
.= (L~ g1) \/ ((L~ f2) \/ (L~ (f1 :- q))) by XBOOLE_1:4
.= (L~ g1) \/ (L~ g2) by A130, Th22 ; ::_thesis: verum
end;
theorem Th51: :: SPPOL_2:51
for P being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p1 holds
p1,q split P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p1 holds
p1,q split P
let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( p1,p2 split P & q in P & q <> p1 implies p1,q split P )
assume p1 <> p2 ; :: according to SPPOL_2:def_1 ::_thesis: ( for f1, f2 being S-Sequence_in_R2 holds
( not p1 = f1 /. 1 or not p1 = f2 /. 1 or not p2 = f1 /. (len f1) or not p2 = f2 /. (len f2) or not (L~ f1) /\ (L~ f2) = {p1,p2} or not P = (L~ f1) \/ (L~ f2) ) or not q in P or not q <> p1 or p1,q split P )
given f1, f2 being S-Sequence_in_R2 such that A1: p1 = f1 /. 1 and
A2: p1 = f2 /. 1 and
A3: p2 = f1 /. (len f1) and
A4: p2 = f2 /. (len f2) and
A5: (L~ f1) /\ (L~ f2) = {p1,p2} and
A6: P = (L~ f1) \/ (L~ f2) ; ::_thesis: ( not q in P or not q <> p1 or p1,q split P )
assume A7: q in P ; ::_thesis: ( not q <> p1 or p1,q split P )
assume A8: q <> p1 ; ::_thesis: p1,q split P
hence p1 <> q ; :: according to SPPOL_2:def_1 ::_thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) )
percases ( q in L~ f1 or q in L~ f2 ) by A6, A7, XBOOLE_0:def_3;
supposeA9: q in L~ f1 ; ::_thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) )
now__::_thesis:_ex_f1,_f2_being_S-Sequence_in_R2_st_
(_p1_=_f1_/._1_&_p1_=_f2_/._1_&_q_=_f1_/._(len_f1)_&_q_=_f2_/._(len_f2)_&_(L~_f1)_/\_(L~_f2)_=_{p1,q}_&_P_=_(L~_f1)_\/_(L~_f2)_)
percases ( q in rng f1 or not q in rng f1 ) ;
suppose q in rng f1 ; ::_thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) )
hence ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) by A1, A2, A3, A4, A5, A6, A8, Lm16; ::_thesis: verum
end;
supposeA10: not q in rng f1 ; ::_thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) )
consider i being Element of NAT such that
A11: 1 <= i and
A12: i + 1 <= len f1 and
A13: q in LSeg (f1,i) by A9, Th13;
reconsider f19 = Ins (f1,i,q) as S-Sequence_in_R2 by A10, A13, Th48;
A14: L~ f19 = L~ f1 by A13, Th25;
len f19 = (len f1) + 1 by FINSEQ_5:69;
then A15: p2 = f19 /. (len f19) by A3, A12, FINSEQ_5:74;
A16: q in rng f19 by FINSEQ_5:71;
p1 = f19 /. 1 by A1, A11, FINSEQ_5:75;
hence ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) by A2, A4, A5, A6, A8, A16, A15, A14, Lm16; ::_thesis: verum
end;
end;
end;
hence ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) ; ::_thesis: verum
end;
supposeA17: q in L~ f2 ; ::_thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) )
now__::_thesis:_ex_f1,_f2_being_S-Sequence_in_R2_st_
(_p1_=_f1_/._1_&_p1_=_f2_/._1_&_q_=_f1_/._(len_f1)_&_q_=_f2_/._(len_f2)_&_(L~_f1)_/\_(L~_f2)_=_{p1,q}_&_P_=_(L~_f1)_\/_(L~_f2)_)
percases ( q in rng f2 or not q in rng f2 ) ;
suppose q in rng f2 ; ::_thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) )
hence ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) by A1, A2, A3, A4, A5, A6, A8, Lm16; ::_thesis: verum
end;
supposeA18: not q in rng f2 ; ::_thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) )
consider i being Element of NAT such that
A19: 1 <= i and
A20: i + 1 <= len f2 and
A21: q in LSeg (f2,i) by A17, Th13;
reconsider f29 = Ins (f2,i,q) as S-Sequence_in_R2 by A18, A21, Th48;
A22: L~ f29 = L~ f2 by A21, Th25;
len f29 = (len f2) + 1 by FINSEQ_5:69;
then A23: p2 = f29 /. (len f29) by A4, A20, FINSEQ_5:74;
A24: q in rng f29 by FINSEQ_5:71;
p1 = f29 /. 1 by A2, A19, FINSEQ_5:75;
hence ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) by A1, A3, A5, A6, A8, A24, A23, A22, Lm16; ::_thesis: verum
end;
end;
end;
hence ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) ; ::_thesis: verum
end;
end;
end;
theorem Th52: :: SPPOL_2:52
for P being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p2 holds
q,p2 split P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p2 holds
q,p2 split P
let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( p1,p2 split P & q in P & q <> p2 implies q,p2 split P )
assume that
A1: p1,p2 split P and
A2: q in P and
A3: q <> p2 ; ::_thesis: q,p2 split P
p2,p1 split P by A1, Th50;
then p2,q split P by A2, A3, Th51;
hence q,p2 split P by Th50; ::_thesis: verum
end;
theorem Th53: :: SPPOL_2:53
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1,p2 split P & q1 in P & q2 in P & q1 <> q2 holds
q1,q2 split P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1,p2 split P & q1 in P & q2 in P & q1 <> q2 holds
q1,q2 split P
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( p1,p2 split P & q1 in P & q2 in P & q1 <> q2 implies q1,q2 split P )
assume that
A1: p1,p2 split P and
A2: q1 in P and
A3: q2 in P and
A4: q1 <> q2 ; ::_thesis: q1,q2 split P
A5: p2,p1 split P by A1, Th50;
percases ( p1 = q1 or p1 = q2 or p1 <> q1 or p2 <> q1 ) ;
suppose p1 = q1 ; ::_thesis: q1,q2 split P
hence q1,q2 split P by A1, A3, A4, Th51; ::_thesis: verum
end;
suppose p1 = q2 ; ::_thesis: q1,q2 split P
hence q1,q2 split P by A2, A4, A5, Th52; ::_thesis: verum
end;
suppose p1 <> q1 ; ::_thesis: q1,q2 split P
then p1,q1 split P by A1, A2, Th51;
then q2,q1 split P by A3, A4, Th52;
hence q1,q2 split P by Th50; ::_thesis: verum
end;
suppose p2 <> q1 ; ::_thesis: q1,q2 split P
then q1,p2 split P by A1, A2, Th52;
hence q1,q2 split P by A3, A4, Th51; ::_thesis: verum
end;
end;
end;
notation
let P be Subset of (TOP-REAL 2);
synonym special_polygonal P for being_special_polygon ;
end;
definition
let P be Subset of (TOP-REAL 2);
redefine attr P is being_special_polygon means :Def2: :: SPPOL_2:def 2
ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P;
compatibility
( P is special_polygonal iff ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P )
proof
thus ( P is being_special_polygon implies ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P ) ::_thesis: ( ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P implies P is special_polygonal )
proof
given p1, p2 being Point of (TOP-REAL 2), P1, P2 being Subset of (TOP-REAL 2) such that A1: p1 <> p2 and
p1 in P and
p2 in P and
A2: P1 is_S-P_arc_joining p1,p2 and
A3: P2 is_S-P_arc_joining p1,p2 and
A4: P1 /\ P2 = {p1,p2} and
A5: P = P1 \/ P2 ; :: according to TOPREAL4:def_2 ::_thesis: ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P
take p1 ; ::_thesis: ex p2 being Point of (TOP-REAL 2) st p1,p2 split P
take p2 ; ::_thesis: p1,p2 split P
thus p1 <> p2 by A1; :: according to SPPOL_2:def_1 ::_thesis: ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) )
consider f1 being FinSequence of (TOP-REAL 2) such that
A6: f1 is being_S-Seq and
A7: P1 = L~ f1 and
A8: p1 = f1 /. 1 and
A9: p2 = f1 /. (len f1) by A2, TOPREAL4:def_1;
consider f2 being FinSequence of (TOP-REAL 2) such that
A10: f2 is being_S-Seq and
A11: P2 = L~ f2 and
A12: p1 = f2 /. 1 and
A13: p2 = f2 /. (len f2) by A3, TOPREAL4:def_1;
reconsider f1 = f1, f2 = f2 as S-Sequence_in_R2 by A6, A10;
take f1 ; ::_thesis: ex f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) )
take f2 ; ::_thesis: ( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) )
thus ( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) ) by A4, A5, A7, A8, A9, A11, A12, A13; ::_thesis: verum
end;
given p1, p2 being Point of (TOP-REAL 2) such that A14: p1,p2 split P ; ::_thesis: P is special_polygonal
A15: p2 in {p1,p2} by TARSKI:def_2;
A16: p1 in {p1,p2} by TARSKI:def_2;
consider f1, f2 being S-Sequence_in_R2 such that
A17: p1 = f1 /. 1 and
A18: p1 = f2 /. 1 and
A19: p2 = f1 /. (len f1) and
A20: p2 = f2 /. (len f2) and
A21: (L~ f1) /\ (L~ f2) = {p1,p2} and
A22: P = (L~ f1) \/ (L~ f2) by A14, Def1;
take p1 ; :: according to TOPREAL4:def_2 ::_thesis: ex b1 being Element of the carrier of (TOP-REAL 2) ex b2, b3 being Element of bool the carrier of (TOP-REAL 2) st
( not p1 = b1 & p1 in P & b1 in P & b2 is_S-P_arc_joining p1,b1 & b3 is_S-P_arc_joining p1,b1 & b2 /\ b3 = {p1,b1} & P = b2 \/ b3 )
take p2 ; ::_thesis: ex b1, b2 being Element of bool the carrier of (TOP-REAL 2) st
( not p1 = p2 & p1 in P & p2 in P & b1 is_S-P_arc_joining p1,p2 & b2 is_S-P_arc_joining p1,p2 & b1 /\ b2 = {p1,p2} & P = b1 \/ b2 )
take P1 = L~ f1; ::_thesis: ex b1 being Element of bool the carrier of (TOP-REAL 2) st
( not p1 = p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & b1 is_S-P_arc_joining p1,p2 & P1 /\ b1 = {p1,p2} & P = P1 \/ b1 )
take P2 = L~ f2; ::_thesis: ( not p1 = p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus p1 <> p2 by A14, Def1; ::_thesis: ( p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
{p1,p2} c= P by A21, A22, XBOOLE_1:29;
hence ( p1 in P & p2 in P ) by A16, A15; ::_thesis: ( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus ex f being FinSequence of (TOP-REAL 2) st
( f is being_S-Seq & P1 = L~ f & p1 = f /. 1 & p2 = f /. (len f) ) by A17, A19; :: according to TOPREAL4:def_1 ::_thesis: ( P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus ex f being FinSequence of (TOP-REAL 2) st
( f is being_S-Seq & P2 = L~ f & p1 = f /. 1 & p2 = f /. (len f) ) by A18, A20; :: according to TOPREAL4:def_1 ::_thesis: ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) by A21, A22; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines special_polygonal SPPOL_2:def_2_:_
for P being Subset of (TOP-REAL 2) holds
( P is special_polygonal iff ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P );
Lm17: for P being Subset of (TOP-REAL 2) st P is being_special_polygon holds
ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_special_polygon implies ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P ) )
assume P is being_special_polygon ; ::_thesis: ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P )
then ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) by TOPREAL4:def_2;
hence ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P ) ; ::_thesis: verum
end;
definition
let r1, r2, r19, r29 be real number ;
func[.r1,r2,r19,r29.] -> Subset of (TOP-REAL 2) equals :: SPPOL_2:def 3
((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|)));
coherence
((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|))) is Subset of (TOP-REAL 2) ;
end;
:: deftheorem defines [. SPPOL_2:def_3_:_
for r1, r2, r19, r29 being real number holds [.r1,r2,r19,r29.] = ((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|)));
registration
let n be Element of NAT ;
let p1, p2 be Point of (TOP-REAL n);
cluster LSeg (p1,p2) -> compact ;
coherence
LSeg (p1,p2) is compact ;
end;
registration
let r1, r2, r19, r29 be real number ;
cluster[.r1,r2,r19,r29.] -> non empty compact ;
coherence
( not [.r1,r2,r19,r29.] is empty & [.r1,r2,r19,r29.] is compact )
proof
thus not [.r1,r2,r19,r29.] is empty ; ::_thesis: [.r1,r2,r19,r29.] is compact
A1: (LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|)) is compact by COMPTS_1:10;
(LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|)) is compact by COMPTS_1:10;
hence [.r1,r2,r19,r29.] is compact by A1, COMPTS_1:10; ::_thesis: verum
end;
end;
theorem :: SPPOL_2:54
for r1, r2, r19, r29 being real number st r1 <= r2 & r19 <= r29 holds
[.r1,r2,r19,r29.] = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }
proof
let r1, r2, r19, r29 be real number ; ::_thesis: ( r1 <= r2 & r19 <= r29 implies [.r1,r2,r19,r29.] = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } )
assume that
A1: r1 <= r2 and
A2: r19 <= r29 ; ::_thesis: [.r1,r2,r19,r29.] = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }
set p1 = |[r1,r19]|;
set p2 = |[r1,r29]|;
set p3 = |[r2,r29]|;
set p4 = |[r2,r19]|;
set P4 = { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ;
set P3 = { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } ;
set P2 = { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ;
set P1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } ;
set P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } ;
A3: { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } = ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } )
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) c= { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }
let x be set ; ::_thesis: ( x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } implies x in ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) )
assume x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } ; ::_thesis: x in ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } )
then ex p being Point of (TOP-REAL 2) st
( x = p & ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) ) ;
then ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) ;
then ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) by XBOOLE_0:def_3;
hence x in ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) by XBOOLE_0:def_3; ::_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 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) or x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } )
assume x in ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }
then A4: ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) by XBOOLE_0:def_3;
percases ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) by A4, XBOOLE_0:def_3;
suppose x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }
then ex p being Point of (TOP-REAL 2) st
( x = p & p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) ;
hence x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } ; ::_thesis: verum
end;
suppose x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }
then ex p being Point of (TOP-REAL 2) st
( x = p & p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) ;
hence x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } ; ::_thesis: verum
end;
suppose x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }
then ex p being Point of (TOP-REAL 2) st
( x = p & p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) ;
hence x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } ; ::_thesis: verum
end;
suppose x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }
then ex p being Point of (TOP-REAL 2) st
( x = p & p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) ;
hence x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } ; ::_thesis: verum
end;
end;
end;
thus [.r1,r2,r19,r29.] = ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|))) by A2, TOPREAL3:9
.= ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|))) by A1, TOPREAL3:10
.= ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ (LSeg (|[r2,r19]|,|[r1,r19]|))) by A2, TOPREAL3:9
.= { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } by A1, A3, TOPREAL3:10 ; ::_thesis: verum
end;
theorem Th55: :: SPPOL_2:55
for r1, r2, r19, r29 being real number st r1 <> r2 & r19 <> r29 holds
[.r1,r2,r19,r29.] is special_polygonal
proof
let r1, r2, r19, r29 be real number ; ::_thesis: ( r1 <> r2 & r19 <> r29 implies [.r1,r2,r19,r29.] is special_polygonal )
assume that
A1: r1 <> r2 and
A2: r19 <> r29 ; ::_thesis: [.r1,r2,r19,r29.] is special_polygonal
set p1 = |[r1,r19]|;
set p2 = |[r1,r29]|;
set p3 = |[r2,r29]|;
set p4 = |[r2,r19]|;
A3: |[r2,r29]| `1 = r2 by EUCLID:52;
take |[r1,r19]| ; :: according to SPPOL_2:def_2 ::_thesis: ex p2 being Point of (TOP-REAL 2) st |[r1,r19]|,p2 split [.r1,r2,r19,r29.]
take |[r2,r29]| ; ::_thesis: |[r1,r19]|,|[r2,r29]| split [.r1,r2,r19,r29.]
thus |[r1,r19]| <> |[r2,r29]| by A1, FINSEQ_1:77; :: according to SPPOL_2:def_1 ::_thesis: ex f1, f2 being S-Sequence_in_R2 st
( |[r1,r19]| = f1 /. 1 & |[r1,r19]| = f2 /. 1 & |[r2,r29]| = f1 /. (len f1) & |[r2,r29]| = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {|[r1,r19]|,|[r2,r29]|} & [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) )
A4: |[r2,r19]| `1 = r2 by EUCLID:52;
A5: |[r2,r29]| `2 = r29 by EUCLID:52;
A6: |[r2,r19]| `2 = r19 by EUCLID:52;
set f1 = <*|[r1,r19]|,|[r1,r29]|,|[r2,r29]|*>;
set f2 = <*|[r1,r19]|,|[r2,r19]|,|[r2,r29]|*>;
A7: |[r1,r19]| `1 = r1 by EUCLID:52;
A8: len <*|[r1,r19]|,|[r2,r19]|,|[r2,r29]|*> = 3 by FINSEQ_1:45;
A9: len <*|[r1,r19]|,|[r1,r29]|,|[r2,r29]|*> = 3 by FINSEQ_1:45;
A10: |[r1,r19]| `2 = r19 by EUCLID:52;
then reconsider f1 = <*|[r1,r19]|,|[r1,r29]|,|[r2,r29]|*>, f2 = <*|[r1,r19]|,|[r2,r19]|,|[r2,r29]|*> as S-Sequence_in_R2 by A1, A2, A7, A3, A5, TOPREAL3:34, TOPREAL3:35;
take f1 ; ::_thesis: ex f2 being S-Sequence_in_R2 st
( |[r1,r19]| = f1 /. 1 & |[r1,r19]| = f2 /. 1 & |[r2,r29]| = f1 /. (len f1) & |[r2,r29]| = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {|[r1,r19]|,|[r2,r29]|} & [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) )
take f2 ; ::_thesis: ( |[r1,r19]| = f1 /. 1 & |[r1,r19]| = f2 /. 1 & |[r2,r29]| = f1 /. (len f1) & |[r2,r29]| = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {|[r1,r19]|,|[r2,r29]|} & [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) )
thus ( |[r1,r19]| = f1 /. 1 & |[r1,r19]| = f2 /. 1 & |[r2,r29]| = f1 /. (len f1) & |[r2,r29]| = f2 /. (len f2) ) by A9, A8, FINSEQ_4:18; ::_thesis: ( (L~ f1) /\ (L~ f2) = {|[r1,r19]|,|[r2,r29]|} & [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) )
A11: L~ f2 = (LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|)) by TOPREAL3:16;
L~ f1 = (LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|)) by TOPREAL3:16;
hence (L~ f1) /\ (L~ f2) = (((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) /\ (LSeg (|[r2,r29]|,|[r2,r19]|))) \/ (((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) /\ (LSeg (|[r2,r19]|,|[r1,r19]|))) by A11, XBOOLE_1:23
.= (((LSeg (|[r1,r29]|,|[r1,r19]|)) \/ (LSeg (|[r2,r29]|,|[r1,r29]|))) /\ (LSeg (|[r2,r19]|,|[r2,r29]|))) \/ {|[r1,r19]|} by A2, A7, A10, A5, A6, TOPREAL3:27
.= {|[r2,r29]|} \/ {|[r1,r19]|} by A1, A7, A3, A5, A4, TOPREAL3:28
.= {|[r1,r19]|,|[r2,r29]|} by ENUMSET1:1 ;
::_thesis: [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2)
thus [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) by A11, TOPREAL3:16; ::_thesis: verum
end;
theorem Th56: :: SPPOL_2:56
R^2-unit_square = [.0,1,0,1.] ;
registration
cluster special_polygonal for Element of bool the carrier of (TOP-REAL 2);
existence
ex b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal
proof
take [.0,1,0,1.] ; ::_thesis: [.0,1,0,1.] is special_polygonal
thus [.0,1,0,1.] is special_polygonal by Th55; ::_thesis: verum
end;
end;
registration
cluster R^2-unit_square -> special_polygonal ;
coherence
R^2-unit_square is special_polygonal by Th55, Th56;
end;
registration
cluster special_polygonal for Element of bool the carrier of (TOP-REAL 2);
existence
ex b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal by Th56;
cluster special_polygonal -> non empty for Element of bool the carrier of (TOP-REAL 2);
coherence
for b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal holds
not b1 is empty
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is special_polygonal implies not P is empty )
assume P is special_polygonal ; ::_thesis: not P is empty
then ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P ) by Lm17;
hence not P is empty ; ::_thesis: verum
end;
cluster special_polygonal -> non trivial for Element of bool the carrier of (TOP-REAL 2);
coherence
for b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal holds
not b1 is trivial
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is special_polygonal implies not P is trivial )
assume P is special_polygonal ; ::_thesis: not P is trivial
then ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P ) by Lm17;
hence not P is trivial by ZFMISC_1:def_10; ::_thesis: verum
end;
end;
definition
mode Special_polygon_in_R2 is special_polygonal Subset of (TOP-REAL 2);
end;
theorem Th57: :: SPPOL_2:57
for P being Subset of (TOP-REAL 2) st P is being_S-P_arc holds
P is compact
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_S-P_arc implies P is compact )
A1: I[01] is compact by HEINE:4, TOPMETR:20;
assume P is being_S-P_arc ; ::_thesis: P is compact
then reconsider P = P as being_S-P_arc Subset of (TOP-REAL 2) ;
consider f being Function of I[01],((TOP-REAL 2) | P) such that
A2: f is being_homeomorphism by TOPREAL1:29;
A3: rng f = [#] ((TOP-REAL 2) | P) by A2, TOPS_2:def_5;
f is continuous by A2, TOPS_2:def_5;
then (TOP-REAL 2) | P is compact by A1, A3, COMPTS_1:14;
hence P is compact by COMPTS_1:3; ::_thesis: verum
end;
registration
cluster special_polygonal -> compact for Element of bool the carrier of (TOP-REAL 2);
coherence
for b1 being Special_polygon_in_R2 holds b1 is compact
proof
let G be Special_polygon_in_R2; ::_thesis: G is compact
consider p, q being Point of (TOP-REAL 2), P1, P2 being Subset of (TOP-REAL 2) such that
p <> q and
p in G and
q in G and
A1: P1 is_S-P_arc_joining p,q and
A2: P2 is_S-P_arc_joining p,q and
P1 /\ P2 = {p,q} and
A3: G = P1 \/ P2 by TOPREAL4:def_2;
reconsider P1 = P1, P2 = P2 as Subset of (TOP-REAL 2) ;
A4: P2 is compact by A2, Th57, TOPREAL4:1;
P1 is compact by A1, Th57, TOPREAL4:1;
hence G is compact by A3, A4, COMPTS_1:10; ::_thesis: verum
end;
end;
theorem Th58: :: SPPOL_2:58
for P being Subset of (TOP-REAL 2) st P is special_polygonal holds
for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds
p1,p2 split P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is special_polygonal implies for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds
p1,p2 split P )
assume P is special_polygonal ; ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds
p1,p2 split P
then ex q1, q2 being Point of (TOP-REAL 2) st q1,q2 split P by Def2;
hence for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds
p1,p2 split P by Th53; ::_thesis: verum
end;
theorem :: SPPOL_2:59
for P being Subset of (TOP-REAL 2) st P is special_polygonal holds
for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds
ex P1, P2 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is special_polygonal implies for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds
ex P1, P2 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) )
assume A1: P is special_polygonal ; ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds
ex P1, P2 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 <> p2 & p1 in P & p2 in P implies ex P1, P2 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) )
assume that
A2: p1 <> p2 and
A3: p1 in P and
A4: p2 in P ; ::_thesis: ex P1, P2 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
p1,p2 split P by A1, A2, A3, A4, Th58;
then consider f1, f2 being S-Sequence_in_R2 such that
A5: p1 = f1 /. 1 and
A6: p1 = f2 /. 1 and
A7: p2 = f1 /. (len f1) and
A8: p2 = f2 /. (len f2) and
A9: (L~ f1) /\ (L~ f2) = {p1,p2} and
A10: P = (L~ f1) \/ (L~ f2) by Def1;
take P1 = L~ f1; ::_thesis: ex P2 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
take P2 = L~ f2; ::_thesis: ( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus P1 is_S-P_arc_joining p1,p2 by A5, A7, TOPREAL4:def_1; ::_thesis: ( P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus P2 is_S-P_arc_joining p1,p2 by A6, A8, TOPREAL4:def_1; ::_thesis: ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) by A9, A10; ::_thesis: verum
end;