:: JORDAN23 semantic presentation begin theorem Th1: :: JORDAN23:1 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f holds len (L_Cut (f,p)) >= 1 proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds len (L_Cut (f,p)) >= 1 let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies len (L_Cut (f,p)) >= 1 ) assume p in L~ f ; ::_thesis: len (L_Cut (f,p)) >= 1 then L_Cut (f,p) <> {} by JORDAN1E:3; then A1: len (L_Cut (f,p)) > 0 by NAT_1:3; 1 = 0 + 1 ; hence len (L_Cut (f,p)) >= 1 by A1, NAT_1:13; ::_thesis: verum end; theorem :: JORDAN23:2 for f being non empty FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) holds len (R_Cut (f,p)) >= 1 proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) holds len (R_Cut (f,p)) >= 1 let p be Point of (TOP-REAL 2); ::_thesis: len (R_Cut (f,p)) >= 1 R_Cut (f,p) <> {} by JORDAN1J:44; then A1: len (R_Cut (f,p)) > 0 by NAT_1:3; 1 = 0 + 1 ; hence len (R_Cut (f,p)) >= 1 by A1, NAT_1:13; ::_thesis: verum end; theorem Th3: :: JORDAN23:3 for f being FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) holds B_Cut (f,p,q) <> {} proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) holds B_Cut (f,p,q) <> {} let p, q be Point of (TOP-REAL 2); ::_thesis: B_Cut (f,p,q) <> {} A1: R_Cut ((L_Cut (f,q)),p) <> {} by JORDAN1J:44; percases ( ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) or ( not ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) ; suppose ( ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; ::_thesis: B_Cut (f,p,q) <> {} then B_Cut (f,p,q) = R_Cut ((L_Cut (f,p)),q) by JORDAN3:def_7; hence B_Cut (f,p,q) <> {} by JORDAN1J:44; ::_thesis: verum end; suppose ( not ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; ::_thesis: B_Cut (f,p,q) <> {} then B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) by JORDAN3:def_7; hence B_Cut (f,p,q) <> {} by A1; ::_thesis: verum end; end; end; registration let x be set ; cluster<*x*> -> one-to-one ; coherence <*x*> is one-to-one by FINSEQ_3:93; end; definition let f be FinSequence; attrf is almost-one-to-one means :Def1: :: JORDAN23:def 1 for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f . i = f . j holds i = j; end; :: deftheorem Def1 defines almost-one-to-one JORDAN23:def_1_:_ for f being FinSequence holds ( f is almost-one-to-one iff for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f . i = f . j holds i = j ); definition let f be FinSequence; attrf is weakly-one-to-one means :Def2: :: JORDAN23:def 2 for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1); end; :: deftheorem Def2 defines weakly-one-to-one JORDAN23:def_2_:_ for f being FinSequence holds ( f is weakly-one-to-one iff for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1) ); definition let f be FinSequence; attrf is poorly-one-to-one means :Def3: :: JORDAN23:def 3 for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1) if len f <> 2 otherwise verum; consistency verum ; end; :: deftheorem Def3 defines poorly-one-to-one JORDAN23:def_3_:_ for f being FinSequence holds ( ( len f <> 2 implies ( f is poorly-one-to-one iff for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1) ) ) & ( not len f <> 2 implies ( f is poorly-one-to-one iff verum ) ) ); theorem :: JORDAN23:4 for D being set for f being FinSequence of D holds ( f is almost-one-to-one iff for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j holds i = j ) proof let D be set ; ::_thesis: for f being FinSequence of D holds ( f is almost-one-to-one iff for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j holds i = j ) let f be FinSequence of D; ::_thesis: ( f is almost-one-to-one iff for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j holds i = j ) thus ( f is almost-one-to-one implies for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j holds i = j ) ::_thesis: ( ( for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j holds i = j ) implies f is almost-one-to-one ) proof assume A1: f is almost-one-to-one ; ::_thesis: for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j holds i = j let i, j be Element of NAT ; ::_thesis: ( i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j implies i = j ) assume that A2: i in dom f and A3: j in dom f and A4: ( i <> 1 or j <> len f ) and A5: ( i <> len f or j <> 1 ) and A6: f /. i = f /. j ; ::_thesis: i = j f . i = f /. j by A2, A6, PARTFUN1:def_6 .= f . j by A3, PARTFUN1:def_6 ; hence i = j by A1, A2, A3, A4, A5, Def1; ::_thesis: verum end; assume A7: for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j holds i = j ; ::_thesis: f is almost-one-to-one now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_f_&_j_in_dom_f_&_(_i_<>_1_or_j_<>_len_f_)_&_(_i_<>_len_f_or_j_<>_1_)_&_f_._i_=_f_._j_holds_ i_=_j let i, j be Element of NAT ; ::_thesis: ( i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f . i = f . j implies i = j ) assume that A8: i in dom f and A9: j in dom f and A10: ( i <> 1 or j <> len f ) and A11: ( i <> len f or j <> 1 ) and A12: f . i = f . j ; ::_thesis: i = j f /. i = f . j by A8, A12, PARTFUN1:def_6 .= f /. j by A9, PARTFUN1:def_6 ; hence i = j by A7, A8, A9, A10, A11; ::_thesis: verum end; hence f is almost-one-to-one by Def1; ::_thesis: verum end; theorem Th5: :: JORDAN23:5 for D being set for f being FinSequence of D holds ( f is weakly-one-to-one iff for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) ) proof let D be set ; ::_thesis: for f being FinSequence of D holds ( f is weakly-one-to-one iff for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) ) let f be FinSequence of D; ::_thesis: ( f is weakly-one-to-one iff for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) ) thus ( f is weakly-one-to-one implies for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) ) ::_thesis: ( ( for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) ) implies f is weakly-one-to-one ) proof assume A1: f is weakly-one-to-one ; ::_thesis: for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies f /. i <> f /. (i + 1) ) assume that A2: 1 <= i and A3: i < len f ; ::_thesis: f /. i <> f /. (i + 1) A4: i + 1 <= len f by A3, NAT_1:13; 1 < i + 1 by A2, NAT_1:13; then A5: f . (i + 1) = f /. (i + 1) by A4, FINSEQ_4:15; f . i = f /. i by A2, A3, FINSEQ_4:15; hence f /. i <> f /. (i + 1) by A1, A2, A3, A5, Def2; ::_thesis: verum end; assume A6: for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) ; ::_thesis: f is weakly-one-to-one now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<_len_f_holds_ f_._i_<>_f_._(i_+_1) let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies f . i <> f . (i + 1) ) assume that A7: 1 <= i and A8: i < len f ; ::_thesis: f . i <> f . (i + 1) A9: i + 1 <= len f by A8, NAT_1:13; 1 < i + 1 by A7, NAT_1:13; then A10: f . (i + 1) = f /. (i + 1) by A9, FINSEQ_4:15; f . i = f /. i by A7, A8, FINSEQ_4:15; hence f . i <> f . (i + 1) by A6, A7, A8, A10; ::_thesis: verum end; hence f is weakly-one-to-one by Def2; ::_thesis: verum end; theorem :: JORDAN23:6 for D being set for f being FinSequence of D holds ( f is poorly-one-to-one iff ( len f <> 2 implies for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) ) ) proof let D be set ; ::_thesis: for f being FinSequence of D holds ( f is poorly-one-to-one iff ( len f <> 2 implies for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) ) ) let f be FinSequence of D; ::_thesis: ( f is poorly-one-to-one iff ( len f <> 2 implies for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) ) ) thus ( f is poorly-one-to-one & len f <> 2 implies for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) ) ::_thesis: ( ( len f <> 2 implies for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) ) implies f is poorly-one-to-one ) proof assume that A1: f is poorly-one-to-one and A2: len f <> 2 ; ::_thesis: for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies f /. i <> f /. (i + 1) ) assume that A3: 1 <= i and A4: i < len f ; ::_thesis: f /. i <> f /. (i + 1) A5: i + 1 <= len f by A4, NAT_1:13; 1 < i + 1 by A3, NAT_1:13; then A6: f . (i + 1) = f /. (i + 1) by A5, FINSEQ_4:15; f . i = f /. i by A3, A4, FINSEQ_4:15; hence f /. i <> f /. (i + 1) by A1, A2, A3, A4, A6, Def3; ::_thesis: verum end; assume A7: ( len f <> 2 implies for i being Element of NAT st 1 <= i & i < len f holds f /. i <> f /. (i + 1) ) ; ::_thesis: f is poorly-one-to-one percases ( len f <> 2 or len f = 2 ) ; supposeA8: len f <> 2 ; ::_thesis: f is poorly-one-to-one now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<_len_f_holds_ f_._i_<>_f_._(i_+_1) let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies f . i <> f . (i + 1) ) assume that A9: 1 <= i and A10: i < len f ; ::_thesis: f . i <> f . (i + 1) A11: i + 1 <= len f by A10, NAT_1:13; 1 < i + 1 by A9, NAT_1:13; then A12: f . (i + 1) = f /. (i + 1) by A11, FINSEQ_4:15; f . i = f /. i by A9, A10, FINSEQ_4:15; hence f . i <> f . (i + 1) by A7, A8, A9, A10, A12; ::_thesis: verum end; hence f is poorly-one-to-one by A8, Def3; ::_thesis: verum end; suppose len f = 2 ; ::_thesis: f is poorly-one-to-one hence f is poorly-one-to-one by Def3; ::_thesis: verum end; end; end; registration clusterV13() Function-like one-to-one FinSequence-like -> almost-one-to-one for set ; coherence for b1 being FinSequence st b1 is one-to-one holds b1 is almost-one-to-one proof let f be FinSequence; ::_thesis: ( f is one-to-one implies f is almost-one-to-one ) assume A1: f is one-to-one ; ::_thesis: f is almost-one-to-one let i, j be Element of NAT ; :: according to JORDAN23:def_1 ::_thesis: ( i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f . i = f . j implies i = j ) assume that A2: i in dom f and A3: j in dom f and ( i <> 1 or j <> len f ) and ( i <> len f or j <> 1 ) and A4: f . i = f . j ; ::_thesis: i = j thus i = j by A1, A2, A3, A4, FUNCT_1:def_4; ::_thesis: verum end; end; registration clusterV13() Function-like FinSequence-like almost-one-to-one -> poorly-one-to-one for set ; coherence for b1 being FinSequence st b1 is almost-one-to-one holds b1 is poorly-one-to-one proof let f be FinSequence; ::_thesis: ( f is almost-one-to-one implies f is poorly-one-to-one ) assume A1: f is almost-one-to-one ; ::_thesis: f is poorly-one-to-one percases ( len f <> 2 or len f = 2 ) ; :: according to JORDAN23:def_3 caseA2: len f <> 2 ; ::_thesis: for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1) now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<_len_f_holds_ f_._i_<>_f_._(i_+_1) percases ( len f <> 0 or len f = 0 ) ; supposeA3: len f <> 0 ; ::_thesis: for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1) let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies f . i <> f . (i + 1) ) A4: ( not i = len f or not i + 1 = 1 ) by A3; A5: i + 1 >= 1 by NAT_1:11; assume that A6: 1 <= i and A7: i < len f ; ::_thesis: f . i <> f . (i + 1) i + 1 <= len f by A7, NAT_1:13; then A8: i + 1 in dom f by A5, FINSEQ_3:25; A9: ( not i = 1 or not i + 1 = len f ) by A2; A10: i <> i + 1 ; i in dom f by A6, A7, FINSEQ_3:25; hence f . i <> f . (i + 1) by A1, A8, A10, A9, A4, Def1; ::_thesis: verum end; supposeA11: len f = 0 ; ::_thesis: for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1) let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies f . i <> f . (i + 1) ) assume that A12: 1 <= i and A13: i < len f ; ::_thesis: f . i <> f . (i + 1) thus f . i <> f . (i + 1) by A11, A12, A13; ::_thesis: verum end; end; end; hence for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1) ; ::_thesis: verum end; case len f = 2 ; ::_thesis: verum end; end; end; end; theorem Th7: :: JORDAN23:7 for f being FinSequence st len f <> 2 holds ( f is weakly-one-to-one iff f is poorly-one-to-one ) proof let f be FinSequence; ::_thesis: ( len f <> 2 implies ( f is weakly-one-to-one iff f is poorly-one-to-one ) ) assume A1: len f <> 2 ; ::_thesis: ( f is weakly-one-to-one iff f is poorly-one-to-one ) thus ( f is weakly-one-to-one implies f is poorly-one-to-one ) ::_thesis: ( f is poorly-one-to-one implies f is weakly-one-to-one ) proof assume f is weakly-one-to-one ; ::_thesis: f is poorly-one-to-one then for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1) by Def2; hence f is poorly-one-to-one by A1, Def3; ::_thesis: verum end; assume f is poorly-one-to-one ; ::_thesis: f is weakly-one-to-one then for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1) by A1, Def3; hence f is weakly-one-to-one by Def2; ::_thesis: verum end; registration cluster empty V13() Function-like FinSequence-like -> weakly-one-to-one for set ; coherence for b1 being FinSequence st b1 is empty holds b1 is weakly-one-to-one proof let F be FinSequence; ::_thesis: ( F is empty implies F is weakly-one-to-one ) assume A1: F is empty ; ::_thesis: F is weakly-one-to-one let i be Element of NAT ; :: according to JORDAN23:def_2 ::_thesis: ( 1 <= i & i < len F implies F . i <> F . (i + 1) ) assume that A2: 1 <= i and A3: i < len F ; ::_thesis: F . i <> F . (i + 1) thus F . i <> F . (i + 1) by A1, A2, A3; ::_thesis: verum end; end; registration let x be set ; cluster<*x*> -> weakly-one-to-one ; coherence <*x*> is weakly-one-to-one proof let i be Element of NAT ; :: according to JORDAN23:def_2 ::_thesis: ( 1 <= i & i < len <*x*> implies <*x*> . i <> <*x*> . (i + 1) ) assume that A1: 1 <= i and A2: i < len <*x*> ; ::_thesis: <*x*> . i <> <*x*> . (i + 1) thus <*x*> . i <> <*x*> . (i + 1) by A1, A2, FINSEQ_1:39; ::_thesis: verum end; end; registration let x, y be set ; cluster<*x,y*> -> poorly-one-to-one ; coherence <*x,y*> is poorly-one-to-one proof len <*x,y*> = 2 by FINSEQ_1:44; hence <*x,y*> is poorly-one-to-one by Def3; ::_thesis: verum end; end; registration cluster non empty V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like weakly-one-to-one for set ; existence ex b1 being FinSequence st ( b1 is weakly-one-to-one & not b1 is empty ) proof set x = the set ; len <* the set *> <> 2 by FINSEQ_1:39; hence ex b1 being FinSequence st ( b1 is weakly-one-to-one & not b1 is empty ) ; ::_thesis: verum end; end; registration let D be non empty set ; cluster non empty V13() V16( NAT ) V17(D) Function-like V26() FinSequence-like FinSubsequence-like circular weakly-one-to-one for FinSequence of D; existence ex b1 being FinSequence of D st ( b1 is weakly-one-to-one & b1 is circular & not b1 is empty ) proof set x = the Element of D; <* the Element of D*> /. 1 = <* the Element of D*> /. (len <* the Element of D*>) by FINSEQ_1:39; then <* the Element of D*> is circular by FINSEQ_6:def_1; hence ex b1 being FinSequence of D st ( b1 is weakly-one-to-one & b1 is circular & not b1 is empty ) ; ::_thesis: verum end; end; theorem Th8: :: JORDAN23:8 for f being FinSequence st f is almost-one-to-one holds Rev f is almost-one-to-one proof let f be FinSequence; ::_thesis: ( f is almost-one-to-one implies Rev f is almost-one-to-one ) assume A1: f is almost-one-to-one ; ::_thesis: Rev f is almost-one-to-one let i, j be Element of NAT ; :: according to JORDAN23:def_1 ::_thesis: ( i in dom (Rev f) & j in dom (Rev f) & ( i <> 1 or j <> len (Rev f) ) & ( i <> len (Rev f) or j <> 1 ) & (Rev f) . i = (Rev f) . j implies i = j ) assume that A2: i in dom (Rev f) and A3: j in dom (Rev f) and A4: ( i <> 1 or j <> len (Rev f) ) and A5: ( i <> len (Rev f) or j <> 1 ) and A6: (Rev f) . i = (Rev f) . j ; ::_thesis: i = j A7: ( not ((len f) - i) + 1 = len f or not ((len f) - j) + 1 = 1 ) by A4, FINSEQ_5:def_3; A8: dom f = dom (Rev f) by FINSEQ_5:57; then i in Seg (len f) by A2, FINSEQ_1:def_3; then ((len f) - i) + 1 in Seg (len f) by FINSEQ_5:2; then A9: ((len f) - i) + 1 in dom f by FINSEQ_1:def_3; A10: (Rev f) . j = f . (((len f) - j) + 1) by A3, FINSEQ_5:def_3; A11: (Rev f) . i = f . (((len f) - i) + 1) by A2, FINSEQ_5:def_3; j in Seg (len f) by A3, A8, FINSEQ_1:def_3; then ((len f) - j) + 1 in Seg (len f) by FINSEQ_5:2; then A12: ((len f) - j) + 1 in dom f by FINSEQ_1:def_3; ( not ((len f) - i) + 1 = 1 or not ((len f) - j) + 1 = len f ) by A5, FINSEQ_5:def_3; then ((len f) - i) + 1 = ((len f) - j) + 1 by A1, A6, A9, A12, A7, A11, A10, Def1; hence i = j ; ::_thesis: verum end; theorem Th9: :: JORDAN23:9 for f being FinSequence st f is weakly-one-to-one holds Rev f is weakly-one-to-one proof let f be FinSequence; ::_thesis: ( f is weakly-one-to-one implies Rev f is weakly-one-to-one ) assume A1: f is weakly-one-to-one ; ::_thesis: Rev f is weakly-one-to-one A2: len f = len (Rev f) by FINSEQ_5:def_3; let i be Element of NAT ; :: according to JORDAN23:def_2 ::_thesis: ( 1 <= i & i < len (Rev f) implies (Rev f) . i <> (Rev f) . (i + 1) ) assume that A3: 1 <= i and A4: i < len (Rev f) ; ::_thesis: (Rev f) . i <> (Rev f) . (i + 1) A5: i + 1 <= len (Rev f) by A4, NAT_1:13; i + 1 >= 1 by NAT_1:11; then A6: i + 1 in Seg (len (Rev f)) by A5, FINSEQ_1:1; then i + 1 in dom (Rev f) by FINSEQ_1:def_3; then A7: (Rev f) . (i + 1) = f . (((len f) - (i + 1)) + 1) by FINSEQ_5:def_3; A8: i in Seg (len (Rev f)) by A3, A4, FINSEQ_1:1; then i in dom (Rev f) by FINSEQ_1:def_3; then A9: (Rev f) . i = f . (((len f) - i) + 1) by FINSEQ_5:def_3; ((len f) - (i + 1)) + 1 = (len f) - i ; then reconsider j = (len f) - i as Element of NAT by A2, A5, FINSEQ_5:1; ((len f) - i) + 1 in Seg (len f) by A2, A8, FINSEQ_5:2; then j + 1 <= len f by FINSEQ_1:1; then A10: j < len f by NAT_1:13; ((len f) - (i + 1)) + 1 in Seg (len f) by A2, A6, FINSEQ_5:2; then j >= 1 by FINSEQ_1:1; hence (Rev f) . i <> (Rev f) . (i + 1) by A1, A9, A7, A10, Def2; ::_thesis: verum end; theorem Th10: :: JORDAN23:10 for f being FinSequence st f is poorly-one-to-one holds Rev f is poorly-one-to-one proof let f be FinSequence; ::_thesis: ( f is poorly-one-to-one implies Rev f is poorly-one-to-one ) assume A1: f is poorly-one-to-one ; ::_thesis: Rev f is poorly-one-to-one A2: len f = len (Rev f) by FINSEQ_5:def_3; percases ( len f <> 2 or len f = 2 ) ; supposeA3: len f <> 2 ; ::_thesis: Rev f is poorly-one-to-one then f is weakly-one-to-one by A1, Th7; then Rev f is weakly-one-to-one by Th9; hence Rev f is poorly-one-to-one by A2, A3, Th7; ::_thesis: verum end; suppose len f = 2 ; ::_thesis: Rev f is poorly-one-to-one hence Rev f is poorly-one-to-one by A2, Def3; ::_thesis: verum end; end; end; registration cluster non empty V13() V16( NAT ) Function-like one-to-one V26() FinSequence-like FinSubsequence-like for set ; existence ex b1 being FinSequence st ( b1 is one-to-one & not b1 is empty ) proof set x = the set ; ( not <* the set *> is empty & <* the set *> is one-to-one ) ; hence ex b1 being FinSequence st ( b1 is one-to-one & not b1 is empty ) ; ::_thesis: verum end; end; registration let f be almost-one-to-one FinSequence; cluster Rev f -> almost-one-to-one ; coherence Rev f is almost-one-to-one by Th8; end; registration let f be weakly-one-to-one FinSequence; cluster Rev f -> weakly-one-to-one ; coherence Rev f is weakly-one-to-one by Th9; end; registration let f be poorly-one-to-one FinSequence; cluster Rev f -> poorly-one-to-one ; coherence Rev f is poorly-one-to-one by Th10; end; theorem Th11: :: JORDAN23:11 for D being non empty set for f being FinSequence of D st f is almost-one-to-one holds for p being Element of D holds Rotate (f,p) is almost-one-to-one proof let D be non empty set ; ::_thesis: for f being FinSequence of D st f is almost-one-to-one holds for p being Element of D holds Rotate (f,p) is almost-one-to-one let f be FinSequence of D; ::_thesis: ( f is almost-one-to-one implies for p being Element of D holds Rotate (f,p) is almost-one-to-one ) assume A1: f is almost-one-to-one ; ::_thesis: for p being Element of D holds Rotate (f,p) is almost-one-to-one let p be Element of D; ::_thesis: Rotate (f,p) is almost-one-to-one percases ( p in rng f or not p in rng f ) ; supposeA2: p in rng f ; ::_thesis: Rotate (f,p) is almost-one-to-one then 0 + 1 <= p .. f by FINSEQ_4:21; then A3: (p .. f) - 1 >= 0 by XREAL_1:19; A4: len (f :- p) = ((len f) - (p .. f)) + 1 by A2, FINSEQ_5:50; let i, j be Element of NAT ; :: according to JORDAN23:def_1 ::_thesis: ( i in dom (Rotate (f,p)) & j in dom (Rotate (f,p)) & ( i <> 1 or j <> len (Rotate (f,p)) ) & ( i <> len (Rotate (f,p)) or j <> 1 ) & (Rotate (f,p)) . i = (Rotate (f,p)) . j implies i = j ) assume that A5: i in dom (Rotate (f,p)) and A6: j in dom (Rotate (f,p)) and A7: ( i <> 1 or j <> len (Rotate (f,p)) ) and A8: ( i <> len (Rotate (f,p)) or j <> 1 ) and A9: (Rotate (f,p)) . i = (Rotate (f,p)) . j ; ::_thesis: i = j A10: 0 + 1 <= i by A5, FINSEQ_3:25; A11: dom (Rotate (f,p)) = dom f by REVROT_1:15; then A12: i <= len f by A5, FINSEQ_3:25; then A13: i - (len f) <= (len f) - (len f) by XREAL_1:9; A14: j <= len f by A6, A11, FINSEQ_3:25; then A15: j - (len f) <= (len f) - (len f) by XREAL_1:9; A16: len (Rotate (f,p)) = len f by REVROT_1:14; A17: 0 + 1 <= j by A6, FINSEQ_3:25; then A18: j - 1 >= 0 by XREAL_1:19; A19: now__::_thesis:_(_(i_-'_1)_+_(p_.._f)_=_len_f_implies_not_(j_-'_1)_+_(p_.._f)_=_1_) assume that A20: (i -' 1) + (p .. f) = len f and A21: (j -' 1) + (p .. f) = 1 ; ::_thesis: contradiction (j -' 1) + ((p .. f) - 1) = 0 by A21; then A22: j -' 1 = 0 by A3; then j - 1 = 0 by A18, XREAL_0:def_2; hence contradiction by A8, A16, A10, A20, A21, A22, XREAL_1:235; ::_thesis: verum end; A23: p .. f <= len f by A2, FINSEQ_4:21; A24: i - 1 >= 0 by A10, XREAL_1:19; A25: now__::_thesis:_(_(i_-'_1)_+_(p_.._f)_=_1_implies_not_(j_-'_1)_+_(p_.._f)_=_len_f_) assume that A26: (i -' 1) + (p .. f) = 1 and A27: (j -' 1) + (p .. f) = len f ; ::_thesis: contradiction (i -' 1) + ((p .. f) - 1) = 0 by A26; then A28: i -' 1 = 0 by A3; then i - 1 = 0 by A24, XREAL_0:def_2; hence contradiction by A7, A16, A17, A26, A27, A28, XREAL_1:235; ::_thesis: verum end; now__::_thesis:_i_=_j percases ( i <= len (f :- p) or i > len (f :- p) ) ; supposeA29: i <= len (f :- p) ; ::_thesis: i = j then i in dom (f :- p) by A10, FINSEQ_3:25; then (i -' 1) + 1 in dom (f :- p) by A10, XREAL_1:235; then A30: (i -' 1) + (p .. f) in dom f by A2, FINSEQ_5:51; (Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) by A2, A10, A29, REVROT_1:9; then A31: (Rotate (f,p)) . i = f /. ((i -' 1) + (p .. f)) by A5, PARTFUN1:def_6; now__::_thesis:_i_=_j percases ( j <= len (f :- p) or j > len (f :- p) ) ; supposeA32: j <= len (f :- p) ; ::_thesis: i = j then j in dom (f :- p) by A17, FINSEQ_3:25; then (j -' 1) + 1 in dom (f :- p) by A17, XREAL_1:235; then A33: (j -' 1) + (p .. f) in dom f by A2, FINSEQ_5:51; (Rotate (f,p)) /. j = f /. ((j -' 1) + (p .. f)) by A2, A17, A32, REVROT_1:9; then A34: f /. ((i -' 1) + (p .. f)) = f /. ((j -' 1) + (p .. f)) by A6, A9, A31, PARTFUN1:def_6; f . ((i -' 1) + (p .. f)) = f /. ((i -' 1) + (p .. f)) by A30, PARTFUN1:def_6 .= f . ((j -' 1) + (p .. f)) by A34, A33, PARTFUN1:def_6 ; then (i -' 1) + (p .. f) = (j -' 1) + (p .. f) by A1, A25, A19, A30, A33, Def1; hence i = j by A10, A17, XREAL_1:234; ::_thesis: verum end; supposeA35: j > len (f :- p) ; ::_thesis: i = j then (Rotate (f,p)) /. j = f /. ((j + (p .. f)) -' (len f)) by A2, A14, REVROT_1:12; then A36: f /. ((i -' 1) + (p .. f)) = f /. ((j + (p .. f)) -' (len f)) by A6, A9, A31, PARTFUN1:def_6; A37: j - ((len f) - (p .. f)) > 1 by A4, A35, XREAL_1:20; then A38: (j + (p .. f)) - (len f) > 1 ; then A39: (j + (p .. f)) -' (len f) >= 1 by XREAL_0:def_2; j + (p .. f) <= (len f) + (len f) by A23, A14, XREAL_1:7; then (j + (p .. f)) - (len f) <= len f by XREAL_1:20; then (j + (p .. f)) -' (len f) <= len f by A37, XREAL_0:def_2; then A40: (j + (p .. f)) -' (len f) in dom f by A39, FINSEQ_3:25; A41: now__::_thesis:_(_(i_-'_1)_+_(p_.._f)_=_1_implies_not_(j_+_(p_.._f))_-'_(len_f)_=_len_f_) assume that A42: (i -' 1) + (p .. f) = 1 and A43: (j + (p .. f)) -' (len f) = len f ; ::_thesis: contradiction (j + (p .. f)) - (len f) = len f by A37, A43, XREAL_0:def_2; then j + (p .. f) = (len f) + (len f) ; then A44: j >= len f by A23, XREAL_1:8; (i -' 1) + ((p .. f) - 1) = 0 by A42; then i -' 1 = 0 by A3; then i - 1 = 0 by A24, XREAL_0:def_2; hence contradiction by A7, A16, A14, A44, XXREAL_0:1; ::_thesis: verum end; A45: ( (i -' 1) + (p .. f) <> len f or (j + (p .. f)) -' (len f) <> 1 ) by A38, XREAL_0:def_2; f . ((i -' 1) + (p .. f)) = f /. ((i -' 1) + (p .. f)) by A30, PARTFUN1:def_6 .= f . ((j + (p .. f)) -' (len f)) by A36, A40, PARTFUN1:def_6 ; then (i -' 1) + (p .. f) = (j + (p .. f)) -' (len f) by A1, A30, A41, A45, A40, Def1; then A46: (i -' 1) + (p .. f) = (j + (p .. f)) - (len f) by A37, XREAL_0:def_2; then A47: j - (len f) = 0 by A15; i - 1 = 0 by A24, A15, A46, XREAL_0:def_2; hence i = j by A7, A47, REVROT_1:14; ::_thesis: verum end; end; end; hence i = j ; ::_thesis: verum end; supposeA48: i > len (f :- p) ; ::_thesis: i = j then A49: i - ((len f) - (p .. f)) > 1 by A4, XREAL_1:20; i + (p .. f) <= (len f) + (len f) by A23, A12, XREAL_1:7; then (i + (p .. f)) - (len f) <= len f by XREAL_1:20; then A50: (i + (p .. f)) -' (len f) <= len f by A49, XREAL_0:def_2; A51: (i + (p .. f)) - (len f) > 1 by A49; then (i + (p .. f)) -' (len f) >= 1 by XREAL_0:def_2; then A52: (i + (p .. f)) -' (len f) in dom f by A50, FINSEQ_3:25; A53: (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) by A2, A12, A48, REVROT_1:12; now__::_thesis:_i_=_j percases ( j <= len (f :- p) or j > len (f :- p) ) ; supposeA54: j <= len (f :- p) ; ::_thesis: i = j A55: now__::_thesis:_(_(j_-'_1)_+_(p_.._f)_=_1_implies_not_(i_+_(p_.._f))_-'_(len_f)_=_len_f_) assume that A56: (j -' 1) + (p .. f) = 1 and A57: (i + (p .. f)) -' (len f) = len f ; ::_thesis: contradiction (i + (p .. f)) - (len f) = len f by A49, A57, XREAL_0:def_2; then i + (p .. f) = (len f) + (len f) ; then A58: i >= len f by A23, XREAL_1:8; (j -' 1) + ((p .. f) - 1) = 0 by A56; then j -' 1 = 0 by A3; then j - 1 = 0 by A18, XREAL_0:def_2; hence contradiction by A8, A16, A12, A58, XXREAL_0:1; ::_thesis: verum end; (Rotate (f,p)) /. j = f /. ((j -' 1) + (p .. f)) by A2, A17, A54, REVROT_1:9; then (Rotate (f,p)) . j = f /. ((j -' 1) + (p .. f)) by A6, PARTFUN1:def_6; then A59: f /. ((j -' 1) + (p .. f)) = f /. ((i + (p .. f)) -' (len f)) by A5, A9, A53, PARTFUN1:def_6; A60: ( (j -' 1) + (p .. f) <> len f or (i + (p .. f)) -' (len f) <> 1 ) by A51, XREAL_0:def_2; j in dom (f :- p) by A17, A54, FINSEQ_3:25; then (j -' 1) + 1 in dom (f :- p) by A17, XREAL_1:235; then A61: (j -' 1) + (p .. f) in dom f by A2, FINSEQ_5:51; then f . ((j -' 1) + (p .. f)) = f /. ((j -' 1) + (p .. f)) by PARTFUN1:def_6 .= f . ((i + (p .. f)) -' (len f)) by A52, A59, PARTFUN1:def_6 ; then (j -' 1) + (p .. f) = (i + (p .. f)) -' (len f) by A1, A52, A61, A55, A60, Def1; then A62: (j -' 1) + (p .. f) = (i + (p .. f)) - (len f) by A49, XREAL_0:def_2; then A63: i - (len f) = 0 by A13; j - 1 = 0 by A18, A13, A62, XREAL_0:def_2; hence i = j by A8, A63, REVROT_1:14; ::_thesis: verum end; supposeA64: j > len (f :- p) ; ::_thesis: i = j then (Rotate (f,p)) /. j = f /. ((j + (p .. f)) -' (len f)) by A2, A14, REVROT_1:12; then (Rotate (f,p)) . j = f /. ((j + (p .. f)) -' (len f)) by A6, PARTFUN1:def_6; then A65: f /. ((j + (p .. f)) -' (len f)) = f /. ((i + (p .. f)) -' (len f)) by A5, A9, A53, PARTFUN1:def_6; A66: ( (i + (p .. f)) -' (len f) <> 1 or (j + (p .. f)) -' (len f) <> len f ) by A51, XREAL_0:def_2; A67: j - ((len f) - (p .. f)) > 1 by A4, A64, XREAL_1:20; then A68: (j + (p .. f)) - (len f) > 1 ; then A69: (j + (p .. f)) -' (len f) >= 1 by XREAL_0:def_2; j + (p .. f) <= (len f) + (len f) by A23, A14, XREAL_1:7; then (j + (p .. f)) - (len f) <= len f by XREAL_1:20; then (j + (p .. f)) -' (len f) <= len f by A67, XREAL_0:def_2; then A70: (j + (p .. f)) -' (len f) in dom f by A69, FINSEQ_3:25; A71: ( (i + (p .. f)) -' (len f) <> len f or (j + (p .. f)) -' (len f) <> 1 ) by A68, XREAL_0:def_2; f . ((i + (p .. f)) -' (len f)) = f /. ((i + (p .. f)) -' (len f)) by A52, PARTFUN1:def_6 .= f . ((j + (p .. f)) -' (len f)) by A65, A70, PARTFUN1:def_6 ; then (i + (p .. f)) -' (len f) = (j + (p .. f)) -' (len f) by A1, A52, A70, A66, A71, Def1; then (i + (p .. f)) - (len f) = (j + (p .. f)) -' (len f) by A49, XREAL_0:def_2; then (i + (p .. f)) - (len f) = (j + (p .. f)) - (len f) by A67, XREAL_0:def_2; hence i = j ; ::_thesis: verum end; end; end; hence i = j ; ::_thesis: verum end; end; end; hence i = j ; ::_thesis: verum end; suppose not p in rng f ; ::_thesis: Rotate (f,p) is almost-one-to-one hence Rotate (f,p) is almost-one-to-one by A1, FINSEQ_6:def_2; ::_thesis: verum end; end; end; theorem Th12: :: JORDAN23:12 for D being non empty set for f being FinSequence of D st f is weakly-one-to-one & f is circular holds for p being Element of D holds Rotate (f,p) is weakly-one-to-one proof let D be non empty set ; ::_thesis: for f being FinSequence of D st f is weakly-one-to-one & f is circular holds for p being Element of D holds Rotate (f,p) is weakly-one-to-one let f be FinSequence of D; ::_thesis: ( f is weakly-one-to-one & f is circular implies for p being Element of D holds Rotate (f,p) is weakly-one-to-one ) assume A1: ( f is weakly-one-to-one & f is circular ) ; ::_thesis: for p being Element of D holds Rotate (f,p) is weakly-one-to-one let p be Element of D; ::_thesis: Rotate (f,p) is weakly-one-to-one percases ( p in rng f or not p in rng f ) ; supposeA2: p in rng f ; ::_thesis: Rotate (f,p) is weakly-one-to-one then A3: p .. f <= len f by FINSEQ_4:21; A4: len (f :- p) = ((len f) - (p .. f)) + 1 by A2, FINSEQ_5:50; let i be Element of NAT ; :: according to JORDAN23:def_2 ::_thesis: ( 1 <= i & i < len (Rotate (f,p)) implies (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1) ) 1 <= p .. f by A2, FINSEQ_4:21; then A5: (i -' 1) + (p .. f) >= 0 + 1 by XREAL_1:7; then A6: ((i -' 1) + (p .. f)) + 1 > 1 by NAT_1:13; assume that A7: 1 <= i and A8: i < len (Rotate (f,p)) ; ::_thesis: (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1) A9: i + 1 > 1 by A7, NAT_1:13; (i - 1) + 1 >= 1 by A7; then A10: i - 1 >= 1 - 1 by XREAL_1:20; A11: ((i + 1) -' 1) + (p .. f) = ((i + 1) - 1) + (p .. f) by A7, XREAL_0:def_2 .= ((i - 1) + (p .. f)) + 1 .= ((i -' 1) + (p .. f)) + 1 by A10, XREAL_0:def_2 ; A12: i + 1 <= len (Rotate (f,p)) by A8, NAT_1:13; A13: len (Rotate (f,p)) = len f by REVROT_1:14; then A14: len f > 1 by A7, A8, XXREAL_0:2; then A15: len f >= 1 + 1 by NAT_1:13; now__::_thesis:_(Rotate_(f,p))_._i_<>_(Rotate_(f,p))_._(i_+_1) percases ( i < len (f :- p) or i = len (f :- p) or i > len (f :- p) ) by XXREAL_0:1; supposeA16: i < len (f :- p) ; ::_thesis: (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1) then i - 1 < (len f) - (p .. f) by A4, XREAL_1:19; then (i - 1) + (p .. f) < len f by XREAL_1:20; then A17: (i -' 1) + (p .. f) < len f by A10, XREAL_0:def_2; then A18: ((i -' 1) + (p .. f)) + 1 <= len f by NAT_1:13; (Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) by A2, A7, A16, REVROT_1:9 .= f . ((i -' 1) + (p .. f)) by A5, A17, FINSEQ_4:15 ; then A19: (Rotate (f,p)) . i = f . ((i -' 1) + (p .. f)) by A7, A8, FINSEQ_4:15; i + 1 <= len (f :- p) by A16, NAT_1:13; then (Rotate (f,p)) /. (i + 1) = f /. (((i + 1) -' 1) + (p .. f)) by A2, A9, REVROT_1:9 .= f . (((i + 1) -' 1) + (p .. f)) by A6, A11, A18, FINSEQ_4:15 ; then (Rotate (f,p)) . (i + 1) = f . (((i + 1) -' 1) + (p .. f)) by A9, A12, FINSEQ_4:15; hence (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1) by A1, A5, A11, A17, A19, Def2; ::_thesis: verum end; supposeA20: i = len (f :- p) ; ::_thesis: (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1) then (Rotate (f,p)) /. i = f /. (len f) by A2, REVROT_1:11 .= f /. 1 by A1, FINSEQ_6:def_1 .= f . 1 by A14, FINSEQ_4:15 ; then A21: (Rotate (f,p)) . i = f . 1 by A7, A8, FINSEQ_4:15; A22: ((i + 1) + (p .. f)) -' (len f) = ((len f) + (1 + 1)) - (len f) by A4, A20, XREAL_0:def_2 .= 2 ; i + 1 > len (f :- p) by A20, NAT_1:13; then (Rotate (f,p)) /. (i + 1) = f /. (((i + 1) + (p .. f)) -' (len f)) by A2, A13, A12, REVROT_1:12 .= f . (((i + 1) + (p .. f)) -' (len f)) by A15, A22, FINSEQ_4:15 ; then (Rotate (f,p)) . (i + 1) = f . (1 + 1) by A9, A12, A22, FINSEQ_4:15; hence (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1) by A1, A14, A21, Def2; ::_thesis: verum end; supposeA23: i > len (f :- p) ; ::_thesis: (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1) then A24: i - ((len f) - (p .. f)) > 1 by A4, XREAL_1:20; then (i + (p .. f)) - (len f) > 1 - 1 by XXREAL_0:2; then A25: ((i + (p .. f)) - (len f)) + 1 > 1 by XREAL_1:19; then A26: ((i + 1) + (p .. f)) -' (len f) = ((i + 1) + (p .. f)) - (len f) by XREAL_0:def_2 .= ((i + (p .. f)) - (len f)) + 1 .= ((i + (p .. f)) -' (len f)) + 1 by A24, XREAL_0:def_2 ; (i + 1) + (p .. f) <= (len f) + (len f) by A3, A13, A12, XREAL_1:7; then ((i + 1) + (p .. f)) - (len f) <= len f by XREAL_1:20; then A27: ((i + 1) + (p .. f)) -' (len f) <= len f by A25, XREAL_0:def_2; ((i + 1) + (p .. f)) - (len f) > 1 by A25; then A28: ((i + 1) + (p .. f)) -' (len f) > 1 by XREAL_0:def_2; i + 1 > len (f :- p) by A23, NAT_1:13; then (Rotate (f,p)) /. (i + 1) = f /. (((i + 1) + (p .. f)) -' (len f)) by A2, A13, A12, REVROT_1:12 .= f . (((i + 1) + (p .. f)) -' (len f)) by A28, A27, FINSEQ_4:15 ; then A29: (Rotate (f,p)) . (i + 1) = f . (((i + 1) + (p .. f)) -' (len f)) by A9, A12, FINSEQ_4:15; (i + (p .. f)) - (len f) > 1 by A24; then A30: (i + (p .. f)) -' (len f) > 1 by XREAL_0:def_2; i + (p .. f) < (len f) + (len f) by A3, A13, A8, XREAL_1:8; then (i + (p .. f)) - (len f) < len f by XREAL_1:19; then A31: (i + (p .. f)) -' (len f) < len f by A24, XREAL_0:def_2; (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) by A2, A13, A8, A23, REVROT_1:12 .= f . ((i + (p .. f)) -' (len f)) by A30, A31, FINSEQ_4:15 ; then (Rotate (f,p)) . i = f . ((i + (p .. f)) -' (len f)) by A7, A8, FINSEQ_4:15; hence (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1) by A1, A30, A31, A29, A26, Def2; ::_thesis: verum end; end; end; hence (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1) ; ::_thesis: verum end; suppose not p in rng f ; ::_thesis: Rotate (f,p) is weakly-one-to-one hence Rotate (f,p) is weakly-one-to-one by A1, FINSEQ_6:def_2; ::_thesis: verum end; end; end; theorem Th13: :: JORDAN23:13 for D being non empty set for f being FinSequence of D st f is poorly-one-to-one & f is circular holds for p being Element of D holds Rotate (f,p) is poorly-one-to-one proof let D be non empty set ; ::_thesis: for f being FinSequence of D st f is poorly-one-to-one & f is circular holds for p being Element of D holds Rotate (f,p) is poorly-one-to-one let f be FinSequence of D; ::_thesis: ( f is poorly-one-to-one & f is circular implies for p being Element of D holds Rotate (f,p) is poorly-one-to-one ) assume A1: ( f is poorly-one-to-one & f is circular ) ; ::_thesis: for p being Element of D holds Rotate (f,p) is poorly-one-to-one let p be Element of D; ::_thesis: Rotate (f,p) is poorly-one-to-one A2: len (Rotate (f,p)) = len f by REVROT_1:14; percases ( len f <> 2 or len f = 2 ) ; supposeA3: len f <> 2 ; ::_thesis: Rotate (f,p) is poorly-one-to-one then f is weakly-one-to-one by A1, Th7; then Rotate (f,p) is weakly-one-to-one by A1, Th12; hence Rotate (f,p) is poorly-one-to-one by A2, A3, Th7; ::_thesis: verum end; suppose len f = 2 ; ::_thesis: Rotate (f,p) is poorly-one-to-one hence Rotate (f,p) is poorly-one-to-one by A2, Def3; ::_thesis: verum end; end; end; registration let D be non empty set ; cluster non empty V13() V16( NAT ) V17(D) Function-like one-to-one V26() FinSequence-like FinSubsequence-like circular for FinSequence of D; existence ex b1 being FinSequence of D st ( b1 is one-to-one & b1 is circular & not b1 is empty ) proof set x = the Element of D; <* the Element of D*> /. 1 = <* the Element of D*> /. (len <* the Element of D*>) by FINSEQ_1:39; then <* the Element of D*> is circular by FINSEQ_6:def_1; hence ex b1 being FinSequence of D st ( b1 is one-to-one & b1 is circular & not b1 is empty ) ; ::_thesis: verum end; end; registration let D be non empty set ; let f be almost-one-to-one FinSequence of D; let p be Element of D; cluster Rotate (f,p) -> almost-one-to-one ; coherence Rotate (f,p) is almost-one-to-one by Th11; end; registration let D be non empty set ; let f be circular weakly-one-to-one FinSequence of D; let p be Element of D; cluster Rotate (f,p) -> weakly-one-to-one ; coherence Rotate (f,p) is weakly-one-to-one by Th12; end; registration let D be non empty set ; let f be circular poorly-one-to-one FinSequence of D; let p be Element of D; cluster Rotate (f,p) -> poorly-one-to-one ; coherence Rotate (f,p) is poorly-one-to-one by Th13; end; theorem Th14: :: JORDAN23:14 for D being non empty set for f being FinSequence of D holds ( f is almost-one-to-one iff ( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one ) ) proof let D be non empty set ; ::_thesis: for f being FinSequence of D holds ( f is almost-one-to-one iff ( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one ) ) let f be FinSequence of D; ::_thesis: ( f is almost-one-to-one iff ( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one ) ) A1: len (f /^ 1) = (len f) -' 1 by RFINSEQ:29; thus ( f is almost-one-to-one implies ( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one ) ) ::_thesis: ( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one implies f is almost-one-to-one ) proof assume A2: f is almost-one-to-one ; ::_thesis: ( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one ) thus f /^ 1 is one-to-one ::_thesis: f | ((len f) -' 1) is one-to-one proof let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in K74((f /^ 1)) or not y in K74((f /^ 1)) or not (f /^ 1) . x = (f /^ 1) . y or x = y ) assume that A3: x in dom (f /^ 1) and A4: y in dom (f /^ 1) and A5: (f /^ 1) . x = (f /^ 1) . y ; ::_thesis: x = y reconsider i = x, j = y as Element of NAT by A3, A4; A6: i in Seg (len (f /^ 1)) by A3, FINSEQ_1:def_3; then A7: 1 <= i by FINSEQ_1:1; A8: i <= len (f /^ 1) by A6, FINSEQ_1:1; then (len f) -' 1 >= 1 by A1, A7, XXREAL_0:2; then A9: (len f) -' 1 = (len f) - 1 by NAT_D:39; then A10: i + 1 <= len f by A1, A8, XREAL_1:19; then A11: (f /^ 1) . i = f . (i + 1) by A7, FINSEQ_6:114; A12: j in Seg (len (f /^ 1)) by A4, FINSEQ_1:def_3; then A13: 1 <= j by FINSEQ_1:1; j <= len (f /^ 1) by A12, FINSEQ_1:1; then A14: j + 1 <= len f by A1, A9, XREAL_1:19; then A15: (f /^ 1) . j = f . (j + 1) by A13, FINSEQ_6:114; A16: j + 1 > 1 by A13, NAT_1:13; then A17: j + 1 in dom f by A14, FINSEQ_3:25; A18: i + 1 > 1 by A7, NAT_1:13; then i + 1 in dom f by A10, FINSEQ_3:25; then i + 1 = j + 1 by A2, A5, A11, A15, A18, A16, A17, Def1; hence x = y ; ::_thesis: verum end; A19: len (f | ((len f) -' 1)) = (len f) -' 1 by FINSEQ_1:59, NAT_D:35; thus f | ((len f) -' 1) is one-to-one ::_thesis: verum proof let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in K74((f | ((len f) -' 1))) or not y in K74((f | ((len f) -' 1))) or not (f | ((len f) -' 1)) . x = (f | ((len f) -' 1)) . y or x = y ) assume that A20: x in dom (f | ((len f) -' 1)) and A21: y in dom (f | ((len f) -' 1)) and A22: (f | ((len f) -' 1)) . x = (f | ((len f) -' 1)) . y ; ::_thesis: x = y reconsider i = x, j = y as Element of NAT by A20, A21; A23: i in Seg (len (f | ((len f) -' 1))) by A20, FINSEQ_1:def_3; then A24: 1 <= i by FINSEQ_1:1; A25: j in Seg (len (f | ((len f) -' 1))) by A21, FINSEQ_1:def_3; then A26: j <= len (f | ((len f) -' 1)) by FINSEQ_1:1; then A27: (f | ((len f) -' 1)) . j = f . j by A19, FINSEQ_3:112; A28: i <= len (f | ((len f) -' 1)) by A23, FINSEQ_1:1; then A29: (f | ((len f) -' 1)) . i = f . i by A19, FINSEQ_3:112; (len f) -' 1 >= 1 by A19, A24, A28, XXREAL_0:2; then A30: (len f) -' 1 = (len f) - 1 by NAT_D:39; then j + 1 <= len f by A19, A26, XREAL_1:19; then A31: j < len f by NAT_1:13; 1 <= j by A25, FINSEQ_1:1; then A32: j in dom f by A31, FINSEQ_3:25; i + 1 <= len f by A19, A28, A30, XREAL_1:19; then A33: i < len f by NAT_1:13; then i in dom f by A24, FINSEQ_3:25; hence x = y by A2, A22, A29, A27, A33, A31, A32, Def1; ::_thesis: verum end; end; assume that A34: f /^ 1 is one-to-one and A35: f | ((len f) -' 1) is one-to-one ; ::_thesis: f is almost-one-to-one let i, j be Element of NAT ; :: according to JORDAN23:def_1 ::_thesis: ( i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f . i = f . j implies i = j ) assume that A36: i in dom f and A37: j in dom f and A38: ( i <> 1 or j <> len f ) and A39: ( i <> len f or j <> 1 ) and A40: f . i = f . j ; ::_thesis: i = j A41: 0 + 1 <= i by A36, FINSEQ_3:25; then A42: i - 1 >= 0 by XREAL_1:19; A43: i <= len f by A36, FINSEQ_3:25; then A44: i - 1 <= (len f) - 1 by XREAL_1:9; then i -' 1 <= (len f) - 1 by A42, XREAL_0:def_2; then A45: i -' 1 <= (len f) -' 1 by XREAL_0:def_2; len f = ((len f) -' 1) + 1 by A41, A43, XREAL_1:235, XXREAL_0:2; then (len f) -' 1 <= len f by NAT_1:13; then A46: len (f | ((len f) -' 1)) = (len f) -' 1 by FINSEQ_1:59; A47: j <= len f by A37, FINSEQ_3:25; then j - 1 <= (len f) - 1 by XREAL_1:9; then j -' 1 <= (len f) - 1 by A42, A44, XREAL_0:def_2; then A48: j -' 1 <= (len f) -' 1 by XREAL_0:def_2; not f is empty by A36; then A49: f = <*(f /. 1)*> ^ (f /^ 1) by FINSEQ_5:29; A50: i = (i -' 1) + 1 by A41, XREAL_1:235; A51: 0 + 1 <= j by A37, FINSEQ_3:25; then A52: j - 1 >= 0 by XREAL_1:19; A53: j = (j -' 1) + 1 by A51, XREAL_1:235; percases ( ( i <> 1 & j <> 1 ) or i = 1 or j = 1 ) ; supposeA54: ( i <> 1 & j <> 1 ) ; ::_thesis: i = j then j > 0 + 1 by A51, XXREAL_0:1; then j - 1 > 0 by XREAL_1:20; then j -' 1 > 0 by XREAL_0:def_2; then j -' 1 >= 0 + 1 by NAT_1:13; then A55: j -' 1 in dom (f /^ 1) by A1, A48, FINSEQ_3:25; then A56: f . j = (f /^ 1) . (j -' 1) by A53, A49, FINSEQ_3:103; i > 0 + 1 by A41, A54, XXREAL_0:1; then i - 1 > 0 by XREAL_1:20; then i -' 1 > 0 by XREAL_0:def_2; then i -' 1 >= 0 + 1 by NAT_1:13; then A57: i -' 1 in dom (f /^ 1) by A1, A45, FINSEQ_3:25; then f . i = (f /^ 1) . (i -' 1) by A50, A49, FINSEQ_3:103; then i -' 1 = j -' 1 by A34, A40, A57, A55, A56, FUNCT_1:def_4; then i - 1 = j -' 1 by A42, XREAL_0:def_2; then i - 1 = j - 1 by A52, XREAL_0:def_2; hence i = j ; ::_thesis: verum end; supposeA58: i = 1 ; ::_thesis: i = j then j < len f by A38, A47, XXREAL_0:1; then j + 1 <= len f by NAT_1:13; then j <= (len f) - 1 by XREAL_1:19; then A59: j <= (len f) -' 1 by XREAL_0:def_2; then A60: (f | ((len f) -' 1)) . j = f . j by FINSEQ_3:112; i <= (len f) -' 1 by A51, A58, A59, XXREAL_0:2; then A61: i in dom (f | ((len f) -' 1)) by A41, A46, FINSEQ_3:25; A62: j in dom (f | ((len f) -' 1)) by A51, A46, A59, FINSEQ_3:25; (f | ((len f) -' 1)) . i = f . i by A51, A58, A59, FINSEQ_3:112, XXREAL_0:2; hence i = j by A35, A40, A60, A61, A62, FUNCT_1:def_4; ::_thesis: verum end; supposeA63: j = 1 ; ::_thesis: i = j then i < len f by A39, A43, XXREAL_0:1; then i + 1 <= len f by NAT_1:13; then i <= (len f) - 1 by XREAL_1:19; then A64: i <= (len f) -' 1 by XREAL_0:def_2; then A65: (f | ((len f) -' 1)) . i = f . i by FINSEQ_3:112; j <= (len f) -' 1 by A41, A63, A64, XXREAL_0:2; then A66: j in dom (f | ((len f) -' 1)) by A51, A46, FINSEQ_3:25; A67: i in dom (f | ((len f) -' 1)) by A41, A46, A64, FINSEQ_3:25; (f | ((len f) -' 1)) . j = f . j by A41, A63, A64, FINSEQ_3:112, XXREAL_0:2; hence i = j by A35, A40, A65, A67, A66, FUNCT_1:def_4; ::_thesis: verum end; end; end; registration let C be compact non horizontal non vertical Subset of (TOP-REAL 2); let n be Element of NAT ; cluster Cage (C,n) -> almost-one-to-one ; coherence Cage (C,n) is almost-one-to-one proof len (Cage (C,n)) > 0 + 1 by GOBOARD7:34, XXREAL_0:2; then (len (Cage (C,n))) - 1 > 0 by XREAL_1:20; then A1: (len (Cage (C,n))) -' 1 = (len (Cage (C,n))) - 1 by XREAL_0:def_2; A2: len (Cage (C,n)) > 4 by GOBOARD7:34; len (Cage (C,n)) < (len (Cage (C,n))) + 1 by NAT_1:13; then (len (Cage (C,n))) -' 1 < len (Cage (C,n)) by A1, XREAL_1:19; then A3: (Cage (C,n)) | ((len (Cage (C,n))) -' 1) is one-to-one by A2, TOPREAL8:22; (Cage (C,n)) /^ 1 is one-to-one ; hence Cage (C,n) is almost-one-to-one by A3, Th14; ::_thesis: verum end; end; registration let C be compact non horizontal non vertical Subset of (TOP-REAL 2); let n be Element of NAT ; cluster Cage (C,n) -> weakly-one-to-one ; coherence Cage (C,n) is weakly-one-to-one proof len (Cage (C,n)) > 2 by GOBOARD7:34, XXREAL_0:2; hence Cage (C,n) is weakly-one-to-one by Th7; ::_thesis: verum end; end; theorem Th15: :: JORDAN23:15 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f & f is weakly-one-to-one holds B_Cut (f,p,p) = <*p*> proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f & f is weakly-one-to-one holds B_Cut (f,p,p) = <*p*> let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & f is weakly-one-to-one implies B_Cut (f,p,p) = <*p*> ) assume that A1: p in L~ f and A2: f is weakly-one-to-one ; ::_thesis: B_Cut (f,p,p) = <*p*> A3: 1 <= Index (p,f) by A1, JORDAN3:8; (L_Cut (f,p)) . 1 = p by A1, JORDAN3:23; then A4: R_Cut ((L_Cut (f,p)),p) = <*p*> by JORDAN3:def_4; A5: Index (p,f) < len f by A1, JORDAN3:8; then A6: (Index (p,f)) + 1 <= len f by NAT_1:13; then A7: (Index (p,f)) + 1 in dom f by A3, SEQ_4:134; f . (Index (p,f)) <> f . ((Index (p,f)) + 1) by A2, A5, A3, Def2; then A8: f . (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A7, PARTFUN1:def_6; Index (p,f) in dom f by A3, A6, SEQ_4:134; then A9: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A8, PARTFUN1:def_6; p in LSeg (f,(Index (p,f))) by A1, JORDAN3:9; then p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, A6, TOPREAL1:def_3; then LE p,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A9, JORDAN5B:9; hence B_Cut (f,p,p) = <*p*> by A4, JORDAN3:def_7; ::_thesis: verum end; theorem Th16: :: JORDAN23:16 for f being FinSequence st f is one-to-one holds f is weakly-one-to-one proof let f be FinSequence; ::_thesis: ( f is one-to-one implies f is weakly-one-to-one ) assume A1: f is one-to-one ; ::_thesis: f is weakly-one-to-one for i being Element of NAT st 1 <= i & i < len f holds f . i <> f . (i + 1) proof let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies f . i <> f . (i + 1) ) assume that A2: 1 <= i and A3: i < len f ; ::_thesis: f . i <> f . (i + 1) A4: i + 1 in dom f by A2, A3, MSUALG_8:1; A5: i <> i + 1 ; i in dom f by A2, A3, MSUALG_8:1; hence f . i <> f . (i + 1) by A1, A4, A5, FUNCT_1:def_4; ::_thesis: verum end; hence f is weakly-one-to-one by Def2; ::_thesis: verum end; registration clusterV13() Function-like one-to-one FinSequence-like -> weakly-one-to-one for set ; coherence for b1 being FinSequence st b1 is one-to-one holds b1 is weakly-one-to-one by Th16; end; theorem Th17: :: JORDAN23:17 for f being FinSequence of (TOP-REAL 2) st f is weakly-one-to-one holds for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is weakly-one-to-one implies for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) ) assume A1: f is weakly-one-to-one ; ::_thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & q in L~ f implies B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) ) assume that A2: p in L~ f and A3: q in L~ f ; ::_thesis: B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) percases ( p = q or ( p <> q & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) or ( p <> q & not Index (p,f) < Index (q,f) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) ; supposeA4: p = q ; ::_thesis: B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) then B_Cut (f,p,q) = <*p*> by A1, A2, Th15; hence B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) by A4, FINSEQ_5:60; ::_thesis: verum end; supposethat A5: p <> q and A6: ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; ::_thesis: B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) ( not Index (q,f) = Index (p,f) or not LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) ) by A5, A6, JORDAN3:27; then A7: Rev (B_Cut (f,q,p)) = Rev (Rev (R_Cut ((L_Cut (f,p)),q))) by A6, JORDAN3:def_7; B_Cut (f,p,q) = R_Cut ((L_Cut (f,p)),q) by A2, A3, A6, JORDAN3:def_7; hence B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) by A7; ::_thesis: verum end; supposethat p <> q and A8: ( not Index (p,f) < Index (q,f) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; ::_thesis: B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) A9: ( Index (q,f) < Index (p,f) or ( Index (p,f) = Index (q,f) & not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) by A8, XXREAL_0:1; A10: now__::_thesis:_(_Index_(p,f)_=_Index_(q,f)_&_not_LE_p,q,f_/._(Index_(p,f)),f_/._((Index_(p,f))_+_1)_implies_LE_q,p,f_/._(Index_(q,f)),f_/._((Index_(q,f))_+_1)_) assume that A11: Index (p,f) = Index (q,f) and A12: not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ; ::_thesis: LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) A13: 1 <= Index (p,f) by A2, JORDAN3:8; A14: Index (p,f) < len f by A2, JORDAN3:8; then A15: (Index (p,f)) + 1 <= len f by NAT_1:13; then A16: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A13, TOPREAL1:def_3; then A17: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, JORDAN3:9; 1 <= (Index (p,f)) + 1 by NAT_1:11; then A18: (Index (p,f)) + 1 in dom f by A15, FINSEQ_3:25; f . (Index (p,f)) <> f . ((Index (p,f)) + 1) by A1, A13, A14, Def2; then A19: f . (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A18, PARTFUN1:def_6; Index (p,f) in dom f by A13, A14, FINSEQ_3:25; then A20: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A19, PARTFUN1:def_6; q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, A11, A16, JORDAN3:9; then LT q,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A12, A17, A20, JORDAN3:28; hence LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) by A11, JORDAN3:def_6; ::_thesis: verum end; B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) by A8, JORDAN3:def_7; hence B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) by A2, A3, A9, A10, JORDAN3:def_7; ::_thesis: verum end; end; end; theorem Th18: :: JORDAN23:18 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for i1 being Element of NAT st f is poorly-one-to-one & f is unfolded & f is s.n.c. & 1 < i1 & i1 <= len f & p = f . i1 holds (Index (p,f)) + 1 = i1 proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) for i1 being Element of NAT st f is poorly-one-to-one & f is unfolded & f is s.n.c. & 1 < i1 & i1 <= len f & p = f . i1 holds (Index (p,f)) + 1 = i1 let p be Point of (TOP-REAL 2); ::_thesis: for i1 being Element of NAT st f is poorly-one-to-one & f is unfolded & f is s.n.c. & 1 < i1 & i1 <= len f & p = f . i1 holds (Index (p,f)) + 1 = i1 let i1 be Element of NAT ; ::_thesis: ( f is poorly-one-to-one & f is unfolded & f is s.n.c. & 1 < i1 & i1 <= len f & p = f . i1 implies (Index (p,f)) + 1 = i1 ) assume A1: ( f is poorly-one-to-one & f is unfolded & f is s.n.c. ) ; ::_thesis: ( not 1 < i1 or not i1 <= len f or not p = f . i1 or (Index (p,f)) + 1 = i1 ) assume that A2: 1 < i1 and A3: i1 <= len f ; ::_thesis: ( not p = f . i1 or (Index (p,f)) + 1 = i1 ) consider j being Nat such that A4: i1 = j + 1 by A2, NAT_1:6; reconsider j = j as Element of NAT by ORDINAL1:def_12; A5: 1 + 0 <= j by A2, A4, NAT_1:13; assume A6: p = f . i1 ; ::_thesis: (Index (p,f)) + 1 = i1 assume A7: (Index (p,f)) + 1 <> i1 ; ::_thesis: contradiction i1 in dom f by A2, A3, FINSEQ_3:25; then p = f /. i1 by A6, PARTFUN1:def_6; then A8: p in LSeg (f,j) by A3, A4, A5, TOPREAL1:21; then Index (p,f) <= j by JORDAN3:7; then Index (p,f) < j by A4, A7, XXREAL_0:1; then A9: (Index (p,f)) + 1 <= j by NAT_1:13; A10: LSeg (f,j) c= L~ f by TOPREAL3:19; then A11: p in LSeg (f,(Index (p,f))) by A8, JORDAN3:9; percases ( (Index (p,f)) + 1 = j or (Index (p,f)) + 1 < j ) by A9, XXREAL_0:1; supposeA12: (Index (p,f)) + 1 = j ; ::_thesis: contradiction A13: 1 <= Index (p,f) by A8, A10, JORDAN3:8; then (Index (p,f)) + 2 >= 1 + 2 by XREAL_1:7; then len f >= 2 + 1 by A3, A4, A12, XXREAL_0:2; then A14: len f > 2 by NAT_1:13; (Index (p,f)) + (1 + 1) <= len f by A3, A4, A12; then (LSeg (f,(Index (p,f)))) /\ (LSeg (f,j)) = {(f /. j)} by A1, A12, A13, TOPREAL1:def_6; then A15: p in {(f /. j)} by A8, A11, XBOOLE_0:def_4; A16: j < len f by A3, A4, NAT_1:13; then j in dom f by A5, FINSEQ_3:25; then f . j = f /. j by PARTFUN1:def_6 .= f . i1 by A6, A15, TARSKI:def_1 ; hence contradiction by A1, A4, A5, A16, A14, Def3; ::_thesis: verum end; supposeA17: (Index (p,f)) + 1 < j ; ::_thesis: contradiction p in (LSeg (f,(Index (p,f)))) /\ (LSeg (f,j)) by A8, A11, XBOOLE_0:def_4; then LSeg (f,(Index (p,f))) meets LSeg (f,j) by XBOOLE_0:4; hence contradiction by A1, A17, TOPREAL1:def_7; ::_thesis: verum end; end; end; theorem Th19: :: JORDAN23:19 for f being FinSequence of (TOP-REAL 2) st f is weakly-one-to-one holds for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds (B_Cut (f,p,q)) /. 1 = p proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is weakly-one-to-one implies for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds (B_Cut (f,p,q)) /. 1 = p ) assume A1: f is weakly-one-to-one ; ::_thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds (B_Cut (f,p,q)) /. 1 = p let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & q in L~ f implies (B_Cut (f,p,q)) /. 1 = p ) assume that A2: p in L~ f and A3: q in L~ f ; ::_thesis: (B_Cut (f,p,q)) /. 1 = p A4: Index (p,f) < len f by A2, JORDAN3:8; A5: 1 <= Index (p,f) by A2, JORDAN3:8; then A6: Index (p,f) in dom f by A4, FINSEQ_3:25; A7: 1 <= len (L_Cut (f,p)) by A2, Th1; percases ( p <> q or p = q ) ; supposeA8: p <> q ; ::_thesis: (B_Cut (f,p,q)) /. 1 = p now__::_thesis:_(B_Cut_(f,p,q))_/._1_=_p percases ( ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) or ( ( not p in L~ f or not q in L~ f or not Index (p,f) < Index (q,f) ) & ( not Index (p,f) = Index (q,f) or not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) ; supposeA9: ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) ; ::_thesis: (B_Cut (f,p,q)) /. 1 = p then q in L~ (L_Cut (f,p)) by JORDAN3:29; then (R_Cut ((L_Cut (f,p)),q)) /. 1 = (L_Cut (f,p)) /. 1 by SPRECT_3:22 .= (L_Cut (f,p)) . 1 by A7, FINSEQ_4:15 .= p by A9, JORDAN3:23 ; hence (B_Cut (f,p,q)) /. 1 = p by A9, JORDAN3:def_7; ::_thesis: verum end; supposeA10: ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ; ::_thesis: (B_Cut (f,p,q)) /. 1 = p then q in L~ (L_Cut (f,p)) by A2, A3, A8, JORDAN3:31; then (R_Cut ((L_Cut (f,p)),q)) /. 1 = (L_Cut (f,p)) /. 1 by SPRECT_3:22 .= (L_Cut (f,p)) . 1 by A7, FINSEQ_4:15 .= p by A2, JORDAN3:23 ; hence (B_Cut (f,p,q)) /. 1 = p by A10, JORDAN3:def_7; ::_thesis: verum end; supposeA11: ( ( not p in L~ f or not q in L~ f or not Index (p,f) < Index (q,f) ) & ( not Index (p,f) = Index (q,f) or not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; ::_thesis: (B_Cut (f,p,q)) /. 1 = p then A12: B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) by JORDAN3:def_7; now__::_thesis:_(B_Cut_(f,p,q))_/._1_=_p percases ( Index (p,f) > Index (q,f) or Index (p,f) = Index (q,f) ) by A2, A3, A11, XXREAL_0:1; suppose Index (p,f) > Index (q,f) ; ::_thesis: (B_Cut (f,p,q)) /. 1 = p then A13: p in L~ (L_Cut (f,q)) by A2, A3, JORDAN3:29; R_Cut ((L_Cut (f,q)),p) <> {} by JORDAN1J:44; hence (B_Cut (f,p,q)) /. 1 = (R_Cut ((L_Cut (f,q)),p)) /. (len (R_Cut ((L_Cut (f,q)),p))) by A12, FINSEQ_5:65 .= p by A13, JORDAN1J:45 ; ::_thesis: verum end; supposeA14: Index (p,f) = Index (q,f) ; ::_thesis: (B_Cut (f,p,q)) /. 1 = p A15: (Index (p,f)) + 1 >= 1 by NAT_1:11; (Index (p,f)) + 1 <= len f by A4, NAT_1:13; then A16: (Index (p,f)) + 1 in dom f by A15, FINSEQ_3:25; set Ls = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))); A17: q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, A14, JORDAN5B:29; A18: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, JORDAN5B:29; f . (Index (p,f)) <> f . ((Index (p,f)) + 1) by A1, A5, A4, Def2; then f . (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A16, PARTFUN1:def_6; then A19: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A6, PARTFUN1:def_6; then A20: LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) is_an_arc_of f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by TOPREAL1:9; not LE p,q, LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))),f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A11, A14, A19, JORDAN5C:17; then LE q,p, LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))),f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A8, A20, A18, A17, JORDAN5C:14; then A21: p in L~ (L_Cut (f,q)) by A2, A3, A8, A14, A19, JORDAN3:31, JORDAN5C:17; R_Cut ((L_Cut (f,q)),p) <> {} by JORDAN1J:44; hence (B_Cut (f,p,q)) /. 1 = (R_Cut ((L_Cut (f,q)),p)) /. (len (R_Cut ((L_Cut (f,q)),p))) by A12, FINSEQ_5:65 .= p by A21, JORDAN1J:45 ; ::_thesis: verum end; end; end; hence (B_Cut (f,p,q)) /. 1 = p ; ::_thesis: verum end; end; end; hence (B_Cut (f,p,q)) /. 1 = p ; ::_thesis: verum end; suppose p = q ; ::_thesis: (B_Cut (f,p,q)) /. 1 = p then B_Cut (f,p,q) = <*p*> by A1, A2, Th15; hence (B_Cut (f,p,q)) /. 1 = p by FINSEQ_4:16; ::_thesis: verum end; end; end; theorem Th20: :: JORDAN23:20 for f being FinSequence of (TOP-REAL 2) st f is weakly-one-to-one holds for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds (B_Cut (f,p,q)) /. (len (B_Cut (f,p,q))) = q proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is weakly-one-to-one implies for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds (B_Cut (f,p,q)) /. (len (B_Cut (f,p,q))) = q ) assume A1: f is weakly-one-to-one ; ::_thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds (B_Cut (f,p,q)) /. (len (B_Cut (f,p,q))) = q let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & q in L~ f implies (B_Cut (f,p,q)) /. (len (B_Cut (f,p,q))) = q ) assume that A2: p in L~ f and A3: q in L~ f ; ::_thesis: (B_Cut (f,p,q)) /. (len (B_Cut (f,p,q))) = q A4: B_Cut (f,q,p) <> {} by Th3; B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) by A1, A2, A3, Th17; hence (B_Cut (f,p,q)) /. (len (B_Cut (f,p,q))) = (Rev (B_Cut (f,q,p))) /. (len (B_Cut (f,q,p))) by FINSEQ_5:def_3 .= (B_Cut (f,q,p)) /. 1 by A4, FINSEQ_5:65 .= q by A1, A2, A3, Th19 ; ::_thesis: verum end; theorem :: JORDAN23:21 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f holds L~ (L_Cut (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 L~ f holds L~ (L_Cut (f,p)) c= L~ f let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies L~ (L_Cut (f,p)) c= L~ f ) assume A1: p in L~ f ; ::_thesis: L~ (L_Cut (f,p)) c= L~ f Index (p,f) < len f by A1, JORDAN3:8; then A2: (Index (p,f)) + 1 <= len f by NAT_1:13; len f <> 0 by A1, TOPREAL1:22; then len f > 0 by NAT_1:3; then A3: len f >= 0 + 1 by NAT_1:13; then A4: len f in dom f by FINSEQ_3:25; A5: 1 <= Index (p,f) by A1, JORDAN3:8; then A6: 1 < (Index (p,f)) + 1 by NAT_1:13; then A7: (Index (p,f)) + 1 in dom f by A2, FINSEQ_3:25; percases ( p = f . ((Index (p,f)) + 1) or p <> f . ((Index (p,f)) + 1) ) ; suppose p = f . ((Index (p,f)) + 1) ; ::_thesis: L~ (L_Cut (f,p)) c= L~ f then L_Cut (f,p) = mid (f,((Index (p,f)) + 1),(len f)) by JORDAN3:def_3; hence L~ (L_Cut (f,p)) c= L~ f by A3, A6, A2, JORDAN4:35; ::_thesis: verum end; suppose p <> f . ((Index (p,f)) + 1) ; ::_thesis: L~ (L_Cut (f,p)) c= L~ f then A8: L_Cut (f,p) = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) by JORDAN3:def_3; A9: f /. ((Index (p,f)) + 1) in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by RLTOPSP1:68; p in LSeg (f,(Index (p,f))) by A1, JORDAN3:9; then A10: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A5, A2, TOPREAL1:def_3; A11: LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) c= L~ f by A1, A2, JORDAN3:8, SPPOL_2:16; (mid (f,((Index (p,f)) + 1),(len f))) /. 1 = f /. ((Index (p,f)) + 1) by A4, A7, SPRECT_2:8; then LSeg (p,((mid (f,((Index (p,f)) + 1),(len f))) /. 1)) c= LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A10, A9, TOPREAL1:6; then A12: LSeg (p,((mid (f,((Index (p,f)) + 1),(len f))) /. 1)) c= L~ f by A11, XBOOLE_1:1; len (mid (f,((Index (p,f)) + 1),(len f))) >= 0 + 1 by A4, A7, SPRECT_2:5; then mid (f,((Index (p,f)) + 1),(len f)) <> {} ; then A13: L~ (<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))) = (LSeg (p,((mid (f,((Index (p,f)) + 1),(len f))) /. 1))) \/ (L~ (mid (f,((Index (p,f)) + 1),(len f)))) by SPPOL_2:20; L~ (mid (f,((Index (p,f)) + 1),(len f))) c= L~ f by A3, A6, A2, JORDAN4:35; hence L~ (L_Cut (f,p)) c= L~ f by A8, A13, A12, XBOOLE_1:8; ::_thesis: verum end; end; end; theorem :: JORDAN23:22 for f being FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & f is weakly-one-to-one holds L~ (B_Cut (f,p,q)) c= L~ f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & f is weakly-one-to-one holds L~ (B_Cut (f,p,q)) c= L~ f let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & q in L~ f & f is weakly-one-to-one implies L~ (B_Cut (f,p,q)) c= L~ f ) assume that A1: p in L~ f and A2: q in L~ f and A3: f is weakly-one-to-one ; ::_thesis: L~ (B_Cut (f,p,q)) c= L~ f percases ( p = q or ( p <> q & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) or ( p <> q & not Index (p,f) < Index (q,f) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) ; suppose p = q ; ::_thesis: L~ (B_Cut (f,p,q)) c= L~ f then B_Cut (f,p,q) = <*p*> by A1, A3, Th15; then len (B_Cut (f,p,q)) = 1 by FINSEQ_1:39; then L~ (B_Cut (f,p,q)) = {} by TOPREAL1:22; hence L~ (B_Cut (f,p,q)) c= L~ f by XBOOLE_1:2; ::_thesis: verum end; suppose ( p <> q & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) ; ::_thesis: L~ (B_Cut (f,p,q)) c= L~ f hence L~ (B_Cut (f,p,q)) c= L~ f by A1, A2, JORDAN5B:33; ::_thesis: verum end; supposethat A4: p <> q and A5: ( not Index (p,f) < Index (q,f) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; ::_thesis: L~ (B_Cut (f,p,q)) c= L~ f A6: now__::_thesis:_(_Index_(p,f)_=_Index_(q,f)_&_not_LE_p,q,f_/._(Index_(p,f)),f_/._((Index_(p,f))_+_1)_implies_LE_q,p,f_/._(Index_(q,f)),f_/._((Index_(q,f))_+_1)_) assume that A7: Index (p,f) = Index (q,f) and A8: not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ; ::_thesis: LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) A9: Index (p,f) < len f by A1, JORDAN3:8; A10: 1 <= Index (p,f) by A1, JORDAN3:8; then A11: Index (p,f) in dom f by A9, FINSEQ_3:25; A12: (Index (p,f)) + 1 <= len f by A9, NAT_1:13; then A13: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A10, TOPREAL1:def_3; then A14: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A1, JORDAN3:9; f . (Index (p,f)) <> f . ((Index (p,f)) + 1) by A3, A10, A9, Def2; then A15: f /. (Index (p,f)) <> f . ((Index (p,f)) + 1) by A11, PARTFUN1:def_6; 1 <= (Index (p,f)) + 1 by NAT_1:11; then (Index (p,f)) + 1 in dom f by A12, FINSEQ_3:25; then A16: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A15, PARTFUN1:def_6; q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, A7, A13, JORDAN3:9; then LT q,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A8, A14, A16, JORDAN3:28; hence LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) by A7, JORDAN3:def_6; ::_thesis: verum end; A17: ( Index (q,f) < Index (p,f) or ( Index (p,f) = Index (q,f) & not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) by A5, XXREAL_0:1; then A18: L~ (B_Cut (f,q,p)) c= L~ f by A1, A2, A4, A6, JORDAN5B:33; B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) by A5, JORDAN3:def_7; then Rev (B_Cut (f,q,p)) = B_Cut (f,p,q) by A1, A2, A17, A6, JORDAN3:def_7; hence L~ (B_Cut (f,p,q)) c= L~ f by A18, SPPOL_2:22; ::_thesis: verum end; end; end; theorem Th23: :: JORDAN23:23 for f, g being FinSequence holds dom f c= dom (f ^' g) proof let f, g be FinSequence; ::_thesis: dom f c= dom (f ^' g) len f <= len (f ^' g) by TOPREAL8:7; hence dom f c= dom (f ^' g) by FINSEQ_3:30; ::_thesis: verum end; theorem :: JORDAN23:24 for f being non empty FinSequence for g being FinSequence holds dom g c= dom (f ^' g) proof let f be non empty FinSequence; ::_thesis: for g being FinSequence holds dom g c= dom (f ^' g) let g be FinSequence; ::_thesis: dom g c= dom (f ^' g) len g <= len (f ^' g) by TOPREAL8:9; hence dom g c= dom (f ^' g) by FINSEQ_3:30; ::_thesis: verum end; theorem Th25: :: JORDAN23:25 for f, g being FinSequence st f ^' g is constant holds f is constant proof let f, g be FinSequence; ::_thesis: ( f ^' g is constant implies f is constant ) assume f ^' g is constant ; ::_thesis: f is constant then reconsider h = f ^' g as constant FinSequence ; rng f c= rng h by TOPREAL8:10; hence f is constant ; ::_thesis: verum end; theorem :: JORDAN23:26 for f, g being FinSequence st f ^' g is constant & f . (len f) = g . 1 & f <> {} holds g is constant proof let f, g be FinSequence; ::_thesis: ( f ^' g is constant & f . (len f) = g . 1 & f <> {} implies g is constant ) assume that A1: f ^' g is constant and A2: f . (len f) = g . 1 and A3: f <> {} ; ::_thesis: g is constant reconsider h = f ^' g as constant FinSequence by A1; percases ( g <> {} or g = {} ) ; suppose g <> {} ; ::_thesis: g is constant then rng h = (rng f) \/ (rng g) by A2, A3, GRAPH_2:18; then rng g c= rng h by XBOOLE_1:7; hence g is constant ; ::_thesis: verum end; suppose g = {} ; ::_thesis: g is constant hence g is constant ; ::_thesis: verum end; end; end; theorem Th27: :: JORDAN23:27 for f being special FinSequence of (TOP-REAL 2) for i, j being Element of NAT holds mid (f,i,j) is special proof let f be special FinSequence of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT holds mid (f,i,j) is special let i, j be Element of NAT ; ::_thesis: mid (f,i,j) is special percases ( i <= j or j < i ) ; suppose i <= j ; ::_thesis: mid (f,i,j) is special then mid (f,i,j) = (f /^ (i -' 1)) | ((j -' i) + 1) by FINSEQ_6:def_3; hence mid (f,i,j) is special ; ::_thesis: verum end; suppose j < i ; ::_thesis: mid (f,i,j) is special then mid (f,j,i) = (f /^ (j -' 1)) | ((i -' j) + 1) by FINSEQ_6:def_3; then Rev (mid (f,i,j)) is special by JORDAN4:18; then Rev (Rev (mid (f,i,j))) is special by SPPOL_2:40; hence mid (f,i,j) is special ; ::_thesis: verum end; end; end; theorem Th28: :: JORDAN23:28 for f being unfolded FinSequence of (TOP-REAL 2) for i, j being Element of NAT holds mid (f,i,j) is unfolded proof let f be unfolded FinSequence of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT holds mid (f,i,j) is unfolded let i, j be Element of NAT ; ::_thesis: mid (f,i,j) is unfolded percases ( i <= j or j < i ) ; suppose i <= j ; ::_thesis: mid (f,i,j) is unfolded then mid (f,i,j) = (f /^ (i -' 1)) | ((j -' i) + 1) by FINSEQ_6:def_3; hence mid (f,i,j) is unfolded ; ::_thesis: verum end; suppose j < i ; ::_thesis: mid (f,i,j) is unfolded then mid (f,j,i) = (f /^ (j -' 1)) | ((i -' j) + 1) by FINSEQ_6:def_3; then Rev (mid (f,i,j)) is unfolded by JORDAN4:18; then Rev (Rev (mid (f,i,j))) is unfolded by SPPOL_2:28; hence mid (f,i,j) is unfolded ; ::_thesis: verum end; end; end; theorem Th29: :: JORDAN23:29 for f being FinSequence of (TOP-REAL 2) st f is special holds for p being Point of (TOP-REAL 2) st p in L~ f holds L_Cut (f,p) is special proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is special implies for p being Point of (TOP-REAL 2) st p in L~ f holds L_Cut (f,p) is special ) assume A1: f is special ; ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds L_Cut (f,p) is special let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies L_Cut (f,p) is special ) A2: mid (f,((Index (p,f)) + 1),(len f)) is special by A1, Th27; A3: <*p*> /. 1 = p by FINSEQ_4:16; assume A4: p in L~ f ; ::_thesis: L_Cut (f,p) is special then Index (p,f) < len f by JORDAN3:8; then A5: (Index (p,f)) + 1 <= len f by NAT_1:13; 1 <= Index (p,f) by A4, JORDAN3:8; then A6: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A5, TOPREAL1:def_3; A7: now__::_thesis:_(_(_LSeg_(f,(Index_(p,f)))_is_vertical_&_p_`1_=_(f_/._((Index_(p,f))_+_1))_`1_)_or_(_LSeg_(f,(Index_(p,f)))_is_horizontal_&_p_`2_=_(f_/._((Index_(p,f))_+_1))_`2_)_) percases ( LSeg (f,(Index (p,f))) is vertical or LSeg (f,(Index (p,f))) is horizontal ) by A1, SPPOL_1:19; case LSeg (f,(Index (p,f))) is vertical ; ::_thesis: p `1 = (f /. ((Index (p,f)) + 1)) `1 hence p `1 = (f /. ((Index (p,f)) + 1)) `1 by A4, A6, JORDAN5B:29, SPPOL_1:41; ::_thesis: verum end; case LSeg (f,(Index (p,f))) is horizontal ; ::_thesis: p `2 = (f /. ((Index (p,f)) + 1)) `2 hence p `2 = (f /. ((Index (p,f)) + 1)) `2 by A4, A6, JORDAN5B:29, SPPOL_1:40; ::_thesis: verum end; end; end; A8: len <*p*> = 1 by FINSEQ_1:39; len f <> 0 by A4, TOPREAL1:22; then len f > 0 by NAT_1:3; then len f >= 0 + 1 by NAT_1:13; then A9: len f in dom f by FINSEQ_3:25; (Index (p,f)) + 1 >= 1 by NAT_1:11; then (Index (p,f)) + 1 in dom f by A5, FINSEQ_3:25; then A10: (mid (f,((Index (p,f)) + 1),(len f))) /. 1 = f /. ((Index (p,f)) + 1) by A9, SPRECT_2:8; percases ( p <> f . ((Index (p,f)) + 1) or p = f . ((Index (p,f)) + 1) ) ; suppose p <> f . ((Index (p,f)) + 1) ; ::_thesis: L_Cut (f,p) is special then L_Cut (f,p) = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) by JORDAN3:def_3; hence L_Cut (f,p) is special by A2, A8, A3, A10, A7, GOBOARD2:8; ::_thesis: verum end; suppose p = f . ((Index (p,f)) + 1) ; ::_thesis: L_Cut (f,p) is special hence L_Cut (f,p) is special by A2, JORDAN3:def_3; ::_thesis: verum end; end; end; theorem Th30: :: JORDAN23:30 for f being FinSequence of (TOP-REAL 2) st f is special holds for p being Point of (TOP-REAL 2) st p in L~ f holds R_Cut (f,p) is special proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is special implies for p being Point of (TOP-REAL 2) st p in L~ f holds R_Cut (f,p) is special ) assume A1: f is special ; ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds R_Cut (f,p) is special let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies R_Cut (f,p) is special ) A2: mid (f,1,(Index (p,f))) is special by A1, Th27; assume A3: p in L~ f ; ::_thesis: R_Cut (f,p) is special then A4: Index (p,f) < len f by JORDAN3:8; len f <> 0 by A3, TOPREAL1:22; then len f > 0 by NAT_1:3; then len f >= 0 + 1 by NAT_1:13; then A5: 1 in dom f by FINSEQ_3:25; A6: 1 <= Index (p,f) by A3, JORDAN3:8; then Index (p,f) in dom f by A4, FINSEQ_3:25; then A7: (mid (f,1,(Index (p,f)))) /. (len (mid (f,1,(Index (p,f))))) = f /. (Index (p,f)) by A5, SPRECT_2:9; (Index (p,f)) + 1 <= len f by A4, NAT_1:13; then A8: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A6, TOPREAL1:def_3; A9: now__::_thesis:_(_(_LSeg_(f,(Index_(p,f)))_is_vertical_&_p_`1_=_(f_/._(Index_(p,f)))_`1_)_or_(_LSeg_(f,(Index_(p,f)))_is_horizontal_&_p_`2_=_(f_/._(Index_(p,f)))_`2_)_) percases ( LSeg (f,(Index (p,f))) is vertical or LSeg (f,(Index (p,f))) is horizontal ) by A1, SPPOL_1:19; case LSeg (f,(Index (p,f))) is vertical ; ::_thesis: p `1 = (f /. (Index (p,f))) `1 hence p `1 = (f /. (Index (p,f))) `1 by A3, A8, JORDAN5B:29, SPPOL_1:41; ::_thesis: verum end; case LSeg (f,(Index (p,f))) is horizontal ; ::_thesis: p `2 = (f /. (Index (p,f))) `2 hence p `2 = (f /. (Index (p,f))) `2 by A3, A8, JORDAN5B:29, SPPOL_1:40; ::_thesis: verum end; end; end; A10: <*p*> /. 1 = p by FINSEQ_4:16; A11: <*p*> is special ; percases ( p <> f . 1 or p = f . 1 ) ; suppose p <> f . 1 ; ::_thesis: R_Cut (f,p) is special then R_Cut (f,p) = (mid (f,1,(Index (p,f)))) ^ <*p*> by JORDAN3:def_4; hence R_Cut (f,p) is special by A2, A10, A7, A9, GOBOARD2:8; ::_thesis: verum end; suppose p = f . 1 ; ::_thesis: R_Cut (f,p) is special hence R_Cut (f,p) is special by A11, JORDAN3:def_4; ::_thesis: verum end; end; end; theorem :: JORDAN23:31 for f being FinSequence of (TOP-REAL 2) st f is special & f is weakly-one-to-one holds for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds B_Cut (f,p,q) is special proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is special & f is weakly-one-to-one implies for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds B_Cut (f,p,q) is special ) assume A1: ( f is special & f is weakly-one-to-one ) ; ::_thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds B_Cut (f,p,q) is special let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & q in L~ f implies B_Cut (f,p,q) is special ) assume that A2: p in L~ f and A3: q in L~ f ; ::_thesis: B_Cut (f,p,q) is special A4: Index (p,f) < len f by A2, JORDAN3:8; A5: 1 <= Index (p,f) by A2, JORDAN3:8; then A6: Index (p,f) in dom f by A4, FINSEQ_3:25; percases ( p <> q or p = q ) ; supposeA7: p <> q ; ::_thesis: B_Cut (f,p,q) is special now__::_thesis:_B_Cut_(f,p,q)_is_special percases ( ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) or ( not ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) ; supposeA8: ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) ; ::_thesis: B_Cut (f,p,q) is special then A9: q in L~ (L_Cut (f,p)) by JORDAN3:29; L_Cut (f,p) is special by A1, A2, Th29; then R_Cut ((L_Cut (f,p)),q) is special by A9, Th30; hence B_Cut (f,p,q) is special by A8, JORDAN3:def_7; ::_thesis: verum end; supposeA10: ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ; ::_thesis: B_Cut (f,p,q) is special A11: L_Cut (f,p) is special by A1, A2, Th29; q in L~ (L_Cut (f,p)) by A2, A3, A7, A10, JORDAN3:31; then R_Cut ((L_Cut (f,p)),q) is special by A11, Th30; hence B_Cut (f,p,q) is special by A10, JORDAN3:def_7; ::_thesis: verum end; supposeA12: ( not ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; ::_thesis: B_Cut (f,p,q) is special A13: now__::_thesis:_p_in_L~_(L_Cut_(f,q)) percases ( Index (q,f) < Index (p,f) or Index (q,f) = Index (p,f) ) by A2, A3, A12, XXREAL_0:1; suppose Index (q,f) < Index (p,f) ; ::_thesis: p in L~ (L_Cut (f,q)) hence p in L~ (L_Cut (f,q)) by A2, A3, JORDAN3:29; ::_thesis: verum end; supposeA14: Index (q,f) = Index (p,f) ; ::_thesis: p in L~ (L_Cut (f,q)) A15: (Index (p,f)) + 1 >= 1 by NAT_1:11; (Index (p,f)) + 1 <= len f by A4, NAT_1:13; then A16: (Index (p,f)) + 1 in dom f by A15, FINSEQ_3:25; set Ls = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))); A17: q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, A14, JORDAN5B:29; A18: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, JORDAN5B:29; f . (Index (p,f)) <> f . ((Index (p,f)) + 1) by A1, A5, A4, Def2; then f . (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A16, PARTFUN1:def_6; then A19: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A6, PARTFUN1:def_6; then A20: LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) is_an_arc_of f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by TOPREAL1:9; not LE p,q, LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))),f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A12, A14, A19, JORDAN5C:17; then LE q,p, LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))),f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A7, A20, A18, A17, JORDAN5C:14; hence p in L~ (L_Cut (f,q)) by A2, A3, A7, A14, A19, JORDAN3:31, JORDAN5C:17; ::_thesis: verum end; end; end; A21: B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) by A12, JORDAN3:def_7; L_Cut (f,q) is special by A1, A3, Th29; then R_Cut ((L_Cut (f,q)),p) is special by A13, Th30; hence B_Cut (f,p,q) is special by A21, SPPOL_2:40; ::_thesis: verum end; end; end; hence B_Cut (f,p,q) is special ; ::_thesis: verum end; suppose p = q ; ::_thesis: B_Cut (f,p,q) is special then B_Cut (f,p,q) = <*p*> by A1, A2, Th15; hence B_Cut (f,p,q) is special ; ::_thesis: verum end; end; end; theorem Th32: :: JORDAN23:32 for f being FinSequence of (TOP-REAL 2) st f is unfolded holds for p being Point of (TOP-REAL 2) st p in L~ f holds L_Cut (f,p) is unfolded proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is unfolded implies for p being Point of (TOP-REAL 2) st p in L~ f holds L_Cut (f,p) is unfolded ) assume A1: f is unfolded ; ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds L_Cut (f,p) is unfolded let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies L_Cut (f,p) is unfolded ) A2: mid (f,((Index (p,f)) + 1),(len f)) is unfolded by A1, Th28; assume A3: p in L~ f ; ::_thesis: L_Cut (f,p) is unfolded then A4: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by JORDAN5B:29; Index (p,f) < len f by A3, JORDAN3:8; then A5: ((Index (p,f)) + 1) + 0 <= len f by NAT_1:13; len f <> 0 by A3, TOPREAL1:22; then len f > 0 by NAT_1:3; then A6: len f >= 0 + 1 by NAT_1:13; then A7: len f in dom f by FINSEQ_3:25; A8: 1 <= Index (p,f) by A3, JORDAN3:8; then A9: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A5, TOPREAL1:def_3; A10: 1 < (Index (p,f)) + 1 by A8, NAT_1:13; then A11: (Index (p,f)) + 1 in dom f by A5, FINSEQ_3:25; then A12: (mid (f,((Index (p,f)) + 1),(len f))) /. 1 = f /. ((Index (p,f)) + 1) by A7, SPRECT_2:8; percases ( ((Index (p,f)) + 1) + 1 <= len f or ((Index (p,f)) + 1) + 1 > len f ) ; supposeA13: ((Index (p,f)) + 1) + 1 <= len f ; ::_thesis: L_Cut (f,p) is unfolded then LSeg (f,((Index (p,f)) + 1)) = LSeg ((f /. ((Index (p,f)) + 1)),(f /. ((Index (p,f)) + (1 + 1)))) by A10, TOPREAL1:def_3; then A14: (LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1)))) /\ (LSeg ((f /. ((Index (p,f)) + 1)),(f /. ((Index (p,f)) + (1 + 1))))) = {(f /. ((Index (p,f)) + 1))} by A1, A8, A9, A13, TOPREAL1:def_6; A15: (len f) - ((Index (p,f)) + 1) >= 0 by A5, XREAL_1:19; (Index (p,f)) + (1 + 1) <= len f by A13; then A16: 2 <= (len f) - (Index (p,f)) by XREAL_1:19; A17: f /. ((Index (p,f)) + 1) in LSeg ((f /. ((Index (p,f)) + 1)),(f /. ((Index (p,f)) + (1 + 1)))) by RLTOPSP1:68; f /. ((Index (p,f)) + 1) in LSeg (p,(f /. ((Index (p,f)) + 1))) by RLTOPSP1:68; then f /. ((Index (p,f)) + 1) in (LSeg (p,(f /. ((Index (p,f)) + 1)))) /\ (LSeg ((f /. ((Index (p,f)) + 1)),(f /. ((Index (p,f)) + (1 + 1))))) by A17, XBOOLE_0:def_4; then A18: {(f /. ((Index (p,f)) + 1))} c= (LSeg (p,(f /. ((Index (p,f)) + 1)))) /\ (LSeg ((f /. ((Index (p,f)) + 1)),(f /. ((Index (p,f)) + (1 + 1))))) by ZFMISC_1:31; (2 + ((Index (p,f)) + 1)) - 1 = ((Index (p,f)) + 1) + 1 ; then A19: (2 + ((Index (p,f)) + 1)) - 1 >= 0 by NAT_1:2; A20: len (mid (f,((Index (p,f)) + 1),(len f))) = ((len f) -' ((Index (p,f)) + 1)) + 1 by A6, A10, A5, FINSEQ_6:118 .= ((len f) - ((Index (p,f)) + 1)) + 1 by A15, XREAL_0:def_2 .= (len f) - (Index (p,f)) ; then 2 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A16, FINSEQ_3:25; then (mid (f,((Index (p,f)) + 1),(len f))) /. 2 = f /. ((2 + ((Index (p,f)) + 1)) -' 1) by A5, A11, A7, SPRECT_2:3 .= f /. ((Index (p,f)) + (1 + 1)) by A19, XREAL_0:def_2 ; then A21: LSeg ((mid (f,((Index (p,f)) + 1),(len f))),1) = LSeg ((f /. ((Index (p,f)) + 1)),(f /. ((Index (p,f)) + (1 + 1)))) by A12, A20, A16, TOPREAL1:def_3; f /. ((Index (p,f)) + 1) in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by RLTOPSP1:68; then (LSeg (p,(f /. ((Index (p,f)) + 1)))) /\ (LSeg ((f /. ((Index (p,f)) + 1)),(f /. ((Index (p,f)) + (1 + 1))))) c= {(f /. ((Index (p,f)) + 1))} by A4, A14, TOPREAL1:6, XBOOLE_1:26; then A22: (LSeg (p,(f /. ((Index (p,f)) + 1)))) /\ (LSeg ((f /. ((Index (p,f)) + 1)),(f /. ((Index (p,f)) + (1 + 1))))) = {(f /. ((Index (p,f)) + 1))} by A18, XBOOLE_0:def_10; now__::_thesis:_L_Cut_(f,p)_is_unfolded percases ( p <> f . ((Index (p,f)) + 1) or p = f . ((Index (p,f)) + 1) ) ; suppose p <> f . ((Index (p,f)) + 1) ; ::_thesis: L_Cut (f,p) is unfolded then L_Cut (f,p) = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) by JORDAN3:def_3; hence L_Cut (f,p) is unfolded by A1, A12, A21, A22, Th28, SPPOL_2:29; ::_thesis: verum end; suppose p = f . ((Index (p,f)) + 1) ; ::_thesis: L_Cut (f,p) is unfolded hence L_Cut (f,p) is unfolded by A2, JORDAN3:def_3; ::_thesis: verum end; end; end; hence L_Cut (f,p) is unfolded ; ::_thesis: verum end; supposeA23: ((Index (p,f)) + 1) + 1 > len f ; ::_thesis: L_Cut (f,p) is unfolded A24: ( (Index (p,f)) + 1 < len f or (Index (p,f)) + 1 = len f ) by A5, XXREAL_0:1; now__::_thesis:_L_Cut_(f,p)_is_unfolded percases ( p <> f . ((Index (p,f)) + 1) or p = f . ((Index (p,f)) + 1) ) ; suppose p <> f . ((Index (p,f)) + 1) ; ::_thesis: L_Cut (f,p) is unfolded then L_Cut (f,p) = <*p*> ^ (mid (f,(len f),(len f))) by A23, A24, JORDAN3:def_3, NAT_1:13 .= <*p*> ^ <*(f /. (len f))*> by A6, JORDAN4:15 .= <*p,(f /. (len f))*> by FINSEQ_1:def_9 ; then len (L_Cut (f,p)) = 2 by FINSEQ_1:44; hence L_Cut (f,p) is unfolded by SPPOL_2:26; ::_thesis: verum end; suppose p = f . ((Index (p,f)) + 1) ; ::_thesis: L_Cut (f,p) is unfolded then L_Cut (f,p) = mid (f,(len f),(len f)) by A23, A24, JORDAN3:def_3, NAT_1:13 .= <*(f /. (len f))*> by A6, JORDAN4:15 ; then len (L_Cut (f,p)) = 1 by FINSEQ_1:39; hence L_Cut (f,p) is unfolded by SPPOL_2:26; ::_thesis: verum end; end; end; hence L_Cut (f,p) is unfolded ; ::_thesis: verum end; end; end; theorem Th33: :: JORDAN23:33 for f being FinSequence of (TOP-REAL 2) st f is unfolded holds for p being Point of (TOP-REAL 2) st p in L~ f holds R_Cut (f,p) is unfolded proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is unfolded implies for p being Point of (TOP-REAL 2) st p in L~ f holds R_Cut (f,p) is unfolded ) assume A1: f is unfolded ; ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds R_Cut (f,p) is unfolded let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies R_Cut (f,p) is unfolded ) assume A2: p in L~ f ; ::_thesis: R_Cut (f,p) is unfolded then A3: 1 <= Index (p,f) by JORDAN3:8; len f <> 0 by A2, TOPREAL1:22; then len f > 0 by NAT_1:3; then A4: len f >= 0 + 1 by NAT_1:13; then 1 in Seg (len f) by FINSEQ_1:1; then A5: 1 in dom f by FINSEQ_1:def_3; A6: Index (p,f) < len f by A2, JORDAN3:8; then A7: ((Index (p,f)) + 1) + 0 <= len f by NAT_1:13; then A8: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, TOPREAL1:def_3; Index (p,f) in Seg (len f) by A3, A6, FINSEQ_1:1; then A9: Index (p,f) in dom f by FINSEQ_1:def_3; then A10: (mid (f,1,(Index (p,f)))) /. (len (mid (f,1,(Index (p,f))))) = f /. (Index (p,f)) by A5, SPRECT_2:9; A11: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, JORDAN5B:29; A12: ((Index (p,f)) -' 1) + 1 = Index (p,f) by A2, JORDAN3:8, XREAL_1:235; percases ( Index (p,f) > 0 + 1 or Index (p,f) = 0 + 1 ) by A3, XXREAL_0:1; supposeA13: Index (p,f) > 0 + 1 ; ::_thesis: R_Cut (f,p) is unfolded A14: f /. (Index (p,f)) in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by RLTOPSP1:68; A15: f /. (Index (p,f)) in LSeg ((f /. (Index (p,f))),p) by RLTOPSP1:68; f /. (Index (p,f)) in LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f)))) by RLTOPSP1:68; then f /. (Index (p,f)) in (LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f))))) /\ (LSeg ((f /. (Index (p,f))),p)) by A15, XBOOLE_0:def_4; then A16: {(f /. (Index (p,f)))} c= (LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f))))) /\ (LSeg ((f /. (Index (p,f))),p)) by ZFMISC_1:31; A17: ((Index (p,f)) -' 1) + (1 + 1) <= len f by A7, A12; (Index (p,f)) - 1 > 0 by A13, XREAL_1:20; then (Index (p,f)) -' 1 > 0 by XREAL_0:def_2; then A18: (Index (p,f)) -' 1 >= 0 + 1 by NAT_1:13; then LSeg (f,((Index (p,f)) -' 1)) = LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f)))) by A6, A12, TOPREAL1:def_3; then (LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f))))) /\ (LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1)))) = {(f /. (Index (p,f)))} by A1, A12, A8, A18, A17, TOPREAL1:def_6; then (LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f))))) /\ (LSeg ((f /. (Index (p,f))),p)) c= {(f /. (Index (p,f)))} by A11, A14, TOPREAL1:6, XBOOLE_1:26; then A19: (LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f))))) /\ (LSeg ((f /. (Index (p,f))),p)) = {(f /. (Index (p,f)))} by A16, XBOOLE_0:def_10; A20: len (mid (f,1,(Index (p,f)))) = ((Index (p,f)) -' 1) + 1 by A4, A3, A6, FINSEQ_6:118 .= Index (p,f) by A2, JORDAN3:8, XREAL_1:235 ; then A21: ((len (mid (f,1,(Index (p,f))))) -' 1) + 1 = len (mid (f,1,(Index (p,f)))) by A2, JORDAN3:8, XREAL_1:235; (len (mid (f,1,(Index (p,f))))) -' 1 <= len (mid (f,1,(Index (p,f)))) by NAT_D:35; then (len (mid (f,1,(Index (p,f))))) -' 1 in Seg (len (mid (f,1,(Index (p,f))))) by A18, A20, FINSEQ_1:1; then (len (mid (f,1,(Index (p,f))))) -' 1 in dom (mid (f,1,(Index (p,f)))) by FINSEQ_1:def_3; then A22: (mid (f,1,(Index (p,f)))) /. ((len (mid (f,1,(Index (p,f))))) -' 1) = f /. ((((len (mid (f,1,(Index (p,f))))) -' 1) + 1) -' 1) by A2, A9, A5, JORDAN3:8, SPRECT_2:3 .= f /. ((len (mid (f,1,(Index (p,f))))) -' 1) by NAT_D:34 .= f /. ((((Index (p,f)) -' 1) + 1) -' 1) by A3, A6, JORDAN4:8 .= f /. ((Index (p,f)) -' 1) by A2, JORDAN3:8, XREAL_1:235 ; ((len (mid (f,1,(Index (p,f))))) -' 1) + 1 = len (mid (f,1,(Index (p,f)))) by A2, A20, JORDAN3:8, XREAL_1:235; then A23: LSeg ((mid (f,1,(Index (p,f)))),((len (mid (f,1,(Index (p,f))))) -' 1)) = LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f)))) by A10, A18, A20, A22, TOPREAL1:def_3; now__::_thesis:_R_Cut_(f,p)_is_unfolded percases ( p <> f . 1 or p = f . 1 ) ; suppose p <> f . 1 ; ::_thesis: R_Cut (f,p) is unfolded then R_Cut (f,p) = (mid (f,1,(Index (p,f)))) ^ <*p*> by JORDAN3:def_4; hence R_Cut (f,p) is unfolded by A1, A10, A23, A21, A19, Th28, SPPOL_2:30; ::_thesis: verum end; suppose p = f . 1 ; ::_thesis: R_Cut (f,p) is unfolded then R_Cut (f,p) = <*p*> by JORDAN3:def_4; then len (R_Cut (f,p)) = 1 by FINSEQ_1:39; hence R_Cut (f,p) is unfolded by SPPOL_2:26; ::_thesis: verum end; end; end; hence R_Cut (f,p) is unfolded ; ::_thesis: verum end; supposeA24: Index (p,f) = 0 + 1 ; ::_thesis: R_Cut (f,p) is unfolded now__::_thesis:_R_Cut_(f,p)_is_unfolded percases ( p <> f . 1 or p = f . 1 ) ; suppose p <> f . 1 ; ::_thesis: R_Cut (f,p) is unfolded then R_Cut (f,p) = (mid (f,1,1)) ^ <*p*> by A24, JORDAN3:def_4 .= <*(f /. 1)*> ^ <*p*> by A4, JORDAN4:15 .= <*(f /. 1),p*> by FINSEQ_1:def_9 ; then len (R_Cut (f,p)) = 2 by FINSEQ_1:44; hence R_Cut (f,p) is unfolded by SPPOL_2:26; ::_thesis: verum end; suppose p = f . 1 ; ::_thesis: R_Cut (f,p) is unfolded then R_Cut (f,p) = <*p*> by JORDAN3:def_4; then len (R_Cut (f,p)) = 1 by FINSEQ_1:39; hence R_Cut (f,p) is unfolded by SPPOL_2:26; ::_thesis: verum end; end; end; hence R_Cut (f,p) is unfolded ; ::_thesis: verum end; end; end; theorem :: JORDAN23:34 for f being FinSequence of (TOP-REAL 2) st f is unfolded & f is weakly-one-to-one holds for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds B_Cut (f,p,q) is unfolded proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is unfolded & f is weakly-one-to-one implies for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds B_Cut (f,p,q) is unfolded ) assume A1: ( f is unfolded & f is weakly-one-to-one ) ; ::_thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds B_Cut (f,p,q) is unfolded let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & q in L~ f implies B_Cut (f,p,q) is unfolded ) assume that A2: p in L~ f and A3: q in L~ f ; ::_thesis: B_Cut (f,p,q) is unfolded A4: Index (p,f) < len f by A2, JORDAN3:8; A5: 1 <= Index (p,f) by A2, JORDAN3:8; then Index (p,f) in Seg (len f) by A4, FINSEQ_1:1; then A6: Index (p,f) in dom f by FINSEQ_1:def_3; percases ( p <> q or p = q ) ; supposeA7: p <> q ; ::_thesis: B_Cut (f,p,q) is unfolded now__::_thesis:_B_Cut_(f,p,q)_is_unfolded percases ( ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) or ( not ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) ; supposeA8: ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) ; ::_thesis: B_Cut (f,p,q) is unfolded then A9: q in L~ (L_Cut (f,p)) by JORDAN3:29; L_Cut (f,p) is unfolded by A1, A2, Th32; then R_Cut ((L_Cut (f,p)),q) is unfolded by A9, Th33; hence B_Cut (f,p,q) is unfolded by A8, JORDAN3:def_7; ::_thesis: verum end; supposeA10: ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ; ::_thesis: B_Cut (f,p,q) is unfolded A11: L_Cut (f,p) is unfolded by A1, A2, Th32; q in L~ (L_Cut (f,p)) by A2, A3, A7, A10, JORDAN3:31; then R_Cut ((L_Cut (f,p)),q) is unfolded by A11, Th33; hence B_Cut (f,p,q) is unfolded by A10, JORDAN3:def_7; ::_thesis: verum end; supposeA12: ( not ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; ::_thesis: B_Cut (f,p,q) is unfolded A13: now__::_thesis:_p_in_L~_(L_Cut_(f,q)) percases ( Index (q,f) < Index (p,f) or Index (q,f) = Index (p,f) ) by A2, A3, A12, XXREAL_0:1; suppose Index (q,f) < Index (p,f) ; ::_thesis: p in L~ (L_Cut (f,q)) hence p in L~ (L_Cut (f,q)) by A2, A3, JORDAN3:29; ::_thesis: verum end; supposeA14: Index (q,f) = Index (p,f) ; ::_thesis: p in L~ (L_Cut (f,q)) A15: (Index (p,f)) + 1 >= 1 by NAT_1:11; (Index (p,f)) + 1 <= len f by A4, NAT_1:13; then (Index (p,f)) + 1 in Seg (len f) by A15, FINSEQ_1:1; then A16: (Index (p,f)) + 1 in dom f by FINSEQ_1:def_3; set Ls = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))); A17: q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, A14, JORDAN5B:29; A18: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, JORDAN5B:29; f . (Index (p,f)) <> f . ((Index (p,f)) + 1) by A1, A5, A4, Def2; then f . (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A16, PARTFUN1:def_6; then A19: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A6, PARTFUN1:def_6; then A20: LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) is_an_arc_of f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by TOPREAL1:9; not LE p,q, LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))),f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A12, A14, A19, JORDAN5C:17; then LE q,p, LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))),f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A7, A20, A18, A17, JORDAN5C:14; hence p in L~ (L_Cut (f,q)) by A2, A3, A7, A14, A19, JORDAN3:31, JORDAN5C:17; ::_thesis: verum end; end; end; A21: B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) by A12, JORDAN3:def_7; L_Cut (f,q) is unfolded by A1, A3, Th32; then R_Cut ((L_Cut (f,q)),p) is unfolded by A13, Th33; hence B_Cut (f,p,q) is unfolded by A21, SPPOL_2:28; ::_thesis: verum end; end; end; hence B_Cut (f,p,q) is unfolded ; ::_thesis: verum end; suppose p = q ; ::_thesis: B_Cut (f,p,q) is unfolded then B_Cut (f,p,q) = <*p*> by A1, A2, Th15; then len (B_Cut (f,p,q)) = 1 by FINSEQ_1:39; hence B_Cut (f,p,q) is unfolded by SPPOL_2:26; ::_thesis: verum end; end; end; theorem Th35: :: JORDAN23:35 for f, g being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 & g = (mid (f,1,(Index (p,f)))) ^ <*p*> holds g is_S-Seq_joining f /. 1,p proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 & g = (mid (f,1,(Index (p,f)))) ^ <*p*> holds g is_S-Seq_joining f /. 1,p let p be Point of (TOP-REAL 2); ::_thesis: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 & g = (mid (f,1,(Index (p,f)))) ^ <*p*> implies g is_S-Seq_joining f /. 1,p ) assume that A1: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. ) and A2: p in L~ f and A3: p <> f . 1 and A4: g = (mid (f,1,(Index (p,f)))) ^ <*p*> ; ::_thesis: g is_S-Seq_joining f /. 1,p A5: Index (p,f) < len f by A2, JORDAN3:8; A6: for j1, j2 being Nat st j1 + 1 < j2 holds LSeg (g,j1) misses LSeg (g,j2) proof let j1, j2 be Nat; ::_thesis: ( j1 + 1 < j2 implies LSeg (g,j1) misses LSeg (g,j2) ) assume A7: j1 + 1 < j2 ; ::_thesis: LSeg (g,j1) misses LSeg (g,j2) j1 >= 0 by NAT_1:2; then A8: ( j1 = 0 or j1 >= 0 + 1 ) by NAT_1:13; now__::_thesis:_(_(_j1_=_0_&_LSeg_(g,j1)_misses_LSeg_(g,j2)_)_or_(_(_j1_=_1_or_j1_>_1_)_&_j2_+_1_<=_len_g_&_LSeg_(g,j1)_misses_LSeg_(g,j2)_)_or_(_j2_+_1_>_len_g_&_LSeg_(g,j1)_misses_LSeg_(g,j2)_)_) percases ( j1 = 0 or ( ( j1 = 1 or j1 > 1 ) & j2 + 1 <= len g ) or j2 + 1 > len g ) by A8, XXREAL_0:1; case j1 = 0 ; ::_thesis: LSeg (g,j1) misses LSeg (g,j2) then LSeg (g,j1) = {} by TOPREAL1:def_3; then (LSeg (g,j1)) /\ (LSeg (g,j2)) = {} ; hence LSeg (g,j1) misses LSeg (g,j2) by XBOOLE_0:def_7; ::_thesis: verum end; casethat A9: ( j1 = 1 or j1 > 1 ) and A10: j2 + 1 <= len g ; ::_thesis: LSeg (g,j1) misses LSeg (g,j2) j2 < len g by A10, NAT_1:13; then j1 + 1 < len g by A7, XXREAL_0:2; then A11: LSeg (g,j1) c= LSeg (f,j1) by A2, A4, A9, JORDAN3:18; 1 + 1 <= j1 + 1 by A9, XREAL_1:6; then 2 <= j2 by A7, XXREAL_0:2; then 1 <= j2 by XXREAL_0:2; then A12: LSeg (g,j2) c= LSeg (f,j2) by A2, A4, A10, JORDAN3:18; LSeg (f,j1) misses LSeg (f,j2) by A1, A7, TOPREAL1:def_7; then (LSeg (f,j1)) /\ (LSeg (f,j2)) = {} by XBOOLE_0:def_7; then (LSeg (g,j1)) /\ (LSeg (g,j2)) = {} by A11, A12, XBOOLE_1:3, XBOOLE_1:27; hence LSeg (g,j1) misses LSeg (g,j2) by XBOOLE_0:def_7; ::_thesis: verum end; case j2 + 1 > len g ; ::_thesis: LSeg (g,j1) misses LSeg (g,j2) then LSeg (g,j2) = {} by TOPREAL1:def_3; then (LSeg (g,j1)) /\ (LSeg (g,j2)) = {} ; hence LSeg (g,j1) misses LSeg (g,j2) by XBOOLE_0:def_7; ::_thesis: verum end; end; end; hence LSeg (g,j1) misses LSeg (g,j2) ; ::_thesis: verum end; A13: len g = (len (mid (f,1,(Index (p,f))))) + (len <*p*>) by A4, FINSEQ_1:22 .= (len (mid (f,1,(Index (p,f))))) + 1 by FINSEQ_1:39 ; consider i being Element of NAT such that 1 <= i and A14: i + 1 <= len f and p in LSeg (f,i) by A2, SPPOL_2:13; A15: 1 <= Index (p,f) by A2, JORDAN3:8; 1 <= 1 + i by NAT_1:12; then A16: 1 <= len f by A14, XXREAL_0:2; then A17: len (mid (f,1,(Index (p,f)))) = ((Index (p,f)) -' 1) + 1 by A15, A5, FINSEQ_6:118; then A18: len (mid (f,1,(Index (p,f)))) = Index (p,f) by A2, JORDAN3:8, XREAL_1:235; then g . 1 = (mid (f,1,(Index (p,f)))) . 1 by A4, A15, FINSEQ_6:109; then g . 1 = f . 1 by A15, A5, A16, FINSEQ_6:118; then A19: g . 1 = f /. 1 by A16, FINSEQ_4:15; A20: for j being Nat st 1 <= j & j + 2 <= len g holds (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} proof let j be Nat; ::_thesis: ( 1 <= j & j + 2 <= len g implies (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} ) assume that A21: 1 <= j and A22: j + 2 <= len g ; ::_thesis: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} A23: j + 1 <= len g by A22, NAT_D:47; then LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by A21, TOPREAL1:def_3; then A24: g /. (j + 1) in LSeg (g,j) by RLTOPSP1:68; A25: 1 <= j + 1 by A21, NAT_D:48; then LSeg (g,(j + 1)) = LSeg ((g /. (j + 1)),(g /. ((j + 1) + 1))) by A22, TOPREAL1:def_3; then g /. (j + 1) in LSeg (g,(j + 1)) by RLTOPSP1:68; then g /. (j + 1) in (LSeg (g,j)) /\ (LSeg (g,(j + 1))) by A24, XBOOLE_0:def_4; then A26: {(g /. (j + 1))} c= (LSeg (g,j)) /\ (LSeg (g,(j + 1))) by ZFMISC_1:31; j + 1 <= len g by A22, NAT_D:47; then A27: LSeg (g,j) c= LSeg (f,j) by A2, A4, A21, JORDAN3:18; A28: Index (p,f) <= len f by A2, JORDAN3:8; A29: (j + 1) + 1 <= len g by A22; then LSeg (g,(j + 1)) c= LSeg (f,(j + 1)) by A2, A4, A25, JORDAN3:18; then A30: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) c= (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by A27, XBOOLE_1:27; A31: g /. (j + 1) = g . (j + 1) by A25, A23, FINSEQ_4:15; now__::_thesis:_(LSeg_(g,j))_/\_(LSeg_(g,(j_+_1)))_=_{(g_/._(j_+_1))} A32: len g = (len (mid (f,1,(Index (p,f))))) + 1 by A4, FINSEQ_2:16; Index (p,f) <= len f by A2, JORDAN3:8; then A33: len g <= (len f) + 1 by A18, A32, XREAL_1:6; now__::_thesis:_(_(_len_g_=_(len_f)_+_1_&_contradiction_)_or_(_len_g_<_(len_f)_+_1_&_(LSeg_(g,j))_/\_(LSeg_(g,(j_+_1)))_=_{(g_/._(j_+_1))}_)_) percases ( len g = (len f) + 1 or len g < (len f) + 1 ) by A33, XXREAL_0:1; case len g = (len f) + 1 ; ::_thesis: contradiction hence contradiction by A2, A18, A32, JORDAN3:8; ::_thesis: verum end; case len g < (len f) + 1 ; ::_thesis: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} then len g <= len f by NAT_1:13; then j + 2 <= len f by A22, XXREAL_0:2; then A34: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) c= {(f /. (j + 1))} by A1, A21, A30, TOPREAL1:def_6; A35: j + 1 <= Index (p,f) by A18, A29, A32, XREAL_1:6; then j + 1 <= len f by A28, XXREAL_0:2; then A36: f . (j + 1) = f /. (j + 1) by A25, FINSEQ_4:15; g . (j + 1) = (mid (f,1,(Index (p,f)))) . (j + 1) by A4, A18, A25, A35, FINSEQ_1:64 .= f . (j + 1) by A5, A25, A35, FINSEQ_6:123 ; hence (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} by A31, A26, A34, A36, XBOOLE_0:def_10; ::_thesis: verum end; end; end; hence (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} ; ::_thesis: verum end; hence (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} ; ::_thesis: verum end; for j being Nat st 1 <= j & j + 1 <= len g & not (g /. j) `1 = (g /. (j + 1)) `1 holds (g /. j) `2 = (g /. (j + 1)) `2 proof A37: Index (p,f) < len f by A2, JORDAN3:8; let j be Nat; ::_thesis: ( 1 <= j & j + 1 <= len g & not (g /. j) `1 = (g /. (j + 1)) `1 implies (g /. j) `2 = (g /. (j + 1)) `2 ) assume that A38: 1 <= j and A39: j + 1 <= len g ; ::_thesis: ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 ) A40: LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by A38, A39, TOPREAL1:def_3; j + 1 <= (Index (p,f)) + 1 by A4, A18, A39, FINSEQ_2:16; then j <= Index (p,f) by XREAL_1:6; then j < len f by A37, XXREAL_0:2; then A41: j + 1 <= len f by NAT_1:13; then A42: LSeg (f,j) = LSeg ((f /. j),(f /. (j + 1))) by A38, TOPREAL1:def_3; A43: ( (f /. j) `1 = (f /. (j + 1)) `1 or (f /. j) `2 = (f /. (j + 1)) `2 ) by A1, A38, A41, TOPREAL1:def_5; LSeg (g,j) c= LSeg (f,j) by A2, A4, A38, A39, JORDAN3:18; hence ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 ) by A40, A42, A43, JORDAN3:3; ::_thesis: verum end; then A44: ( g is unfolded & g is s.n.c. & g is special ) by A20, A6, TOPREAL1:def_5, TOPREAL1:def_6, TOPREAL1:def_7; 1 <= len <*p*> by FINSEQ_1:39; then A45: 1 in dom <*p*> by FINSEQ_3:25; for x1, x2 being set st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 implies x1 = x2 ) assume that A46: x1 in dom g and A47: x2 in dom g and A48: g . x1 = g . x2 ; ::_thesis: x1 = x2 reconsider n1 = x1, n2 = x2 as Element of NAT by A46, A47; A49: 1 <= n1 by A46, FINSEQ_3:25; A50: n2 <= len g by A47, FINSEQ_3:25; A51: 1 <= n2 by A47, FINSEQ_3:25; A52: n1 <= len g by A46, FINSEQ_3:25; now__::_thesis:_x1_=_x2 A53: g . (len g) = <*p*> . 1 by A4, A45, A13, FINSEQ_1:def_7 .= p by FINSEQ_1:def_8 ; now__::_thesis:_(_(_n1_=_len_g_&_x1_=_x2_)_or_(_n2_=_len_g_&_x1_=_x2_)_or_(_n1_<>_len_g_&_n2_<>_len_g_&_x1_=_x2_)_) percases ( n1 = len g or n2 = len g or ( n1 <> len g & n2 <> len g ) ) ; caseA54: n1 = len g ; ::_thesis: x1 = x2 now__::_thesis:_not_n2_<>_len_g assume A55: n2 <> len g ; ::_thesis: contradiction then n2 < len g by A50, XXREAL_0:1; then A56: n2 <= len (mid (f,1,(Index (p,f)))) by A13, NAT_1:13; then A57: n2 < len f by A5, A18, XXREAL_0:2; g . n2 = (mid (f,1,(Index (p,f)))) . n2 by A4, A51, A56, FINSEQ_1:64; then g . n2 = f . ((n2 + 1) -' 1) by A15, A5, A16, A51, A56, FINSEQ_6:118; then A58: p = f . n2 by A48, A53, A54, NAT_D:34; then 1 < n2 by A3, A51, XXREAL_0:1; then (Index (p,f)) + 1 = n2 by A1, A58, A57, Th18; hence contradiction by A2, A17, A13, A55, JORDAN3:8, XREAL_1:235; ::_thesis: verum end; hence x1 = x2 by A54; ::_thesis: verum end; caseA59: n2 = len g ; ::_thesis: x1 = x2 now__::_thesis:_not_n1_<>_len_g assume A60: n1 <> len g ; ::_thesis: contradiction then n1 < len g by A52, XXREAL_0:1; then A61: n1 <= len (mid (f,1,(Index (p,f)))) by A13, NAT_1:13; then A62: n1 < len f by A5, A18, XXREAL_0:2; g . n1 = (mid (f,1,(Index (p,f)))) . n1 by A4, A49, A61, FINSEQ_1:64; then g . n1 = f . ((n1 + 1) -' 1) by A15, A5, A16, A49, A61, FINSEQ_6:118; then A63: p = f . n1 by A48, A53, A59, NAT_D:34; then 1 < n1 by A3, A49, XXREAL_0:1; then (Index (p,f)) + 1 = n1 by A1, A63, A62, Th18; hence contradiction by A2, A17, A13, A60, JORDAN3:8, XREAL_1:235; ::_thesis: verum end; hence x1 = x2 by A59; ::_thesis: verum end; casethat A64: n1 <> len g and A65: n2 <> len g ; ::_thesis: x1 = x2 n2 < len g by A50, A65, XXREAL_0:1; then A66: n2 <= len (mid (f,1,(Index (p,f)))) by A13, NAT_1:13; then A67: g . n2 = (mid (f,1,(Index (p,f)))) . n2 by A4, A51, FINSEQ_1:64 .= f . n2 by A5, A18, A51, A66, FINSEQ_6:123 ; n2 < len f by A5, A18, A66, XXREAL_0:2; then n2 in Seg (len f) by A51, FINSEQ_1:1; then A68: n2 in dom f by FINSEQ_1:def_3; n1 < len g by A52, A64, XXREAL_0:1; then A69: n1 <= len (mid (f,1,(Index (p,f)))) by A13, NAT_1:13; then n1 < len f by A5, A18, XXREAL_0:2; then n1 in Seg (len f) by A49, FINSEQ_1:1; then A70: n1 in dom f by FINSEQ_1:def_3; g . n1 = (mid (f,1,(Index (p,f)))) . n1 by A4, A49, A69, FINSEQ_1:64 .= f . n1 by A5, A18, A49, A69, FINSEQ_6:123 ; hence x1 = x2 by A1, A5, A18, A48, A69, A66, A67, A70, A68, Def1; ::_thesis: verum end; end; end; hence x1 = x2 ; ::_thesis: verum end; hence x1 = x2 ; ::_thesis: verum end; then A71: g is one-to-one by FUNCT_1:def_4; 1 + 1 <= len g by A15, A18, A13, XREAL_1:6; then A72: g is being_S-Seq by A71, A44, TOPREAL1:def_8; g . (len g) = p by A4, A13, FINSEQ_1:42; hence g is_S-Seq_joining f /. 1,p by A19, A72, JORDAN3:def_2; ::_thesis: verum end; theorem Th36: :: JORDAN23:36 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p = f . ((Index (p,f)) + 1) & p <> f . (len f) holds ((Index (p,(Rev f))) + (Index (p,f))) + 1 = len f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p = f . ((Index (p,f)) + 1) & p <> f . (len f) holds ((Index (p,(Rev f))) + (Index (p,f))) + 1 = len f let p be Point of (TOP-REAL 2); ::_thesis: ( f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p = f . ((Index (p,f)) + 1) & p <> f . (len f) implies ((Index (p,(Rev f))) + (Index (p,f))) + 1 = len f ) assume that A1: ( f is poorly-one-to-one & f is unfolded & f is s.n.c. ) and A2: p in L~ f and A3: p = f . ((Index (p,f)) + 1) and A4: p <> f . (len f) ; ::_thesis: ((Index (p,(Rev f))) + (Index (p,f))) + 1 = len f A5: Rev f is s.n.c. by A1, SPPOL_2:35; A6: len f = len (Rev f) by FINSEQ_5:def_3; len f <= (len f) + (Index (p,f)) by NAT_1:11; then A7: (len f) - (Index (p,f)) <= len (Rev f) by A6, XREAL_1:20; Index (p,f) <= len f by A2, JORDAN3:8; then A8: (len f) - (Index (p,f)) = (len f) -' (Index (p,f)) by XREAL_1:233; Index (p,f) < len f by A2, JORDAN3:8; then A9: (Index (p,f)) + 1 <= len f by NAT_1:13; then (Index (p,f)) + 1 < len f by A3, A4, XXREAL_0:1; then A10: 1 < (len f) - (Index (p,f)) by XREAL_1:20; 1 <= (Index (p,f)) + 1 by NAT_1:11; then (Index (p,f)) + 1 in dom f by A9, FINSEQ_3:25; then A11: (Index (p,f)) + 1 in dom (Rev f) by FINSEQ_5:57; p = (Rev (Rev f)) . ((Index (p,f)) + 1) by A3 .= (Rev f) . (((len (Rev f)) - ((Index (p,f)) + 1)) + 1) by A11, FINSEQ_5:58 .= (Rev f) . ((len (Rev f)) - (Index (p,f))) .= (Rev f) . ((len f) - (Index (p,f))) by FINSEQ_5:def_3 ; then (Index (p,(Rev f))) + 1 = (len f) -' (Index (p,f)) by A1, A5, A7, A10, A8, Th18, SPPOL_2:28; hence ((Index (p,(Rev f))) + (Index (p,f))) + 1 = len f by A8; ::_thesis: verum end; theorem :: JORDAN23:37 for f being non empty FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is weakly-one-to-one & len f >= 2 holds L_Cut (f,(f /. 1)) = f proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is weakly-one-to-one & len f >= 2 holds L_Cut (f,(f /. 1)) = f let p be Point of (TOP-REAL 2); ::_thesis: ( f is weakly-one-to-one & len f >= 2 implies L_Cut (f,(f /. 1)) = f ) assume that A1: f is weakly-one-to-one and A2: len f >= 2 ; ::_thesis: L_Cut (f,(f /. 1)) = f A3: Index ((f /. 1),f) = 1 by A2, JORDAN3:11; 1 <= len f by A2, XXREAL_0:2; then A4: 1 in dom f by FINSEQ_3:25; then A5: f /. 1 = f . 1 by PARTFUN1:def_6; 2 = 1 + 1 ; then A6: 1 < len f by A2, NAT_1:13; then f . 1 <> f . (1 + 1) by A1, Def2; then f /. 1 <> f . (1 + 1) by A4, PARTFUN1:def_6; hence L_Cut (f,(f /. 1)) = <*(f /. 1)*> ^ (mid (f,((Index ((f /. 1),f)) + 1),(len f))) by A3, JORDAN3:def_3 .= mid (f,1,(len f)) by A4, A6, A5, A3, FINSEQ_6:126 .= f by A2, FINSEQ_6:120, XXREAL_0:2 ; ::_thesis: verum end; theorem Th38: :: JORDAN23:38 for f being non empty FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) holds L_Cut ((Rev f),p) = Rev (R_Cut (f,p)) proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) holds L_Cut ((Rev f),p) = Rev (R_Cut (f,p)) let p be Point of (TOP-REAL 2); ::_thesis: ( f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) implies L_Cut ((Rev f),p) = Rev (R_Cut (f,p)) ) assume that A1: ( f is poorly-one-to-one & f is unfolded & f is s.n.c. ) and A2: p in L~ f and A3: p <> f . (len f) ; ::_thesis: L_Cut ((Rev f),p) = Rev (R_Cut (f,p)) A4: Index (p,f) < len f by A2, JORDAN3:8; A5: p in L~ (Rev f) by A2, SPPOL_2:22; A6: Rev f is s.n.c. by A1, SPPOL_2:35; A7: dom (Rev f) = dom f by FINSEQ_5:57; A8: len f = len (Rev f) by FINSEQ_5:def_3; A9: 1 <= Index (p,f) by A2, JORDAN3:8; then A10: 1 < len f by A4, XXREAL_0:2; L~ f = L~ (Rev f) by SPPOL_2:22; then Index (p,(Rev f)) < len (Rev f) by A2, JORDAN3:8; then A11: (Index (p,(Rev f))) + 1 <= len f by A8, NAT_1:13; 1 <= (Index (p,(Rev f))) + 1 by NAT_1:11; then A12: (Index (p,(Rev f))) + 1 in dom f by A11, FINSEQ_3:25; percases ( p = f . 1 or ( p <> f . 1 & p <> f . (len f) & p = f . ((Index (p,f)) + 1) ) or ( p <> f . 1 & p <> f . ((Index (p,f)) + 1) ) ) by A3; supposeA13: p = f . 1 ; ::_thesis: L_Cut ((Rev f),p) = Rev (R_Cut (f,p)) A14: ((len (Rev f)) -' 1) + 1 = len (Rev f) by A8, A9, A4, XREAL_1:235, XXREAL_0:2; then A15: ((Rev f) /^ ((len (Rev f)) -' 1)) . 1 = (Rev f) . (len (Rev f)) by FINSEQ_6:114; A16: len ((Rev f) /^ ((len (Rev f)) -' 1)) = (len (Rev f)) -' ((len (Rev f)) -' 1) by RFINSEQ:29; A17: 1 <= (len (Rev f)) - ((len (Rev f)) -' 1) by A14; then A18: 1 <= len ((Rev f) /^ ((len (Rev f)) -' 1)) by A16, NAT_D:39; A19: not (Rev f) /^ ((len (Rev f)) -' 1) is empty by A16, A17, NAT_D:39; ((len (Rev f)) -' (len (Rev f))) + 1 = ((len (Rev f)) - (len (Rev f))) + 1 by XREAL_1:233 .= 1 ; then A20: mid ((Rev f),(len (Rev f)),(len (Rev f))) = ((Rev f) /^ ((len (Rev f)) -' 1)) | 1 by FINSEQ_6:def_3 .= <*(((Rev f) /^ ((len (Rev f)) -' 1)) /. 1)*> by A19, FINSEQ_5:20 .= <*((Rev f) . (len (Rev f)))*> by A15, A18, FINSEQ_4:15 ; A21: p = (Rev f) . (len f) by A13, FINSEQ_5:62; then (Index (p,(Rev f))) + 1 = len f by A1, A6, A8, A10, Th18, SPPOL_2:28; hence L_Cut ((Rev f),p) = <*p*> by A8, A21, A20, JORDAN3:def_3 .= Rev <*p*> by FINSEQ_5:60 .= Rev (R_Cut (f,p)) by A13, JORDAN3:def_4 ; ::_thesis: verum end; supposethat A22: p <> f . 1 and A23: p <> f . (len f) and A24: p = f . ((Index (p,f)) + 1) ; ::_thesis: L_Cut ((Rev f),p) = Rev (R_Cut (f,p)) A25: len f = ((Index (p,(Rev f))) + (Index (p,f))) + 1 by A1, A2, A23, A24, Th36 .= (Index (p,f)) + ((Index (p,(Rev f))) + 1) ; len f = ((Index (p,(Rev f))) + (Index (p,f))) + 1 by A1, A2, A23, A24, Th36 .= (Index (p,(Rev f))) + ((Index (p,f)) + 1) ; then A26: p = f . (((len f) - ((Index (p,(Rev f))) + 1)) + 1) by A24 .= (Rev f) . ((Index (p,(Rev f))) + 1) by A12, FINSEQ_5:58 ; A27: (len f) -' (Index (p,f)) = (len f) - (Index (p,f)) by A4, XREAL_1:233 .= (Index (p,(Rev f))) + 1 by A25 ; p <> (Rev f) . (len f) by A22, FINSEQ_5:62; then A28: (Index (p,(Rev f))) + 1 < len f by A11, A26, XXREAL_0:1; thus L_Cut ((Rev f),p) = mid ((Rev f),((Index (p,(Rev f))) + 1),(len f)) by A8, A26, JORDAN3:def_3 .= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(len f))) by A7, A12, A26, A27, A28, FINSEQ_6:126 .= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(((len f) -' 1) + 1))) by A9, A4, XREAL_1:235, XXREAL_0:2 .= <*p*> ^ (Rev (mid (f,1,(Index (p,f))))) by A9, A4, A10, FINSEQ_6:113 .= Rev ((mid (f,1,(Index (p,f)))) ^ <*p*>) by FINSEQ_5:63 .= Rev (R_Cut (f,p)) by A22, JORDAN3:def_4 ; ::_thesis: verum end; supposethat A29: p <> f . 1 and A30: p <> f . ((Index (p,f)) + 1) ; ::_thesis: L_Cut ((Rev f),p) = Rev (R_Cut (f,p)) A31: p <> (Rev f) . (len f) by A29, FINSEQ_5:62; A32: now__::_thesis:_not_p_=_(Rev_f)_._((Index_(p,(Rev_f)))_+_1) assume A33: p = (Rev f) . ((Index (p,(Rev f))) + 1) ; ::_thesis: contradiction then A34: len (Rev f) = ((Index (p,(Rev (Rev f)))) + (Index (p,(Rev f)))) + 1 by A1, A6, A5, A8, A31, Th36, SPPOL_2:28 .= ((Index (p,f)) + 1) + (Index (p,(Rev f))) ; p = f . (((len f) - ((Index (p,(Rev f))) + 1)) + 1) by A12, A33, FINSEQ_5:58 .= f . ((Index (p,f)) + 1) by A8, A34 ; hence contradiction by A30; ::_thesis: verum end; A35: Index (p,f) < len f by A2, JORDAN3:8; len f = (Index (p,(Rev f))) + (Index (p,f)) by A1, A2, A30, JORDAN3:21; then Index (p,(Rev f)) = (len f) - (Index (p,f)) .= (len f) -' (Index (p,f)) by A35, XREAL_1:233 ; hence L_Cut ((Rev f),p) = <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(len f))) by A8, A32, JORDAN3:def_3 .= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(((len f) -' 1) + 1))) by A9, A4, XREAL_1:235, XXREAL_0:2 .= <*p*> ^ (Rev (mid (f,1,(Index (p,f))))) by A9, A4, A10, FINSEQ_6:113 .= Rev ((mid (f,1,(Index (p,f)))) ^ <*p*>) by FINSEQ_5:63 .= Rev (R_Cut (f,p)) by A29, JORDAN3:def_4 ; ::_thesis: verum end; end; end; theorem Th39: :: JORDAN23:39 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 holds R_Cut (f,p) is_S-Seq_joining f /. 1,p proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 holds R_Cut (f,p) is_S-Seq_joining f /. 1,p let p be Point of (TOP-REAL 2); ::_thesis: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 implies R_Cut (f,p) is_S-Seq_joining f /. 1,p ) assume that A1: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. ) and A2: p in L~ f and A3: p <> f . 1 ; ::_thesis: R_Cut (f,p) is_S-Seq_joining f /. 1,p R_Cut (f,p) = (mid (f,1,(Index (p,f)))) ^ <*p*> by A3, JORDAN3:def_4; hence R_Cut (f,p) is_S-Seq_joining f /. 1,p by A1, A2, A3, Th35; ::_thesis: verum end; theorem Th40: :: JORDAN23:40 for f being non empty FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) & p <> f . 1 holds L_Cut (f,p) is_S-Seq_joining p,f /. (len f) proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) & p <> f . 1 holds L_Cut (f,p) is_S-Seq_joining p,f /. (len f) let p be Point of (TOP-REAL 2); ::_thesis: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) & p <> f . 1 implies L_Cut (f,p) is_S-Seq_joining p,f /. (len f) ) assume that A1: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. ) and A2: p in L~ f and A3: p <> f . (len f) and A4: p <> f . 1 ; ::_thesis: L_Cut (f,p) is_S-Seq_joining p,f /. (len f) A5: Rev f is special by A1, SPPOL_2:40; A6: p in L~ (Rev f) by A2, SPPOL_2:22; p <> (Rev f) . (len f) by A4, FINSEQ_5:62; then A7: p <> (Rev f) . (len (Rev f)) by FINSEQ_5:def_3; A8: Rev f is s.n.c. by A1, SPPOL_2:35; A9: p <> (Rev f) . 1 by A3, FINSEQ_5:62; A10: Rev f is unfolded by A1, SPPOL_2:28; L_Cut (f,p) = L_Cut ((Rev (Rev f)),p) .= Rev (R_Cut ((Rev f),p)) by A1, A7, A10, A8, A6, Th38 ; then L_Cut (f,p) is_S-Seq_joining p,(Rev f) /. 1 by A1, A5, A10, A8, A6, A9, Th39, JORDAN3:15; hence L_Cut (f,p) is_S-Seq_joining p,f /. (len f) by FINSEQ_5:65; ::_thesis: verum end; theorem :: JORDAN23:41 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 holds R_Cut (f,p) is being_S-Seq proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 holds R_Cut (f,p) is being_S-Seq let p be Point of (TOP-REAL 2); ::_thesis: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 implies R_Cut (f,p) is being_S-Seq ) assume that A1: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. ) and A2: p in L~ f and A3: p <> f . 1 ; ::_thesis: R_Cut (f,p) is being_S-Seq R_Cut (f,p) is_S-Seq_joining f /. 1,p by A1, A2, A3, Th39; hence R_Cut (f,p) is being_S-Seq by JORDAN3:def_2; ::_thesis: verum end; theorem Th42: :: JORDAN23:42 for f being non empty FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) & p <> f . 1 holds L_Cut (f,p) is being_S-Seq proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) & p <> f . 1 holds L_Cut (f,p) is being_S-Seq let p be Point of (TOP-REAL 2); ::_thesis: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) & p <> f . 1 implies L_Cut (f,p) is being_S-Seq ) assume that A1: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. ) and A2: p in L~ f and A3: p <> f . (len f) and A4: p <> f . 1 ; ::_thesis: L_Cut (f,p) is being_S-Seq L_Cut (f,p) is_S-Seq_joining p,f /. (len f) by A1, A2, A3, A4, Th40; hence L_Cut (f,p) is being_S-Seq by JORDAN3:def_2; ::_thesis: verum end; Lm1: for f being non empty FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & q in L~ f & p <> q & p <> f . 1 & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) holds B_Cut (f,p,q) is_S-Seq_joining p,q proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & q in L~ f & p <> q & p <> f . 1 & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) holds B_Cut (f,p,q) is_S-Seq_joining p,q let p, q be Point of (TOP-REAL 2); ::_thesis: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & q in L~ f & p <> q & p <> f . 1 & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) implies B_Cut (f,p,q) is_S-Seq_joining p,q ) assume that A1: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. ) and A2: p in L~ f and A3: q in L~ f and A4: p <> q ; ::_thesis: ( not p <> f . 1 or ( not Index (p,f) < Index (q,f) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) or B_Cut (f,p,q) is_S-Seq_joining p,q ) assume A5: p <> f . 1 ; ::_thesis: ( ( not Index (p,f) < Index (q,f) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) or B_Cut (f,p,q) is_S-Seq_joining p,q ) A6: Index (q,f) < len f by A3, JORDAN3:8; Index (p,f) < len f by A2, JORDAN3:8; then A7: (Index (p,f)) + 1 <= len f by NAT_1:13; assume A8: ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; ::_thesis: B_Cut (f,p,q) is_S-Seq_joining p,q then A9: B_Cut (f,p,q) = R_Cut ((L_Cut (f,p)),q) by A2, A3, JORDAN3:def_7; 1 <= Index (q,f) by A3, JORDAN3:8; then A10: 1 < len f by A6, XXREAL_0:2; A11: now__::_thesis:_(_(_Index_(p,f)_<_Index_(q,f)_&_not_p_=_f_._(len_f)_)_or_(_Index_(p,f)_=_Index_(q,f)_&_LE_p,q,f_/._(Index_(p,f)),f_/._((Index_(p,f))_+_1)_&_not_p_=_f_._(len_f)_)_) percases ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) by A8; caseA12: Index (p,f) < Index (q,f) ; ::_thesis: not p = f . (len f) assume A13: p = f . (len f) ; ::_thesis: contradiction (Index (p,f)) + 1 <= Index (q,f) by A12, NAT_1:13; then len f <= Index (q,f) by A1, A10, A13, Th18; hence contradiction by A3, JORDAN3:8; ::_thesis: verum end; caseA14: ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ; ::_thesis: not p = f . (len f) A15: now__::_thesis:_not_p_=_f_._((Index_(p,f))_+_1) q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A14, JORDAN3:def_5; then consider r being Real such that A16: q = ((1 - r) * (f /. (Index (p,f)))) + (r * (f /. ((Index (p,f)) + 1))) and A17: 0 <= r and A18: r <= 1 ; A19: p = 1 * p by EUCLID:29 .= (0. (TOP-REAL 2)) + (1 * p) by EUCLID:27 .= ((1 - 1) * (f /. (Index (p,f)))) + (1 * p) by EUCLID:29 ; assume A20: p = f . ((Index (p,f)) + 1) ; ::_thesis: contradiction then p = f /. ((Index (p,f)) + 1) by A7, FINSEQ_4:15, NAT_1:11; then 1 <= r by A14, A16, A17, A19, JORDAN3:def_5; then r = 1 by A18, XXREAL_0:1; hence contradiction by A4, A7, A20, A16, A19, FINSEQ_4:15, NAT_1:11; ::_thesis: verum end; assume p = f . (len f) ; ::_thesis: contradiction hence contradiction by A1, A10, A15, Th18; ::_thesis: verum end; end; end; then L_Cut (f,p) is_S-Seq_joining p,f /. (len f) by A1, A2, A5, Th40; then A21: (L_Cut (f,p)) . 1 = p by JORDAN3:def_2; now__::_thesis:_(_(_Index_(p,f)_<_Index_(q,f)_&_ex_i1_being_Element_of_NAT_st_ (_1_<=_i1_&_i1_+_1_<=_len_(L_Cut_(f,p))_&_q_in_LSeg_((L_Cut_(f,p)),i1)_)_)_or_(_Index_(p,f)_=_Index_(q,f)_&_LE_p,q,f_/._(Index_(p,f)),f_/._((Index_(p,f))_+_1)_&_ex_i1_being_Element_of_NAT_st_ (_1_<=_i1_&_i1_+_1_<=_len_(L_Cut_(f,p))_&_q_in_LSeg_((L_Cut_(f,p)),i1)_)_)_) percases ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) by A8; case Index (p,f) < Index (q,f) ; ::_thesis: ex i1 being Element of NAT st ( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) ) then q in L~ (L_Cut (f,p)) by A2, A3, JORDAN3:29; hence ex i1 being Element of NAT st ( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) ) by SPPOL_2:13; ::_thesis: verum end; case ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ; ::_thesis: ex i1 being Element of NAT st ( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) ) then q in L~ (L_Cut (f,p)) by A2, A3, A4, JORDAN3:31; hence ex i1 being Element of NAT st ( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) ) by SPPOL_2:13; ::_thesis: verum end; end; end; then A22: q in L~ (L_Cut (f,p)) by SPPOL_2:17; then A23: Index (q,(L_Cut (f,p))) < len (L_Cut (f,p)) by JORDAN3:8; 1 <= Index (q,(L_Cut (f,p))) by A22, JORDAN3:8; then 1 <= len (L_Cut (f,p)) by A23, XXREAL_0:2; then p = (L_Cut (f,p)) /. 1 by A21, FINSEQ_4:15; hence B_Cut (f,p,q) is_S-Seq_joining p,q by A1, A2, A4, A5, A9, A11, A22, A21, Th42, JORDAN3:32; ::_thesis: verum end; theorem Th43: :: JORDAN23:43 for f being non empty FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & len f <> 2 & p in L~ f & q in L~ f & p <> q & p <> f . 1 & q <> f . 1 holds B_Cut (f,p,q) is_S-Seq_joining p,q proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & len f <> 2 & p in L~ f & q in L~ f & p <> q & p <> f . 1 & q <> f . 1 holds B_Cut (f,p,q) is_S-Seq_joining p,q let p, q be Point of (TOP-REAL 2); ::_thesis: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & len f <> 2 & p in L~ f & q in L~ f & p <> q & p <> f . 1 & q <> f . 1 implies B_Cut (f,p,q) is_S-Seq_joining p,q ) assume that A1: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. ) and A2: len f <> 2 and A3: p in L~ f and A4: q in L~ f and A5: p <> q and A6: p <> f . 1 and A7: q <> f . 1 ; ::_thesis: B_Cut (f,p,q) is_S-Seq_joining p,q percases ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) or ( not Index (p,f) < Index (q,f) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) ; suppose ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; ::_thesis: B_Cut (f,p,q) is_S-Seq_joining p,q hence B_Cut (f,p,q) is_S-Seq_joining p,q by A1, A3, A4, A5, A6, Lm1; ::_thesis: verum end; supposeA8: ( not Index (p,f) < Index (q,f) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; ::_thesis: B_Cut (f,p,q) is_S-Seq_joining p,q A9: now__::_thesis:_(_Index_(p,f)_=_Index_(q,f)_&_not_LE_p,q,f_/._(Index_(p,f)),f_/._((Index_(p,f))_+_1)_implies_LE_q,p,f_/._(Index_(q,f)),f_/._((Index_(q,f))_+_1)_) assume that A10: Index (p,f) = Index (q,f) and A11: not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ; ::_thesis: LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) A12: Index (p,f) < len f by A3, JORDAN3:8; A13: 1 <= Index (p,f) by A3, JORDAN3:8; then A14: Index (p,f) in dom f by A12, FINSEQ_3:25; f is weakly-one-to-one by A1, A2, Th7; then f . (Index (p,f)) <> f . ((Index (p,f)) + 1) by A13, A12, Def2; then A15: f /. (Index (p,f)) <> f . ((Index (p,f)) + 1) by A14, PARTFUN1:def_6; A16: (Index (p,f)) + 1 <= len f by A12, NAT_1:13; then A17: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A13, TOPREAL1:def_3; then A18: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, JORDAN3:9; 1 <= (Index (p,f)) + 1 by NAT_1:11; then (Index (p,f)) + 1 in dom f by A16, FINSEQ_3:25; then A19: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A15, PARTFUN1:def_6; q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A4, A10, A17, JORDAN3:9; then LT q,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A11, A18, A19, JORDAN3:28; hence LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) by A10, JORDAN3:def_6; ::_thesis: verum end; A20: ( Index (q,f) < Index (p,f) or ( Index (p,f) = Index (q,f) & not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) by A8, XXREAL_0:1; B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) by A8, JORDAN3:def_7; then A21: Rev (B_Cut (f,q,p)) = B_Cut (f,p,q) by A3, A4, A20, A9, JORDAN3:def_7; B_Cut (f,q,p) is_S-Seq_joining q,p by A1, A3, A4, A5, A7, A20, A9, Lm1; hence B_Cut (f,p,q) is_S-Seq_joining p,q by A21, JORDAN3:15; ::_thesis: verum end; end; end; theorem :: JORDAN23:44 for f being non empty FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & len f <> 2 & p in L~ f & q in L~ f & p <> q & p <> f . 1 & q <> f . 1 holds B_Cut (f,p,q) is being_S-Seq proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & len f <> 2 & p in L~ f & q in L~ f & p <> q & p <> f . 1 & q <> f . 1 holds B_Cut (f,p,q) is being_S-Seq let p, q be Point of (TOP-REAL 2); ::_thesis: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & len f <> 2 & p in L~ f & q in L~ f & p <> q & p <> f . 1 & q <> f . 1 implies B_Cut (f,p,q) is being_S-Seq ) assume that A1: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. ) and A2: len f <> 2 and A3: p in L~ f and A4: q in L~ f and A5: p <> q and A6: p <> f . 1 and A7: q <> f . 1 ; ::_thesis: B_Cut (f,p,q) is being_S-Seq B_Cut (f,p,q) is_S-Seq_joining p,q by A1, A2, A3, A4, A5, A6, A7, Th43; hence B_Cut (f,p,q) is being_S-Seq by JORDAN3:def_2; ::_thesis: verum end; theorem :: JORDAN23:45 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st p in BDD (L~ (Cage (C,n))) holds ex B being S-Sequence_in_R2 st ( B = B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) & ex P being S-Sequence_in_R2 st ( P is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P & P /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & P /. (len P) = South-Bound (p,(L~ (Cage (C,n)))) & len P >= 2 & ex B1 being S-Sequence_in_R2 st ( B1 is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ B = L~ B1 & B /. 1 = B1 /. 1 & B /. (len B) = B1 /. (len B1) & len B <= len B1 & ex g being non constant standard special_circular_sequence st g = B1 ^' P ) ) ) proof let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st p in BDD (L~ (Cage (C,n))) holds ex B being S-Sequence_in_R2 st ( B = B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) & ex P being S-Sequence_in_R2 st ( P is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P & P /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & P /. (len P) = South-Bound (p,(L~ (Cage (C,n)))) & len P >= 2 & ex B1 being S-Sequence_in_R2 st ( B1 is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ B = L~ B1 & B /. 1 = B1 /. 1 & B /. (len B) = B1 /. (len B1) & len B <= len B1 & ex g being non constant standard special_circular_sequence st g = B1 ^' P ) ) ) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st p in BDD (L~ (Cage (C,n))) holds ex B being S-Sequence_in_R2 st ( B = B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) & ex P being S-Sequence_in_R2 st ( P is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P & P /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & P /. (len P) = South-Bound (p,(L~ (Cage (C,n)))) & len P >= 2 & ex B1 being S-Sequence_in_R2 st ( B1 is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ B = L~ B1 & B /. 1 = B1 /. 1 & B /. (len B) = B1 /. (len B1) & len B <= len B1 & ex g being non constant standard special_circular_sequence st g = B1 ^' P ) ) ) let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in BDD (L~ (Cage (C,n))) implies ex B being S-Sequence_in_R2 st ( B = B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) & ex P being S-Sequence_in_R2 st ( P is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P & P /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & P /. (len P) = South-Bound (p,(L~ (Cage (C,n)))) & len P >= 2 & ex B1 being S-Sequence_in_R2 st ( B1 is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ B = L~ B1 & B /. 1 = B1 /. 1 & B /. (len B) = B1 /. (len B1) & len B <= len B1 & ex g being non constant standard special_circular_sequence st g = B1 ^' P ) ) ) ) set f = Cage (C,n); set Lf = L~ (Cage (C,n)); set a = North-Bound (p,(L~ (Cage (C,n)))); set b = South-Bound (p,(L~ (Cage (C,n)))); set Rotf = Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))); set rf = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1); A1: L~ (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) = L~ (Cage (C,n)) by REVROT_1:33; A2: (LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1))) /\ (LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1)) = {((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)} by GOBOARD7:34, REVROT_1:30; then A3: LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) meets LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) by XBOOLE_0:def_7; A4: (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2 in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)) by RLTOPSP1:68; len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) >= 1 + 1 by GOBOARD7:34, XXREAL_0:2; then A5: LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) = LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1))) by TOPREAL1:def_3; A6: (South-Bound (p,(L~ (Cage (C,n))))) `1 = p `1 by JORDAN18:16; len (Cage (C,n)) > 4 by GOBOARD7:34; then A7: ((len (Cage (C,n))) -' 1) + 1 = len (Cage (C,n)) by XREAL_1:235, XXREAL_0:2; then A8: (len (Cage (C,n))) -' 1 < len (Cage (C,n)) by NAT_1:13; set pion = <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>; A9: len (Cage (C,n)) > 1 by GOBOARD7:34, XXREAL_0:2; A10: (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))))) by RLTOPSP1:68; assume A11: p in BDD (L~ (Cage (C,n))) ; ::_thesis: ex B being S-Sequence_in_R2 st ( B = B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) & ex P being S-Sequence_in_R2 st ( P is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P & P /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & P /. (len P) = South-Bound (p,(L~ (Cage (C,n)))) & len P >= 2 & ex B1 being S-Sequence_in_R2 st ( B1 is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ B = L~ B1 & B /. 1 = B1 /. 1 & B /. (len B) = B1 /. (len B1) & len B <= len B1 & ex g being non constant standard special_circular_sequence st g = B1 ^' P ) ) ) A12: North-Bound (p,(L~ (Cage (C,n)))) <> South-Bound (p,(L~ (Cage (C,n)))) by A11, JORDAN18:20; A13: South-Bound (p,(L~ (Cage (C,n)))) in L~ (Cage (C,n)) by A11, JORDAN18:17; then A14: Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))) < len (Cage (C,n)) by JORDAN3:8; A15: for i being Nat st 1 <= i & i < Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))) holds (Cage (C,n)) /. i <> (Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))) proof let i be Nat; ::_thesis: ( 1 <= i & i < Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))) implies (Cage (C,n)) /. i <> (Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))) ) i in NAT by ORDINAL1:def_12; hence ( 1 <= i & i < Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))) implies (Cage (C,n)) /. i <> (Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))) ) by A14, GOBOARD7:36; ::_thesis: verum end; 1 <= Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))) by A13, JORDAN3:8; then A16: Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))) in dom (Cage (C,n)) by A14, FINSEQ_3:25; then ((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n)) <= Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))) by FINSEQ_5:39; then 0 + (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n))) < len (Cage (C,n)) by A14, XXREAL_0:2; then A17: (len (Cage (C,n))) - (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n))) > 1 - 1 by XREAL_1:20; A18: (Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))) in rng (Cage (C,n)) by A16, PARTFUN2:2; then len ((Cage (C,n)) :- ((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))) = ((len (Cage (C,n))) - (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n)))) + 1 by FINSEQ_5:50; then 1 < len ((Cage (C,n)) :- ((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))) by A17, XREAL_1:19; then A19: LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) = LSeg ((Cage (C,n)),((1 -' 1) + (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n))))) by A18, REVROT_1:24 .= LSeg ((Cage (C,n)),(0 + (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n))))) by XREAL_1:232 .= LSeg ((Cage (C,n)),(Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) by A16, A15, FINSEQ_6:48 ; then A20: South-Bound (p,(L~ (Cage (C,n)))) in LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) by A13, JORDAN3:9; A21: len (Cage (C,n)) > 1 + 1 by GOBOARD7:34, XXREAL_0:2; then A22: (len (Cage (C,n))) - 1 > 1 by XREAL_1:20; then A23: 1 < (len (Cage (C,n))) -' 1 by XREAL_0:def_2; A24: len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) = len (Cage (C,n)) by REVROT_1:14; then A25: LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) = LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1))) by A21, TOPREAL1:def_3; A26: (North-Bound (p,(L~ (Cage (C,n))))) `1 = p `1 by JORDAN18:16; then LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))) is vertical by A6, SPPOL_1:16; then A27: <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> is being_S-Seq by A12, JORDAN1B:7; A28: p `2 < (North-Bound (p,(L~ (Cage (C,n))))) `2 by A11, JORDAN18:18; A29: (South-Bound (p,(L~ (Cage (C,n))))) `2 < p `2 by A11, JORDAN18:18; then A30: p in LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))) by A26, A6, A28, GOBOARD7:7; A31: LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) = LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))))) by A24, A22, A7, TOPREAL1:def_3; reconsider rf = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) as S-Sequence_in_R2 by A24, A22, A7, JORDAN4:37; A32: L~ (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) = (L~ rf) \/ (LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1))) by A24, A22, A7, GOBOARD2:3; A33: (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1 = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) by FINSEQ_6:def_1; A34: (South-Bound (p,(L~ (Cage (C,n))))) `2 < (North-Bound (p,(L~ (Cage (C,n))))) `2 by A29, A28, XXREAL_0:2; A35: now__::_thesis:_not_North-Bound_(p,(L~_(Cage_(C,n))))_in_LSeg_((Rotate_((Cage_(C,n)),((Cage_(C,n))_/._(Index_((South-Bound_(p,(L~_(Cage_(C,n))))),(Cage_(C,n))))))),((len_(Rotate_((Cage_(C,n)),((Cage_(C,n))_/._(Index_((South-Bound_(p,(L~_(Cage_(C,n))))),(Cage_(C,n))))))))_-'_1)) assume A36: North-Bound (p,(L~ (Cage (C,n)))) in LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) ; ::_thesis: contradiction percases ( ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is vertical & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is vertical ) or ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is vertical & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is horizontal ) or ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is horizontal & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is vertical ) or ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is horizontal & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is horizontal ) ) by SPPOL_1:19; supposeA37: ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is vertical & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is vertical ) ; ::_thesis: contradiction then A38: (South-Bound (p,(L~ (Cage (C,n))))) `1 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1 by A13, A19, A25, JORDAN3:9, SPPOL_1:41; A39: ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `1 by A25, A37, SPPOL_1:16; A40: ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `1 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `1 by A31, A37, SPPOL_1:16; percases ( (South-Bound (p,(L~ (Cage (C,n))))) `2 < ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 or ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 < (North-Bound (p,(L~ (Cage (C,n))))) `2 ) by A34, XXREAL_0:2; supposeA41: (South-Bound (p,(L~ (Cage (C,n))))) `2 < ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 ; ::_thesis: contradiction then A42: (((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2 < ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 by XREAL_1:226; A43: (South-Bound (p,(L~ (Cage (C,n))))) `2 < (((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2 by A41, XREAL_1:226; set p1 = |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]|; A44: |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `1 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1 by EUCLID:52; A45: |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `2 = (((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2 by EUCLID:52; A46: ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 > ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 by A20, A25, A41, TOPREAL1:4; then ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 <= (South-Bound (p,(L~ (Cage (C,n))))) `2 by A20, A25, TOPREAL1:4; then ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 < |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `2 by A45, A43, XXREAL_0:2; then A47: |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in L~ (Cage (C,n)) by A1, A5, A39, A44, A45, A42, GOBOARD7:7, SPPOL_2:17; ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `2 <= ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 proof A48: ( ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 < ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 or ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 >= ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 ) ; assume ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `2 > ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 ; ::_thesis: contradiction then ( (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2 in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))))) or (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)) ) by A33, A39, A40, A46, A48, GOBOARD7:7; then ( (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2 in {((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)} or (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) in {((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)} ) by A4, A10, A2, A25, A31, XBOOLE_0:def_4; then ( (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1) = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1 or (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) ) by A33, TARSKI:def_1; hence contradiction by A24, A22, A9, A7, A8, Th5; ::_thesis: verum end; then A49: ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `2 <= (North-Bound (p,(L~ (Cage (C,n))))) `2 by A31, A36, TOPREAL1:4; then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `2 < (North-Bound (p,(L~ (Cage (C,n))))) `2 by A33, A45, A42, XXREAL_0:2; then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in LSeg ((South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) by A26, A6, A38, A44, A45, A43, GOBOARD7:7; then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) by A47, XBOOLE_0:def_4; then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A11, JORDAN18:22; hence contradiction by A33, A45, A43, A42, A49, TARSKI:def_2; ::_thesis: verum end; supposeA50: ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 < (North-Bound (p,(L~ (Cage (C,n))))) `2 ; ::_thesis: contradiction then A51: (((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2 < (North-Bound (p,(L~ (Cage (C,n))))) `2 by XREAL_1:226; A52: ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 < (((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2 by A50, XREAL_1:226; set p1 = |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]|; A53: |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `1 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1 by EUCLID:52; A54: |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `2 = (((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2 by EUCLID:52; A55: ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 > ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `2 by A33, A31, A36, A50, TOPREAL1:4; then (North-Bound (p,(L~ (Cage (C,n))))) `2 <= ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 by A31, A36, TOPREAL1:4; then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `2 < ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 by A54, A51, XXREAL_0:2; then A56: |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in L~ (Cage (C,n)) by A1, A33, A31, A40, A53, A54, A52, GOBOARD7:7, SPPOL_2:17; ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 <= ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 proof A57: ( ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 < ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 or ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 >= ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 ) ; assume ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 > ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 ; ::_thesis: contradiction then ( (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2 in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))))) or (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)) ) by A33, A39, A40, A55, A57, GOBOARD7:7; then ( (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2 in {((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)} or (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) in {((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)} ) by A4, A10, A2, A25, A31, XBOOLE_0:def_4; then ( (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1) = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1 or (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) ) by A33, TARSKI:def_1; hence contradiction by A24, A22, A9, A7, A8, Th5; ::_thesis: verum end; then A58: (South-Bound (p,(L~ (Cage (C,n))))) `2 <= ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 by A20, A25, TOPREAL1:4; then (South-Bound (p,(L~ (Cage (C,n))))) `2 < |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `2 by A54, A52, XXREAL_0:2; then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in LSeg ((South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) by A26, A6, A38, A53, A54, A51, GOBOARD7:7; then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) by A56, XBOOLE_0:def_4; then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A11, JORDAN18:22; hence contradiction by A54, A52, A51, A58, TARSKI:def_2; ::_thesis: verum end; end; end; supposeA59: ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is vertical & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is horizontal ) ; ::_thesis: contradiction then A60: (North-Bound (p,(L~ (Cage (C,n))))) `2 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `2 by A31, A36, SPPOL_1:40; (North-Bound (p,(L~ (Cage (C,n))))) `1 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `1 by A26, A6, A13, A19, A33, A25, A59, JORDAN3:9, SPPOL_1:41; then North-Bound (p,(L~ (Cage (C,n)))) = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) by A60, TOPREAL3:6; then North-Bound (p,(L~ (Cage (C,n)))) in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2)) by A33, RLTOPSP1:68; then LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))) c= LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2)) by A20, A25, TOPREAL1:6; then p in L~ (Cage (C,n)) by A1, A30, A25, SPPOL_2:17; then p in (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) by A30, XBOOLE_0:def_4; then p in {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A11, JORDAN18:22; hence contradiction by A29, A28, TARSKI:def_2; ::_thesis: verum end; supposeA61: ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is horizontal & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is vertical ) ; ::_thesis: contradiction then A62: (South-Bound (p,(L~ (Cage (C,n))))) `2 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 by A13, A19, A25, JORDAN3:9, SPPOL_1:40; (South-Bound (p,(L~ (Cage (C,n))))) `1 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1 by A26, A6, A33, A31, A36, A61, SPPOL_1:41; then South-Bound (p,(L~ (Cage (C,n)))) = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1 by A62, TOPREAL3:6; then South-Bound (p,(L~ (Cage (C,n)))) in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))))) by A33, RLTOPSP1:68; then LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))) c= LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))))) by A31, A36, TOPREAL1:6; then p in L~ (Cage (C,n)) by A1, A30, A31, SPPOL_2:17; then p in (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) by A30, XBOOLE_0:def_4; then p in {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A11, JORDAN18:22; hence contradiction by A29, A28, TARSKI:def_2; ::_thesis: verum end; supposeA63: ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is horizontal & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is horizontal ) ; ::_thesis: contradiction then A64: (North-Bound (p,(L~ (Cage (C,n))))) `2 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 by A31, A36, SPPOL_1:40; (South-Bound (p,(L~ (Cage (C,n))))) `2 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 by A13, A19, A25, A63, JORDAN3:9, SPPOL_1:40; hence contradiction by A29, A28, A3, A25, A31, A63, A64, SPRECT_3:9; ::_thesis: verum end; end; end; North-Bound (p,(L~ (Cage (C,n)))) in L~ (Cage (C,n)) by A11, JORDAN18:17; then A65: North-Bound (p,(L~ (Cage (C,n)))) in L~ rf by A1, A35, A32, XBOOLE_0:def_3; len rf = (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1 by FINSEQ_1:59, NAT_D:35; then 1 + 1 <= len rf by A24, A23, NAT_1:13; then A66: South-Bound (p,(L~ (Cage (C,n)))) in LSeg (rf,1) by A20, SPPOL_2:3; A67: LSeg (rf,1) c= L~ rf by TOPREAL3:19; then reconsider BCut = B_Cut (rf,(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) as S-Sequence_in_R2 by A11, A66, A65, JORDAN18:20, JORDAN3:37; A68: (len BCut) + 1 >= 1 by NAT_1:11; set Ga = GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>); now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_BCut_holds_ ex_i,_j_being_Element_of_NAT_st_ (_[i,j]_in_Indices_(GoB_(BCut_^'_<*(North-Bound_(p,(L~_(Cage_(C,n))))),(South-Bound_(p,(L~_(Cage_(C,n)))))*>))_&_BCut_/._n_=_(GoB_(BCut_^'_<*(North-Bound_(p,(L~_(Cage_(C,n))))),(South-Bound_(p,(L~_(Cage_(C,n)))))*>))_*_(i,j)_) let n be Element of NAT ; ::_thesis: ( n in dom BCut implies ex i, j being Element of NAT st ( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & BCut /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) ) ) assume A69: n in dom BCut ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & BCut /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) ) then A70: n <= len BCut by FINSEQ_3:25; dom BCut c= dom (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) by Th23; then consider i, j being Element of NAT such that A71: [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) and A72: (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) by A69, GOBOARD2:14; take i = i; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & BCut /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) ) take j = j; ::_thesis: ( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & BCut /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) ) thus [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) by A71; ::_thesis: BCut /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) 1 <= n by A69, FINSEQ_3:25; hence BCut /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) by A72, A70, GRAPH_2:57; ::_thesis: verum end; then consider BCut1 being FinSequence of (TOP-REAL 2) such that A73: BCut1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) and A74: BCut1 is being_S-Seq and A75: L~ BCut = L~ BCut1 and A76: BCut /. 1 = BCut1 /. 1 and A77: BCut /. (len BCut) = BCut1 /. (len BCut1) and A78: len BCut <= len BCut1 by GOBOARD3:2; reconsider BCut1 = BCut1 as S-Sequence_in_R2 by A74; A79: L~ BCut1 c= L~ rf by A67, A66, A65, A75, JORDAN5B:24; A80: len BCut1 in dom BCut1 by FINSEQ_5:6; A81: 1 in dom BCut1 by FINSEQ_5:6; A82: now__::_thesis:_not_BCut1_is_constant assume BCut1 is constant ; ::_thesis: contradiction then BCut1 /. 1 = BCut1 /. (len BCut1) by A81, A80, REVROT_1:def_1; then BCut1 /. (len BCut1) = South-Bound (p,(L~ (Cage (C,n)))) by A67, A66, A65, A76, Th19; hence contradiction by A11, A67, A66, A65, A77, Th20, JORDAN18:20; ::_thesis: verum end; BCut /. (len BCut) = North-Bound (p,(L~ (Cage (C,n)))) by A67, A66, A65, Th20; then A83: North-Bound (p,(L~ (Cage (C,n)))) in LSeg ((BCut1 /. ((len BCut1) -' 1)),(BCut1 /. (len BCut1))) by A77, RLTOPSP1:68; A84: len BCut1 >= 1 + 1 by TOPREAL1:def_8; then A85: (len BCut1) - 1 >= 1 by XREAL_1:19; take BCut ; ::_thesis: ( BCut = B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) & ex P being S-Sequence_in_R2 st ( P is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P & P /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & P /. (len P) = South-Bound (p,(L~ (Cage (C,n)))) & len P >= 2 & ex B1 being S-Sequence_in_R2 st ( B1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ BCut = L~ B1 & BCut /. 1 = B1 /. 1 & BCut /. (len BCut) = B1 /. (len B1) & len BCut <= len B1 & ex g being non constant standard special_circular_sequence st g = B1 ^' P ) ) ) thus BCut = B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) ; ::_thesis: ex P being S-Sequence_in_R2 st ( P is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P & P /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & P /. (len P) = South-Bound (p,(L~ (Cage (C,n)))) & len P >= 2 & ex B1 being S-Sequence_in_R2 st ( B1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ BCut = L~ B1 & BCut /. 1 = B1 /. 1 & BCut /. (len BCut) = B1 /. (len B1) & len BCut <= len B1 & ex g being non constant standard special_circular_sequence st g = B1 ^' P ) ) A86: (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) = {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A11, JORDAN18:22; len BCut > 0 by NAT_1:3; then A87: len BCut >= 0 + 1 by NAT_1:13; then A88: (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) /. (len BCut) = BCut /. (len BCut) by GRAPH_2:57 .= North-Bound (p,(L~ (Cage (C,n)))) by A67, A66, A65, Th20 .= <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. 1 by FINSEQ_4:17 ; A89: len <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = 1 + 1 by FINSEQ_1:44; then A90: (len (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) + 1 = (len BCut) + (1 + 1) by GRAPH_2:13 .= ((len BCut) + 1) + 1 ; then A91: len BCut < len (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) by NAT_1:13; now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_<*(North-Bound_(p,(L~_(Cage_(C,n))))),(South-Bound_(p,(L~_(Cage_(C,n)))))*>_holds_ ex_i,_j_being_Element_of_NAT_st_ (_[i,j]_in_Indices_(GoB_(BCut_^'_<*(North-Bound_(p,(L~_(Cage_(C,n))))),(South-Bound_(p,(L~_(Cage_(C,n)))))*>))_&_<*(North-Bound_(p,(L~_(Cage_(C,n))))),(South-Bound_(p,(L~_(Cage_(C,n)))))*>_/._n_=_(GoB_(BCut_^'_<*(North-Bound_(p,(L~_(Cage_(C,n))))),(South-Bound_(p,(L~_(Cage_(C,n)))))*>))_*_(i,j)_) let n be Element of NAT ; ::_thesis: ( n in dom <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> implies ex i, j being Element of NAT st ( [j,b3] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. i = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (j,b3) ) ) assume n in dom <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> ; ::_thesis: ex i, j being Element of NAT st ( [j,b3] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. i = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (j,b3) ) then A92: n in Seg 2 by FINSEQ_1:89; percases ( n = 1 or n = 1 + 1 ) by A92, FINSEQ_1:2, TARSKI:def_2; supposeA93: n = 1 ; ::_thesis: ex i, j being Element of NAT st ( [j,b3] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. i = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (j,b3) ) len BCut in Seg (len (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) by A91, A87, FINSEQ_1:1; then len BCut in dom (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) by FINSEQ_1:def_3; then consider i, j being Element of NAT such that A94: [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) and A95: (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) /. (len BCut) = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) by GOBOARD2:14; take i = i; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) ) take j = j; ::_thesis: ( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) ) thus [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) by A94; ::_thesis: <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) thus <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) by A88, A93, A95; ::_thesis: verum end; supposeA96: n = 1 + 1 ; ::_thesis: ex i, j being Element of NAT st ( [j,b3] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. i = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (j,b3) ) (len BCut) + 1 in dom (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) by A90, A68, FINSEQ_3:25; then consider i, j being Element of NAT such that A97: [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) and A98: (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) /. ((len BCut) + 1) = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) by GOBOARD2:14; take i = i; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) ) take j = j; ::_thesis: ( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) ) thus [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) by A97; ::_thesis: <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) thus <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) by A89, A96, A98, GRAPH_2:58; ::_thesis: verum end; end; end; then consider pion1 being FinSequence of (TOP-REAL 2) such that A99: pion1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) and A100: pion1 is being_S-Seq and A101: L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ pion1 and A102: <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. 1 = pion1 /. 1 and A103: <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. (len <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) = pion1 /. (len pion1) and A104: len <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> <= len pion1 by A27, GOBOARD3:2; reconsider pion1 = pion1 as S-Sequence_in_R2 by A100; A105: pion1 /. (len pion1) = South-Bound (p,(L~ (Cage (C,n)))) by A89, A103, FINSEQ_4:17 .= BCut1 /. 1 by A67, A66, A65, A76, Th19 ; A106: L~ rf c= L~ (Cage (C,n)) by A1, TOPREAL3:20; then L~ BCut1 c= L~ (Cage (C,n)) by A79, XBOOLE_1:1; then (L~ BCut1) /\ (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) c= {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A86, XBOOLE_1:26; then (L~ BCut1) /\ (L~ pion1) c= {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A101, SPPOL_2:21; then (L~ BCut1) /\ (L~ pion1) c= {(North-Bound (p,(L~ (Cage (C,n))))),(BCut1 /. 1)} by A67, A66, A65, A76, Th19; then A107: (L~ BCut1) /\ (L~ pion1) c= {(BCut1 /. 1),(pion1 /. 1)} by A102, FINSEQ_4:17; len BCut1 > 1 by A84, NAT_1:13; then A108: ((len BCut1) -' 1) + 1 = len BCut1 by XREAL_1:235; A109: BCut1 /. (len BCut1) = North-Bound (p,(L~ (Cage (C,n)))) by A67, A66, A65, A77, Th20 .= pion1 /. 1 by A102, FINSEQ_4:17 ; then A110: BCut1 ^' pion1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) by A99, A73, TOPREAL8:12; A111: L~ BCut1 c= L~ (Cage (C,n)) by A106, A79, XBOOLE_1:1; A112: now__::_thesis:_not_South-Bound_(p,(L~_(Cage_(C,n))))_in_LSeg_(BCut1,((len_BCut1)_-'_1)) assume South-Bound (p,(L~ (Cage (C,n)))) in LSeg (BCut1,((len BCut1) -' 1)) ; ::_thesis: contradiction then South-Bound (p,(L~ (Cage (C,n)))) in LSeg ((BCut1 /. ((len BCut1) -' 1)),(BCut1 /. (len BCut1))) by A85, A108, TOPREAL1:def_3; then LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))) c= LSeg ((BCut1 /. ((len BCut1) -' 1)),(BCut1 /. (len BCut1))) by A83, TOPREAL1:6; then p in LSeg ((BCut1 /. ((len BCut1) -' 1)),(BCut1 /. (len BCut1))) by A30; then p in LSeg (BCut1,((len BCut1) -' 1)) by A85, A108, TOPREAL1:def_3; then p in L~ BCut1 by SPPOL_2:17; then p in (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) by A30, A111, XBOOLE_0:def_4; then p in {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A11, JORDAN18:22; hence contradiction by A29, A28, TARSKI:def_2; ::_thesis: verum end; LSeg (BCut1,((len BCut1) -' 1)) c= L~ BCut1 by TOPREAL3:19; then LSeg (BCut1,((len BCut1) -' 1)) c= L~ rf by A79, XBOOLE_1:1; then A113: LSeg (BCut1,((len BCut1) -' 1)) c= L~ (Cage (C,n)) by A106, XBOOLE_1:1; LSeg (pion1,1) c= L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> by A101, TOPREAL3:19; then LSeg (pion1,1) c= LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))) by SPPOL_2:21; then (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) c= (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) by A113, XBOOLE_1:27; then A114: (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) c= {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A11, JORDAN18:22; A115: (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) = {(BCut1 /. (len BCut1))} proof thus (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) c= {(BCut1 /. (len BCut1))} :: according to XBOOLE_0:def_10 ::_thesis: {(BCut1 /. (len BCut1))} c= (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) or x in {(BCut1 /. (len BCut1))} ) assume A116: x in (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) ; ::_thesis: x in {(BCut1 /. (len BCut1))} then x <> South-Bound (p,(L~ (Cage (C,n)))) by A112, XBOOLE_0:def_4; then x = North-Bound (p,(L~ (Cage (C,n)))) by A114, A116, TARSKI:def_2; then x = BCut1 /. (len BCut1) by A67, A66, A65, A77, Th20; hence x in {(BCut1 /. (len BCut1))} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(BCut1 /. (len BCut1))} or x in (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) ) assume x in {(BCut1 /. (len BCut1))} ; ::_thesis: x in (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) then A117: x = BCut1 /. (len BCut1) by TARSKI:def_1; then x in LSeg ((BCut1 /. ((len BCut1) -' 1)),(BCut1 /. (len BCut1))) by RLTOPSP1:68; then A118: x in LSeg (BCut1,((len BCut1) -' 1)) by A85, A108, TOPREAL1:def_3; x in LSeg ((pion1 /. 1),(pion1 /. (1 + 1))) by A109, A117, RLTOPSP1:68; then x in LSeg (pion1,1) by A89, A104, TOPREAL1:def_3; hence x in (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) by A118, XBOOLE_0:def_4; ::_thesis: verum end; take pion1 ; ::_thesis: ( pion1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ pion1 & pion1 /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & pion1 /. (len pion1) = South-Bound (p,(L~ (Cage (C,n)))) & len pion1 >= 2 & ex B1 being S-Sequence_in_R2 st ( B1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ BCut = L~ B1 & BCut /. 1 = B1 /. 1 & BCut /. (len BCut) = B1 /. (len B1) & len BCut <= len B1 & ex g being non constant standard special_circular_sequence st g = B1 ^' pion1 ) ) len <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = 2 by FINSEQ_1:44; hence ( pion1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ pion1 & pion1 /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & pion1 /. (len pion1) = South-Bound (p,(L~ (Cage (C,n)))) & len pion1 >= 2 ) by A99, A101, A102, A103, A104, FINSEQ_4:17; ::_thesis: ex B1 being S-Sequence_in_R2 st ( B1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ BCut = L~ B1 & BCut /. 1 = B1 /. 1 & BCut /. (len BCut) = B1 /. (len B1) & len BCut <= len B1 & ex g being non constant standard special_circular_sequence st g = B1 ^' pion1 ) set g = BCut1 ^' pion1; now__::_thesis:_not_len_BCut_=_1 assume len BCut = 1 ; ::_thesis: contradiction then BCut /. 1 = North-Bound (p,(L~ (Cage (C,n)))) by A67, A66, A65, Th20; hence contradiction by A12, A67, A66, A65, Th19; ::_thesis: verum end; then len BCut > 1 by A87, XXREAL_0:1; then len BCut1 > 1 by A78, XXREAL_0:2; then A119: len BCut1 >= 1 + 1 by NAT_1:13; {(BCut1 /. 1),(pion1 /. 1)} c= (L~ BCut1) /\ (L~ pion1) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(BCut1 /. 1),(pion1 /. 1)} or x in (L~ BCut1) /\ (L~ pion1) ) assume x in {(BCut1 /. 1),(pion1 /. 1)} ; ::_thesis: x in (L~ BCut1) /\ (L~ pion1) then A120: ( x = BCut1 /. 1 or x = pion1 /. 1 ) by TARSKI:def_2; then A121: x in L~ BCut1 by A109, A119, JORDAN3:1; x in L~ pion1 by A89, A104, A105, A120, JORDAN3:1; hence x in (L~ BCut1) /\ (L~ pion1) by A121, XBOOLE_0:def_4; ::_thesis: verum end; then (L~ BCut1) /\ (L~ pion1) = {(BCut1 /. 1),(pion1 /. 1)} by A107, XBOOLE_0:def_10; then reconsider g = BCut1 ^' pion1 as non constant standard special_circular_sequence by A109, A82, A110, A115, A105, Th25, JORDAN8:4, TOPREAL8:11, TOPREAL8:33, TOPREAL8:34; take BCut1 ; ::_thesis: ( BCut1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ BCut = L~ BCut1 & BCut /. 1 = BCut1 /. 1 & BCut /. (len BCut) = BCut1 /. (len BCut1) & len BCut <= len BCut1 & ex g being non constant standard special_circular_sequence st g = BCut1 ^' pion1 ) thus ( BCut1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ BCut = L~ BCut1 & BCut /. 1 = BCut1 /. 1 & BCut /. (len BCut) = BCut1 /. (len BCut1) & len BCut <= len BCut1 ) by A73, A75, A76, A77, A78; ::_thesis: ex g being non constant standard special_circular_sequence st g = BCut1 ^' pion1 take g ; ::_thesis: g = BCut1 ^' pion1 thus g = BCut1 ^' pion1 ; ::_thesis: verum end;