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