:: Reconstructions of Special Sequences
:: by Yatsuka Nakamura and Roman Matuszewski
::
:: Received December 10, 1996
:: Copyright (c) 1996 Association of Mizar Users

theorem :: JORDAN3:1

canceled;

theorem :: JORDAN3:2

canceled;

theorem :: JORDAN3:3

canceled;

theorem :: JORDAN3:4

canceled;

theorem :: JORDAN3:5

canceled;

theorem :: JORDAN3:6

canceled;

theorem :: JORDAN3:7

canceled;

theorem :: JORDAN3:8

canceled;

theorem :: JORDAN3:9

canceled;

theorem :: JORDAN3:10

canceled;

theorem :: JORDAN3:11

canceled;

theorem :: JORDAN3:12

canceled;

theorem :: JORDAN3:13

canceled;

theorem :: JORDAN3:14

canceled;

theorem Th15: :: JORDAN3:15

for i being Nat
for p, q being FinSequence st len p < i & ( i <= (len p) + (len q) or i <= len (p ^ q) ) holds
(p ^ q) . i = q . (i - (len p))

proof end;

theorem :: JORDAN3:16

canceled;

theorem Th17: :: JORDAN3:17

for D being non empty set
for x being set
for f being FinSequence of D st 1 <= len f holds
( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) )

proof end;

theorem Th18: :: JORDAN3:18

for f being FinSequence st len f = 1 holds
Rev f = f

proof end;

theorem :: JORDAN3:19

for D being non empty set
for f being FinSequence of D
for k being Nat holds len (f /^ k) = (len f) -' k by RFINSEQ:42;

theorem :: JORDAN3:20

canceled;

theorem :: JORDAN3:21

for D being non empty set
for f being FinSequence of D
for l1, l2 being Nat holds (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by FINSEQ_5:83;

definition

let D be non empty set ;
let f be FinSequence of D;
let k1, k2 be Nat;
func mid f,k1,k2 -> FinSequence of D equals :Def1: :: JORDAN3:def 1
(f /^ (k1 -' 1)) | ((k2 -' k1) + 1) if k1 <= k2
otherwise Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1));
correctness
coherence
( ( k1 <= k2 implies (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) is FinSequence of D ) & ( not k1 <= k2 implies Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is FinSequence of D ) );
consistency
for b₁ being FinSequence of D holds verum;
;

end;

:: deftheorem Def1 defines mid JORDAN3:def 1 :

for D being non empty set
for f being FinSequence of D
for k1, k2 being Nat holds
( ( k1 <= k2 implies mid f,k1,k2 = (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) ) & ( not k1 <= k2 implies mid f,k1,k2 = Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) ) );

theorem Th22: :: JORDAN3:22

for D being non empty set
for f being FinSequence of D
for k1, k2 being Element of NAT st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds
Rev (mid f,k1,k2) = mid (Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)

proof end;

theorem Th23: :: JORDAN3:23

for D being non empty set
for n, m being Element of NAT
for f being FinSequence of D st 1 <= m & m + n <= len f holds
(f /^ n) . m = f . (m + n)

proof end;

theorem Th24: :: JORDAN3:24

for D being non empty set
for i being Element of NAT
for f being FinSequence of D st 1 <= i & i <= len f holds
(Rev f) . i = f . (((len f) - i) + 1)

proof end;

theorem :: JORDAN3:25

for D being non empty set
for f being FinSequence of D
for k being Nat st 1 <= k holds
mid f,1,k = f | k

proof end;

theorem Th26: :: JORDAN3:26

for D being non empty set
for f being FinSequence of D
for k being Element of NAT st k <= len f holds
mid f,k,(len f) = f /^ (k -' 1)

proof end;

theorem Th27: :: JORDAN3:27

for D being non empty set
for f being FinSequence of D
for k1, k2 being Element of NAT st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds
( (mid f,k1,k2) . 1 = f . k1 & ( k1 <= k2 implies ( len (mid f,k1,k2) = (k2 -' k1) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid f,k1,k2) holds
(mid f,k1,k2) . i = f . ((i + k1) -' 1) ) ) ) & ( k1 > k2 implies ( len (mid f,k1,k2) = (k1 -' k2) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid f,k1,k2) holds
(mid f,k1,k2) . i = f . ((k1 -' i) + 1) ) ) ) )

proof end;

theorem Th28: :: JORDAN3:28

for D being non empty set
for f being FinSequence of D
for k1, k2 being Element of NAT holds rng (mid f,k1,k2) c= rng f

proof end;

theorem :: JORDAN3:29

for D being non empty set
for f being FinSequence of D st 1 <= len f holds
mid f,1,(len f) = f

proof end;

theorem :: JORDAN3:30

for D being non empty set
for f being FinSequence of D st 1 <= len f holds
mid f,(len f),1 = Rev f

proof end;

theorem Th31: :: JORDAN3:31

for D being non empty set
for f being FinSequence of D
for k1, k2, i being Element of NAT st 1 <= k1 & k1 <= k2 & k2 <= len f & 1 <= i & ( i <= (k2 -' k1) + 1 or i <= (k2 - k1) + 1 or i <= (k2 + 1) - k1 ) holds
( (mid f,k1,k2) . i = f . ((i + k1) -' 1) & (mid f,k1,k2) . i = f . ((i -' 1) + k1) & (mid f,k1,k2) . i = f . ((i + k1) - 1) & (mid f,k1,k2) . i = f . ((i - 1) + k1) )

proof end;

theorem Th32: :: JORDAN3:32

for D being non empty set
for f being FinSequence of D
for k, i being Nat st 1 <= i & i <= k & k <= len f holds
(mid f,1,k) . i = f . i

proof end;

theorem :: JORDAN3:33

for D being non empty set
for f being FinSequence of D
for k1, k2 being Element of NAT st 1 <= k1 & k1 <= k2 & k2 <= len f holds
len (mid f,k1,k2) <= len f

proof end;

theorem :: JORDAN3:34

for n being Element of 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 )

proof end;

theorem Th35: :: JORDAN3:35

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

proof end;

theorem Th36: :: JORDAN3:36

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

proof end;

theorem Th37: :: JORDAN3:37

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

proof end;

theorem Th38: :: JORDAN3:38

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

proof end;

theorem :: JORDAN3:39

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

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 ;
func Index p,f -> Element of NAT means :Def2: :: JORDAN3:def 2
ex S being non empty Subset of NAT st
( it = min S & S = { i where i is Element of NAT : p in LSeg f,i } );
existence
ex b₁ being Element of NAT ex S being non empty Subset of NAT st
( b₁ = min S & S = { i where i is Element of NAT : p in LSeg f,i } )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ex S being non empty Subset of NAT st
( b₁ = min S & S = { i where i is Element of NAT : p in LSeg f,i } ) & ex S being non empty Subset of NAT st
( b₂ = min S & S = { i where i is Element of NAT : p in LSeg f,i } ) holds
b₁ = b₂ ;

end;

:: deftheorem Def2 defines Index JORDAN3:def 2 :

for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
for b₃ being Element of NAT holds
( b₃ = Index p,f iff ex S being non empty Subset of NAT st
( b₃ = min S & S = { i where i is Element of NAT : p in LSeg f,i } ) );

theorem Th40: :: JORDAN3:40

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

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
( 1 <= Index p,f & Index p,f < len f )

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
p in LSeg f,(Index p,f)

proof end;

theorem Th43: :: JORDAN3:43

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

proof end;

theorem Th44: :: JORDAN3:44

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

proof end;

theorem Th45: :: JORDAN3:45

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

proof end;

theorem Th46: :: JORDAN3:46

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

proof end;

theorem Th47: :: JORDAN3:47

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

proof end;

definition

let g be FinSequence of (TOP-REAL 2);
let p1, p2 be Point of (TOP-REAL 2);
pred g is_S-Seq_joining p1,p2 means :Def3: :: JORDAN3:def 3
( g is being_S-Seq & g . 1 = p1 & g . (len g) = p2 );

end;

:: deftheorem Def3 defines is_S-Seq_joining JORDAN3:def 3 :

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 Th48: :: JORDAN3:48

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

proof end;

theorem Th49: :: JORDAN3:49

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)

proof end;

theorem :: JORDAN3:50

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)

proof end;

theorem Th51: :: JORDAN3:51

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

proof end;

theorem Th52: :: JORDAN3:52

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

proof end;

definition

let f be FinSequence of (TOP-REAL 2);
let p be Point of (TOP-REAL 2);
func L_Cut f,p -> FinSequence of (TOP-REAL 2) equals :Def4: :: JORDAN3:def 4
<*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
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₁ being FinSequence of (TOP-REAL 2) holds verum;
;
func R_Cut f,p -> FinSequence of (TOP-REAL 2) equals :Def5: :: JORDAN3:def 5
(mid f,1,(Index p,f)) ^ <*p*> if p <> f . 1
otherwise <*p*>;
correctness
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₁ being FinSequence of (TOP-REAL 2) holds verum;
;

end;

:: deftheorem Def4 defines L_Cut JORDAN3:def 4 :

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 Def5 defines R_Cut JORDAN3:def 5 :

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 Th53: :: JORDAN3:53

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

proof end;

theorem Th54: :: JORDAN3:54

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

proof end;

theorem Th55: :: JORDAN3:55

for D being non empty set
for f being FinSequence of D
for k being Element of NAT
for p being Element of D holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k)

proof end;

theorem Th56: :: JORDAN3:56

for D being non empty set
for f being FinSequence of D
for k1, k2 being Element of NAT st k1 < k2 & k1 in dom f holds
mid f,k1,k2 = <*(f . k1)*> ^ (mid f,(k1 + 1),k2)

proof end;

theorem Th57: :: JORDAN3:57

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)

proof end;

theorem Th58: :: JORDAN3:58

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 Element of 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 Th59: :: JORDAN3:59

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 ) )

proof end;

theorem :: JORDAN3:60

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 ) )

proof end;

theorem Th61: :: JORDAN3:61

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 ) )

proof end;

definition

let p1, p2, q1, q2 be Point of (TOP-REAL 2);
pred LE q1,q2,p1,p2 means :Def6: :: JORDAN3:def 6
( 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 ) );

end;

:: deftheorem Def6 defines LE JORDAN3:def 6 :

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

definition

let p1, p2, q1, q2 be Point of (TOP-REAL 2);
pred LT q1,q2,p1,p2 means :Def7: :: JORDAN3:def 7
( LE q1,q2,p1,p2 & q1 <> q2 );

end;

:: deftheorem Def7 defines LT JORDAN3:def 7 :

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 :: JORDAN3:62

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

proof end;

theorem Th63: :: JORDAN3:63

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 ) )

proof end;

theorem Th64: :: JORDAN3:64

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)

proof end;

theorem Th65: :: JORDAN3:65

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 )

proof end;

theorem Th66: :: JORDAN3:66

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)

proof end;

definition

let f be FinSequence of (TOP-REAL 2);
let p, q be Point of (TOP-REAL 2);
func B_Cut f,p,q -> FinSequence of (TOP-REAL 2) equals :Def8: :: JORDAN3:def 8
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
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₁ being FinSequence of (TOP-REAL 2) holds verum;
;

end;

:: deftheorem Def8 defines B_Cut JORDAN3:def 8 :

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 Th67: :: JORDAN3:67

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

proof end;

theorem Th68: :: JORDAN3:68

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)

proof end;

theorem Th69: :: JORDAN3:69

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

proof end;

theorem Th70: :: JORDAN3:70

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

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 Th71: :: JORDAN3:71

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

proof end;

theorem :: JORDAN3:72

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

proof end;

theorem Th73: :: JORDAN3:73

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

proof end;

theorem Th74: :: JORDAN3:74

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)

proof end;

theorem :: JORDAN3:75

for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT holds L~ (f /^ n) c= L~ f

proof end;

theorem Th76: :: JORDAN3:76

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

proof end;

Lm2: for k being Nat
for i, j being Element of NAT st i <= j holds
(j + k) -' i = (j + k) - i
by NAT_1:12, XREAL_1:235;

Lm3: for i being Element of NAT
for D being non empty set holds (<*> D) | i = <*> D

proof end;

Lm5: for D being non empty set
for f1 being FinSequence of D
for k being Element of NAT st 1 <= k & k <= len f1 holds
( mid f1,k,k = <*(f1 /. k)*> & len (mid f1,k,k) = 1 )

proof end;

Lm6: for D being non empty set
for f1 being FinSequence of D holds mid f1,0 ,0 = f1 | 1

proof end;

Lm7: for D being non empty set
for f1 being FinSequence of D
for k being Element of NAT st len f1 < k holds
mid f1,k,k = <*> D

proof end;

Lm8: for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Element of NAT holds mid f1,i1,i2 = Rev (mid f1,i2,i1)

proof end;

Lm9: for h being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st 1 <= i1 & i1 <= len h & 1 <= i2 & i2 <= len h holds
L~ (mid h,i1,i2) c= L~ h

proof end;

Lm10: for i, j being Element of 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;

Lm11: for i, j being Element of 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;

Lm12: for i, j being Element of 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 Th77: :: JORDAN3:77

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

theorem Th78: :: JORDAN3:78

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)

proof end;

theorem :: JORDAN3:79

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

proof end;

theorem Th80: :: JORDAN3:80

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

proof end;

theorem Th81: :: JORDAN3:81

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)

proof end;

theorem Th82: :: JORDAN3:82

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

proof end;

theorem :: JORDAN3:83

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

proof end;