:: by Yatsuka Nakamura and Roman Matuszewski

::

:: Received December 10, 1996

:: Copyright (c) 1996-2016 Association of Mizar Users

theorem :: JORDAN3:1

for n being Nat

for f being FinSequence of (TOP-REAL n) st 2 <= len f holds

( f . 1 in L~ f & f /. 1 in L~ f & f . (len f) in L~ f & f /. (len f) in L~ f )

for f being FinSequence of (TOP-REAL n) st 2 <= len f holds

( f . 1 in L~ f & f /. 1 in L~ f & f . (len f) in L~ f & f /. (len f) in L~ f )

proof end;

theorem Th2: :: JORDAN3:2

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st ( p1 `1 = p2 `1 or p1 `2 = p2 `2 ) & q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) & not q1 `1 = q2 `1 holds

q1 `2 = q2 `2

q1 `2 = q2 `2

proof end;

theorem Th3: :: JORDAN3:3

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st ( p1 `1 = p2 `1 or p1 `2 = p2 `2 ) & LSeg (q1,q2) c= LSeg (p1,p2) & not q1 `1 = q2 `1 holds

q1 `2 = q2 `2

q1 `2 = q2 `2

proof end;

theorem Th4: :: JORDAN3:4

for f being FinSequence of (TOP-REAL 2)

for n being Element of NAT st 2 <= n & f is being_S-Seq holds

f | n is being_S-Seq

for n being Element of NAT st 2 <= n & f is being_S-Seq holds

f | n is being_S-Seq

proof end;

theorem Th5: :: JORDAN3:5

for f being FinSequence of (TOP-REAL 2)

for n being Element of NAT st n <= len f & 2 <= (len f) -' n & f is being_S-Seq holds

f /^ n is being_S-Seq

for n being Element of NAT st n <= len f & 2 <= (len f) -' n & f is being_S-Seq holds

f /^ n is being_S-Seq

proof end;

theorem :: JORDAN3:6

for f being FinSequence of (TOP-REAL 2)

for k1, k2 being Element of NAT st f is being_S-Seq & 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & k1 <> k2 holds

mid (f,k1,k2) is being_S-Seq

for k1, k2 being Element of NAT st f is being_S-Seq & 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & k1 <> k2 holds

mid (f,k1,k2) is being_S-Seq

proof end;

definition

let f be FinSequence of (TOP-REAL 2);

let p be Point of (TOP-REAL 2);

assume A1: p in L~ f ;

ex b_{1} being Element of NAT ex S being non empty Subset of NAT st

( b_{1} = min S & S = { i where i is Nat : p in LSeg (f,i) } )

for b_{1}, b_{2} being Element of NAT st ex S being non empty Subset of NAT st

( b_{1} = min S & S = { i where i is Nat : p in LSeg (f,i) } ) & ex S being non empty Subset of NAT st

( b_{2} = min S & S = { i where i is Nat : p in LSeg (f,i) } ) holds

b_{1} = b_{2}
;

end;
let p be Point of (TOP-REAL 2);

assume A1: p in L~ f ;

func Index (p,f) -> Element of NAT means :Def1: :: JORDAN3:def 1

ex S being non empty Subset of NAT st

( it = min S & S = { i where i is Nat : p in LSeg (f,i) } );

existence ex S being non empty Subset of NAT st

( it = min S & S = { i where i is Nat : p in LSeg (f,i) } );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

:: deftheorem Def1 defines Index JORDAN3:def 1 :

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f holds

for b_{3} being Element of NAT holds

( b_{3} = Index (p,f) iff ex S being non empty Subset of NAT st

( b_{3} = min S & S = { i where i is Nat : p in LSeg (f,i) } ) );

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f holds

for b

( b

( b

theorem Th7: :: JORDAN3:7

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for i being Element of NAT st p in LSeg (f,i) holds

Index (p,f) <= i

for p being Point of (TOP-REAL 2)

for i being Element of NAT st p in LSeg (f,i) holds

Index (p,f) <= i

proof end;

theorem Th8: :: JORDAN3:8

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f holds

( 1 <= Index (p,f) & Index (p,f) < len f )

for p being Point of (TOP-REAL 2) st p in L~ f holds

( 1 <= Index (p,f) & Index (p,f) < len f )

proof end;

theorem Th9: :: JORDAN3:9

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f holds

p in LSeg (f,(Index (p,f)))

for p being Point of (TOP-REAL 2) st p in L~ f holds

p in LSeg (f,(Index (p,f)))

proof end;

theorem Th10: :: JORDAN3:10

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in LSeg (f,1) holds

Index (p,f) = 1

for p being Point of (TOP-REAL 2) st p in LSeg (f,1) holds

Index (p,f) = 1

proof end;

theorem Th11: :: JORDAN3:11

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st len f >= 2 holds

Index ((f /. 1),f) = 1

for p being Point of (TOP-REAL 2) st len f >= 2 holds

Index ((f /. 1),f) = 1

proof end;

theorem Th12: :: JORDAN3:12

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for i1 being Nat st f is being_S-Seq & 1 < i1 & i1 <= len f & p = f . i1 holds

(Index (p,f)) + 1 = i1

for p being Point of (TOP-REAL 2)

for i1 being Nat st f is being_S-Seq & 1 < i1 & i1 <= len f & p = f . i1 holds

(Index (p,f)) + 1 = i1

proof end;

theorem Th13: :: JORDAN3:13

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 s.n.c. & p in LSeg (f,i1) & not i1 = Index (p,f) holds

i1 = (Index (p,f)) + 1

for p being Point of (TOP-REAL 2)

for i1 being Element of NAT st f is s.n.c. & p in LSeg (f,i1) & not i1 = Index (p,f) holds

i1 = (Index (p,f)) + 1

proof end;

theorem Th14: :: JORDAN3:14

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 unfolded & f is s.n.c. & i1 + 1 <= len f & p in LSeg (f,i1) & p <> f . i1 holds

i1 = Index (p,f)

for p being Point of (TOP-REAL 2)

for i1 being Element of NAT st f is unfolded & f is s.n.c. & i1 + 1 <= len f & p in LSeg (f,i1) & p <> f . i1 holds

i1 = Index (p,f)

proof end;

definition

let g be FinSequence of (TOP-REAL 2);

let p1, p2 be Point of (TOP-REAL 2);

end;
let p1, p2 be Point of (TOP-REAL 2);

pred g is_S-Seq_joining p1,p2 means :: JORDAN3:def 2

( g is being_S-Seq & g . 1 = p1 & g . (len g) = p2 );

( g is being_S-Seq & g . 1 = p1 & g . (len g) = p2 );

:: deftheorem defines is_S-Seq_joining JORDAN3:def 2 :

for g being FinSequence of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) holds

( g is_S-Seq_joining p1,p2 iff ( g is being_S-Seq & g . 1 = p1 & g . (len g) = p2 ) );

for g being FinSequence of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) holds

( g is_S-Seq_joining p1,p2 iff ( g is being_S-Seq & g . 1 = p1 & g . (len g) = p2 ) );

theorem Th15: :: JORDAN3:15

for g being FinSequence of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st g is_S-Seq_joining p1,p2 holds

Rev g is_S-Seq_joining p2,p1

for p1, p2 being Point of (TOP-REAL 2) st g is_S-Seq_joining p1,p2 holds

Rev g is_S-Seq_joining p2,p1

proof end;

theorem Th16: :: JORDAN3:16

for f, g being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for j being Nat st p in L~ f & g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) & 1 <= j & j + 1 <= len g holds

LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1))

for p being Point of (TOP-REAL 2)

for j being Nat st p in L~ f & g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) & 1 <= j & j + 1 <= len g holds

LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1))

proof end;

theorem :: JORDAN3:17

for f, g being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p <> f . ((Index (p,f)) + 1) & g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) holds

g is_S-Seq_joining p,f /. (len f)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p <> f . ((Index (p,f)) + 1) & g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) holds

g is_S-Seq_joining p,f /. (len f)

proof end;

theorem Th18: :: JORDAN3:18

for f, g being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for j being Nat st p in L~ f & 1 <= j & j + 1 <= len g & g = (mid (f,1,(Index (p,f)))) ^ <*p*> holds

LSeg (g,j) c= LSeg (f,j)

for p being Point of (TOP-REAL 2)

for j being Nat st p in L~ f & 1 <= j & j + 1 <= len g & g = (mid (f,1,(Index (p,f)))) ^ <*p*> holds

LSeg (g,j) c= LSeg (f,j)

proof end;

theorem Th19: :: JORDAN3:19

for f, g being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p <> f . 1 & g = (mid (f,1,(Index (p,f)))) ^ <*p*> holds

g is_S-Seq_joining f /. 1,p

for p being Point of (TOP-REAL 2) st f is being_S-Seq & 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 end;

::----------------------------------------------------------------------:

:: Left and Right Cutting Functions for Finite Sequences in TOP-REAL 2 :

::----------------------------------------------------------------------:

:: Left and Right Cutting Functions for Finite Sequences in TOP-REAL 2 :

::----------------------------------------------------------------------:

definition

let f be FinSequence of (TOP-REAL 2);

let p be Point of (TOP-REAL 2);

coherence

( ( p <> f . ((Index (p,f)) + 1) implies <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) is FinSequence of (TOP-REAL 2) ) & ( not p <> f . ((Index (p,f)) + 1) implies mid (f,((Index (p,f)) + 1),(len f)) is FinSequence of (TOP-REAL 2) ) );

consistency

for b_{1} being FinSequence of (TOP-REAL 2) holds verum;

;

coherence

( ( p <> f . 1 implies (mid (f,1,(Index (p,f)))) ^ <*p*> is FinSequence of (TOP-REAL 2) ) & ( not p <> f . 1 implies <*p*> is FinSequence of (TOP-REAL 2) ) );

consistency

for b_{1} being FinSequence of (TOP-REAL 2) holds verum;

;

end;
let p be Point of (TOP-REAL 2);

func L_Cut (f,p) -> FinSequence of (TOP-REAL 2) equals :Def3: :: JORDAN3:def 3

<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) if p <> f . ((Index (p,f)) + 1)

otherwise mid (f,((Index (p,f)) + 1),(len f));

correctness <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) if p <> f . ((Index (p,f)) + 1)

otherwise mid (f,((Index (p,f)) + 1),(len f));

coherence

( ( p <> f . ((Index (p,f)) + 1) implies <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) is FinSequence of (TOP-REAL 2) ) & ( not p <> f . ((Index (p,f)) + 1) implies mid (f,((Index (p,f)) + 1),(len f)) is FinSequence of (TOP-REAL 2) ) );

consistency

for b

;

func R_Cut (f,p) -> FinSequence of (TOP-REAL 2) equals :Def4: :: JORDAN3:def 4

(mid (f,1,(Index (p,f)))) ^ <*p*> if p <> f . 1

otherwise <*p*>;

correctness (mid (f,1,(Index (p,f)))) ^ <*p*> if p <> f . 1

otherwise <*p*>;

coherence

( ( p <> f . 1 implies (mid (f,1,(Index (p,f)))) ^ <*p*> is FinSequence of (TOP-REAL 2) ) & ( not p <> f . 1 implies <*p*> is FinSequence of (TOP-REAL 2) ) );

consistency

for b

;

:: deftheorem Def3 defines L_Cut JORDAN3:def 3 :

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) holds

( ( p <> f . ((Index (p,f)) + 1) implies L_Cut (f,p) = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) ) & ( not p <> f . ((Index (p,f)) + 1) implies L_Cut (f,p) = mid (f,((Index (p,f)) + 1),(len f)) ) );

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) holds

( ( p <> f . ((Index (p,f)) + 1) implies L_Cut (f,p) = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) ) & ( not p <> f . ((Index (p,f)) + 1) implies L_Cut (f,p) = mid (f,((Index (p,f)) + 1),(len f)) ) );

:: deftheorem Def4 defines R_Cut JORDAN3:def 4 :

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) holds

( ( p <> f . 1 implies R_Cut (f,p) = (mid (f,1,(Index (p,f)))) ^ <*p*> ) & ( not p <> f . 1 implies R_Cut (f,p) = <*p*> ) );

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) holds

( ( p <> f . 1 implies R_Cut (f,p) = (mid (f,1,(Index (p,f)))) ^ <*p*> ) & ( not p <> f . 1 implies R_Cut (f,p) = <*p*> ) );

theorem Th20: :: JORDAN3:20

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & 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

for p being Point of (TOP-REAL 2) st f is being_S-Seq & 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 end;

theorem Th21: :: JORDAN3:21

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f is unfolded & f is s.n.c. & p in L~ f & p <> f . ((Index (p,f)) + 1) holds

(Index (p,(Rev f))) + (Index (p,f)) = len f

for p being Point of (TOP-REAL 2) st f is unfolded & f is s.n.c. & p in L~ f & p <> f . ((Index (p,f)) + 1) holds

(Index (p,(Rev f))) + (Index (p,f)) = len f

proof end;

theorem Th22: :: JORDAN3:22

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f holds

L_Cut ((Rev f),p) = Rev (R_Cut (f,p))

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f holds

L_Cut ((Rev f),p) = Rev (R_Cut (f,p))

proof end;

theorem Th23: :: JORDAN3:23

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f holds

( (L_Cut (f,p)) . 1 = p & ( for i being Nat st 1 < i & i <= len (L_Cut (f,p)) holds

( ( p = f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . ((Index (p,f)) + i) ) & ( p <> f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . (((Index (p,f)) + i) - 1) ) ) ) )

for p being Point of (TOP-REAL 2) st p in L~ f holds

( (L_Cut (f,p)) . 1 = p & ( for i being Nat st 1 < i & i <= len (L_Cut (f,p)) holds

( ( p = f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . ((Index (p,f)) + i) ) & ( p <> f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . (((Index (p,f)) + i) - 1) ) ) ) )

proof end;

theorem Th24: :: JORDAN3:24

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f holds

( (R_Cut (f,p)) . (len (R_Cut (f,p))) = p & ( for i being Element of NAT st 1 <= i & i <= Index (p,f) holds

(R_Cut (f,p)) . i = f . i ) )

for p being Point of (TOP-REAL 2) st p in L~ f holds

( (R_Cut (f,p)) . (len (R_Cut (f,p))) = p & ( for i being Element of NAT st 1 <= i & i <= Index (p,f) holds

(R_Cut (f,p)) . i = f . i ) )

proof end;

theorem :: JORDAN3:25

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f holds

( ( p <> f . 1 implies len (R_Cut (f,p)) = (Index (p,f)) + 1 ) & ( p = f . 1 implies len (R_Cut (f,p)) = Index (p,f) ) )

for p being Point of (TOP-REAL 2) st p in L~ f holds

( ( p <> f . 1 implies len (R_Cut (f,p)) = (Index (p,f)) + 1 ) & ( p = f . 1 implies len (R_Cut (f,p)) = Index (p,f) ) )

proof end;

theorem Th26: :: JORDAN3:26

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f holds

( ( p = f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = (len f) - (Index (p,f)) ) & ( p <> f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = ((len f) - (Index (p,f))) + 1 ) )

for p being Point of (TOP-REAL 2) st p in L~ f holds

( ( p = f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = (len f) - (Index (p,f)) ) & ( p <> f . ((Index (p,f)) + 1) implies len (L_Cut (f,p)) = ((len f) - (Index (p,f))) + 1 ) )

proof end;

:: deftheorem defines LE JORDAN3:def 5 :

for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds

( LE q1,q2,p1,p2 iff ( q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) & ( for r1, r2 being Real st 0 <= r1 & r1 <= 1 & q1 = ((1 - r1) * p1) + (r1 * p2) & 0 <= r2 & r2 <= 1 & q2 = ((1 - r2) * p1) + (r2 * p2) holds

r1 <= r2 ) ) );

for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds

( LE q1,q2,p1,p2 iff ( q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) & ( for r1, r2 being Real st 0 <= r1 & r1 <= 1 & q1 = ((1 - r1) * p1) + (r1 * p2) & 0 <= r2 & r2 <= 1 & q2 = ((1 - r2) * p1) + (r2 * p2) holds

r1 <= r2 ) ) );

:: deftheorem defines LT JORDAN3:def 6 :

for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds

( LT q1,q2,p1,p2 iff ( LE q1,q2,p1,p2 & q1 <> q2 ) );

for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds

( LT q1,q2,p1,p2 iff ( LE q1,q2,p1,p2 & q1 <> q2 ) );

theorem Th28: :: JORDAN3:28

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) & p1 <> p2 holds

( ( LE q1,q2,p1,p2 or LT q2,q1,p1,p2 ) & ( not LE q1,q2,p1,p2 or not LT q2,q1,p1,p2 ) )

( ( LE q1,q2,p1,p2 or LT q2,q1,p1,p2 ) & ( not LE q1,q2,p1,p2 or not LT q2,q1,p1,p2 ) )

proof end;

theorem Th29: :: JORDAN3:29

for f being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & Index (p,f) < Index (q,f) holds

q in L~ (L_Cut (f,p))

for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & Index (p,f) < Index (q,f) holds

q in L~ (L_Cut (f,p))

proof end;

theorem Th30: :: JORDAN3:30

for p, q, p1, p2 being Point of (TOP-REAL 2) st LE p,q,p1,p2 holds

( q in LSeg (p,p2) & p in LSeg (p1,q) )

( q in LSeg (p,p2) & p in LSeg (p1,q) )

proof end;

theorem Th31: :: JORDAN3:31

for f being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & p <> q & Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) holds

q in L~ (L_Cut (f,p))

for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & p <> q & Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) holds

q in L~ (L_Cut (f,p))

proof end;

::--------------------------------------------------------:

:: Cutting Both Sides of a Finite Sequence and :

:: a Discussion of Speciality of Sequences in TOP-REAL 2 :

::--------------------------------------------------------:

:: Cutting Both Sides of a Finite Sequence and :

:: a Discussion of Speciality of Sequences in TOP-REAL 2 :

::--------------------------------------------------------:

definition

let f be FinSequence of (TOP-REAL 2);

let p, q be Point of (TOP-REAL 2);

coherence

( ( ( ( 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) ) ) implies R_Cut ((L_Cut (f,p)),q) is FinSequence of (TOP-REAL 2) ) & ( ( 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 Rev (R_Cut ((L_Cut (f,q)),p)) is FinSequence of (TOP-REAL 2) ) );

consistency

for b_{1} being FinSequence of (TOP-REAL 2) holds verum;

;

end;
let p, q be Point of (TOP-REAL 2);

func B_Cut (f,p,q) -> FinSequence of (TOP-REAL 2) equals :Def7: :: JORDAN3:def 7

R_Cut ((L_Cut (f,p)),q) if ( ( 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) ) )

otherwise Rev (R_Cut ((L_Cut (f,q)),p));

correctness R_Cut ((L_Cut (f,p)),q) if ( ( 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) ) )

otherwise Rev (R_Cut ((L_Cut (f,q)),p));

coherence

( ( ( ( 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) ) ) implies R_Cut ((L_Cut (f,p)),q) is FinSequence of (TOP-REAL 2) ) & ( ( 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 Rev (R_Cut ((L_Cut (f,q)),p)) is FinSequence of (TOP-REAL 2) ) );

consistency

for b

;

:: deftheorem Def7 defines B_Cut JORDAN3:def 7 :

for f being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) holds

( ( ( ( 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) ) ) implies B_Cut (f,p,q) = R_Cut ((L_Cut (f,p)),q) ) & ( ( 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 B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) ) );

for f being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) holds

( ( ( ( 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) ) ) implies B_Cut (f,p,q) = R_Cut ((L_Cut (f,p)),q) ) & ( ( 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 B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) ) );

theorem Th32: :: JORDAN3:32

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p <> f . 1 holds

R_Cut (f,p) is_S-Seq_joining f /. 1,p

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p <> f . 1 holds

R_Cut (f,p) is_S-Seq_joining f /. 1,p

proof end;

theorem Th33: :: JORDAN3:33

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p <> f . (len f) holds

L_Cut (f,p) is_S-Seq_joining p,f /. (len f)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p <> f . (len f) holds

L_Cut (f,p) is_S-Seq_joining p,f /. (len f)

proof end;

theorem Th34: :: JORDAN3:34

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p <> f . (len f) holds

L_Cut (f,p) is being_S-Seq

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p <> f . (len f) holds

L_Cut (f,p) is being_S-Seq

proof end;

theorem Th35: :: JORDAN3:35

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p <> f . 1 holds

R_Cut (f,p) is being_S-Seq

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p <> f . 1 holds

R_Cut (f,p) is being_S-Seq

proof end;

Lm1: for f being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & q in L~ f & 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) ) ) holds

B_Cut (f,p,q) is_S-Seq_joining p,q

proof end;

theorem Th36: :: JORDAN3:36

for f being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & q in L~ f & p <> q holds

B_Cut (f,p,q) is_S-Seq_joining p,q

for p, q being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & q in L~ f & p <> q holds

B_Cut (f,p,q) is_S-Seq_joining p,q

proof end;

theorem :: JORDAN3:37

for f being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & q in L~ f & p <> q holds

B_Cut (f,p,q) is being_S-Seq

for p, q being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & q in L~ f & p <> q holds

B_Cut (f,p,q) is being_S-Seq

proof end;

theorem Th38: :: JORDAN3:38

for f, g being FinSequence of (TOP-REAL 2) st f . (len f) = g . 1 & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} holds

f ^ (mid (g,2,(len g))) is being_S-Seq

f ^ (mid (g,2,(len g))) is being_S-Seq

proof end;

theorem Th39: :: JORDAN3:39

for f, g being FinSequence of (TOP-REAL 2) st f . (len f) = g . 1 & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} holds

f ^ (mid (g,2,(len g))) is_S-Seq_joining f /. 1,g /. (len g)

f ^ (mid (g,2,(len g))) is_S-Seq_joining f /. 1,g /. (len g)

proof end;

theorem Th41: :: JORDAN3:41

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f holds

L~ (R_Cut (f,p)) c= L~ f

for p being Point of (TOP-REAL 2) st p in L~ f holds

L~ (R_Cut (f,p)) c= L~ f

proof end;

Lm2: for i being Nat

for D being non empty set holds (<*> D) | i = <*> D

proof end;

Lm3: for D being non empty set

for f1 being FinSequence of D

for k being Nat st 1 <= k & k <= len f1 holds

( mid (f1,k,k) = <*(f1 /. k)*> & len (mid (f1,k,k)) = 1 )

proof end;

Lm4: for D being non empty set

for f1 being FinSequence of D holds mid (f1,0,0) = f1 | 1

proof end;

Lm5: for D being non empty set

for f1 being FinSequence of D

for k being Nat st len f1 < k holds

mid (f1,k,k) = <*> D

proof end;

Lm6: for D being non empty set

for f1 being FinSequence of D

for i1, i2 being Nat holds mid (f1,i1,i2) = Rev (mid (f1,i2,i1))

proof end;

Lm7: for h being FinSequence of (TOP-REAL 2)

for i1, i2 being Nat st 1 <= i1 & i1 <= len h & 1 <= i2 & i2 <= len h holds

L~ (mid (h,i1,i2)) c= L~ h

proof end;

Lm8: for i, j being Nat

for D being non empty set

for f being FinSequence of D st i in dom f & j in dom f holds

len (mid (f,i,j)) >= 1

proof end;

Lm9: for i, j being Nat

for D being non empty set

for f being FinSequence of D st i in dom f & j in dom f holds

not mid (f,i,j) is empty

proof end;

Lm10: for i, j being Nat

for D being non empty set

for f being FinSequence of D st i in dom f & j in dom f holds

(mid (f,i,j)) /. 1 = f /. i

proof end;

theorem Th42: :: JORDAN3:42

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

for p being Point of (TOP-REAL 2) st p in L~ f holds

L~ (L_Cut (f,p)) c= L~ f

proof end;

theorem Th43: :: JORDAN3:43

for f, g being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f . (len f) = g . 1 & p in L~ f & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} & p <> f . (len f) holds

(L_Cut (f,p)) ^ (mid (g,2,(len g))) is_S-Seq_joining p,g /. (len g)

for p being Point of (TOP-REAL 2) st f . (len f) = g . 1 & p in L~ f & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} & p <> f . (len f) holds

(L_Cut (f,p)) ^ (mid (g,2,(len g))) is_S-Seq_joining p,g /. (len g)

proof end;

theorem :: JORDAN3:44

for f, g being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f . (len f) = g . 1 & p in L~ f & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} & p <> f . (len f) holds

(L_Cut (f,p)) ^ (mid (g,2,(len g))) is being_S-Seq

for p being Point of (TOP-REAL 2) st f . (len f) = g . 1 & p in L~ f & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} & p <> f . (len f) holds

(L_Cut (f,p)) ^ (mid (g,2,(len g))) is being_S-Seq

proof end;

theorem Th45: :: JORDAN3:45

for f, g being FinSequence of (TOP-REAL 2) st f . (len f) = g . 1 & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} holds

(mid (f,1,((len f) -' 1))) ^ g is being_S-Seq

(mid (f,1,((len f) -' 1))) ^ g is being_S-Seq

proof end;

theorem Th46: :: JORDAN3:46

for f, g being FinSequence of (TOP-REAL 2) st f . (len f) = g . 1 & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} holds

(mid (f,1,((len f) -' 1))) ^ g is_S-Seq_joining f /. 1,g /. (len g)

(mid (f,1,((len f) -' 1))) ^ g is_S-Seq_joining f /. 1,g /. (len g)

proof end;

theorem Th47: :: JORDAN3:47

for f, g being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f . (len f) = g . 1 & p in L~ g & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} & p <> g . 1 holds

(mid (f,1,((len f) -' 1))) ^ (R_Cut (g,p)) is_S-Seq_joining f /. 1,p

for p being Point of (TOP-REAL 2) st f . (len f) = g . 1 & p in L~ g & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} & p <> g . 1 holds

(mid (f,1,((len f) -' 1))) ^ (R_Cut (g,p)) is_S-Seq_joining f /. 1,p

proof end;

theorem :: JORDAN3:48

for f, g being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f . (len f) = g . 1 & p in L~ g & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} & p <> g . 1 holds

(mid (f,1,((len f) -' 1))) ^ (R_Cut (g,p)) is being_S-Seq

for p being Point of (TOP-REAL 2) st f . (len f) = g . 1 & p in L~ g & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} & p <> g . 1 holds

(mid (f,1,((len f) -' 1))) ^ (R_Cut (g,p)) is being_S-Seq

proof end;

:: A Concept of Index for Finite Sequences in TOP-REAL 2 :

::---------------------------------------------------------: