for D being non empty set
for f1 being FinSequence of D
for k being Nat st k < len f1 holds
( (f1 /^ k) . (len (f1 /^ k)) = f1 . (len f1) & (f1 /^ k) /. (len (f1 /^ k)) = f1 /. (len f1) )

proof end;

theorem Th19: :: JORDAN4:19

for g being FinSequence of (TOP-REAL 2)
for i being Nat st g is_S-Seq & i + 1 < len g holds
g /^ i is_S-Seq

proof end;

theorem Th20: :: JORDAN4:20

for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Nat st 1 <= i2 & i2 <= i1 & i1 <= len f1 holds
len (mid f1,i2,i1) = (i1 -' i2) + 1

proof end;

theorem Th21: :: JORDAN4:21

for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Nat st 1 <= i2 & i2 <= i1 & i1 <= len f1 holds
len (mid f1,i1,i2) = (i1 -' i2) + 1

proof end;

theorem Th22: :: JORDAN4:22

for D being non empty set
for f1 being FinSequence of D
for i1, i2, j being Nat st 1 <= i1 & i1 <= i2 & i2 <= len f1 holds
(mid f1,i1,i2) . (len (mid f1,i1,i2)) = f1 . i2

proof end;

theorem Th23: :: JORDAN4:23

for D being non empty set
for f1 being FinSequence of D
for i1, i2, j being Nat st 1 <= i1 & i1 <= len f1 & 1 <= i2 & i2 <= len f1 holds
(mid f1,i1,i2) . (len (mid f1,i1,i2)) = f1 . i2

proof end;

theorem Th24: :: JORDAN4:24

for D being non empty set
for f1 being FinSequence of D
for i1, i2, j being Nat st 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 holds
(mid f1,i1,i2) . j = f1 . ((i1 -' j) + 1)

proof end;

theorem Th25: :: JORDAN4:25

for j being Nat
for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Nat st 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 holds
( (mid f1,i1,i2) . j = (mid f1,i2,i1) . ((((i1 - i2) + 1) - j) + 1) & (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 )

proof end;

theorem :: JORDAN4:26

for j being Nat
for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 <= len f1 & 1 <= j & j <= (i2 -' i1) + 1 holds
( (mid f1,i1,i2) . j = (mid f1,i2,i1) . ((((i2 - i1) + 1) - j) + 1) & (((i2 - i1) + 1) - j) + 1 = (((i2 -' i1) + 1) -' j) + 1 )

proof end;

theorem Th27: :: JORDAN4:27

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;

theorem Th28: :: JORDAN4:28

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

proof end;

theorem Th29: :: JORDAN4:29

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;

theorem Th30: :: JORDAN4:30

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;

theorem Th31: :: JORDAN4:31

for f being FinSequence of (TOP-REAL 2)
for i1, i2, i being Nat st 1 <= i1 & i1 < i2 & i2 <= len f & 1 <= i & i < (i2 -' i1) + 1 holds
LSeg (mid f,i1,i2),i = LSeg f,((i + i1) -' 1)

proof end;

theorem Th32: :: JORDAN4:32

for f being FinSequence of (TOP-REAL 2)
for i1, i2, i being Nat st 1 <= i1 & i1 < i2 & i2 <= len f & 1 <= i & i < (i2 -' i1) + 1 holds
LSeg (mid f,i2,i1),i = LSeg f,(i2 -' i)

proof end;

definition

let n be Nat;
let f be FinSequence;
func S_Drop n,f -> Nat equals :Def1: :: JORDAN4:def 1
n mod ((len f) -' 1) if n mod ((len f) -' 1) <> 0
otherwise (len f) -' 1;
correctness ;

end;

:: deftheorem Def1 defines S_Drop JORDAN4:def 1 :

theorem Th33: :: JORDAN4:33

for f being FinSequence holds S_Drop ((len f) -' 1),f = (len f) -' 1

proof end;

theorem Th34: :: JORDAN4:34

for n being Nat
for f being FinSequence st 1 <= n & n <= (len f) -' 1 holds
S_Drop n,f = n

proof end;

theorem Th35: :: JORDAN4:35

for n being Nat
for f being FinSequence holds
( S_Drop n,f = S_Drop (n + ((len f) -' 1)),f & S_Drop n,f = S_Drop (((len f) -' 1) + n),f )

proof end;

definition

let f be non constant standard special_circular_sequence;
let g be FinSequence of (TOP-REAL 2);
let i1, i2 be Nat;
pred g is_a_part>_of f,i1,i2 means :Def2: :: JORDAN4:def 2
( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & g . (len g) = f . i2 & 1 <= len g & len g < len f & ( for i being Nat st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((i1 + i) -' 1),f) ) );

end;

:: deftheorem Def2 defines is_a_part>_of JORDAN4:def 2 :

definition

let f be non constant standard special_circular_sequence;
let g be FinSequence of (TOP-REAL 2);
let i1, i2 be Nat;
pred g is_a_part<_of f,i1,i2 means :Def3: :: JORDAN4:def 3
( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & g . (len g) = f . i2 & 1 <= len g & len g < len f & ( for i being Nat st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((len f) + i1) -' i),f) ) );

end;

:: deftheorem Def3 defines is_a_part<_of JORDAN4:def 3 :

definition

let f be non constant standard special_circular_sequence;
let g be FinSequence of (TOP-REAL 2);
let i1, i2 be Nat;
pred g is_a_part_of f,i1,i2 means :Def4: :: JORDAN4:def 4
( g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2 );

end;

:: deftheorem Def4 defines is_a_part_of JORDAN4:def 4 :

theorem :: JORDAN4:36

for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part_of f,i1,i2 holds
( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & g . (len g) = f . i2 & 1 <= len g & len g < len f & ( for i being Nat st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((i1 + i) -' 1),f) or for i being Nat st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((len f) + i1) -' i),f) ) )

proof end;

theorem Th37: :: JORDAN4:37

for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 <= i2 holds
( len g = (i2 -' i1) + 1 & g = mid f,i1,i2 )

proof end;

theorem Th38: :: JORDAN4:38

for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 > i2 holds
( len g = ((len f) + i2) -' i1 & g = (mid f,i1,((len f) -' 1)) ^ (f | i2) & g = (mid f,i1,((len f) -' 1)) ^ (mid f,1,i2) )

proof end;

theorem Th39: :: JORDAN4:39

for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part<_of f,i1,i2 & i1 >= i2 holds
( len g = (i1 -' i2) + 1 & g = mid f,i1,i2 )

proof end;

theorem Th40: :: JORDAN4:40

for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part<_of f,i1,i2 & i1 < i2 holds
( len g = ((len f) + i1) -' i2 & g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) )

proof end;

theorem Th41: :: JORDAN4:41

for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 holds
Rev g is_a_part<_of f,i2,i1

proof end;

theorem Th42: :: JORDAN4:42

for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part<_of f,i1,i2 holds
Rev g is_a_part>_of f,i2,i1

proof end;

theorem Th43: :: JORDAN4:43

for f being non constant standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 < len f holds
mid f,i1,i2 is_a_part>_of f,i1,i2

proof end;

theorem Th44: :: JORDAN4:44

for f being non constant standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 < len f holds
mid f,i2,i1 is_a_part<_of f,i2,i1

proof end;

theorem Th45: :: JORDAN4:45

for f being non constant standard special_circular_sequence
for i1, i2 being Nat st 1 <= i2 & i1 > i2 & i1 < len f holds
(mid f,i1,((len f) -' 1)) ^ (mid f,1,i2) is_a_part>_of f,i1,i2

proof end;

theorem Th46: :: JORDAN4:46

for f being non constant standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 < i2 & i2 < len f holds
(mid f,i1,1) ^ (mid f,((len f) -' 1),i2) is_a_part<_of f,i1,i2

proof end;

theorem Th47: :: JORDAN4:47

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;

theorem Th48: :: JORDAN4:48

for D being non empty set
for g being FinSequence of D holds
( g is one-to-one iff for i1, i2 being Nat st 1 <= i1 & i1 <= len g & 1 <= i2 & i2 <= len g & ( g . i1 = g . i2 or g /. i1 = g /. i2 ) holds
i1 = i2 )

proof end;

theorem Th49: :: JORDAN4:49

for f being non constant standard special_circular_sequence
for i2 being Nat st 1 < i2 & i2 + 1 <= len f holds
f | i2 is_S-Seq

proof end;

theorem Th50: :: JORDAN4:50

for f being non constant standard special_circular_sequence
for i2 being Nat st 1 <= i2 & i2 + 1 < len f holds
f /^ i2 is_S-Seq

proof end;

theorem Th51: :: JORDAN4:51

for f being non constant standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 < i2 & i2 + 1 <= len f holds
mid f,i1,i2 is_S-Seq

proof end;

theorem Th52: :: JORDAN4:52

for f being non constant standard special_circular_sequence
for i1, i2 being Nat st 1 < i1 & i1 < i2 & i2 <= len f holds
mid f,i1,i2 is_S-Seq

proof end;

theorem Th53: :: JORDAN4:53

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

proof end;

theorem Th54: :: JORDAN4:54

for f being non constant standard special_circular_sequence holds (LSeg f,1) /\ (LSeg f,((len f) -' 1)) = {(f . 1)}

proof end;

theorem Th55: :: JORDAN4:55

for f being non constant standard special_circular_sequence
for i1, i2 being Nat
for g1, g2 being FinSequence of (TOP-REAL 2) st 1 <= i1 & i1 < i2 & i2 < len f & g1 = mid f,i1,i2 & g2 = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) holds
( (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f )

proof end;

theorem Th56: :: JORDAN4:56

for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 < i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2

proof end;

Lm1: for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 > i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2

proof end;

theorem :: JORDAN4:57

for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part<_of f,i1,i2 & i1 > i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2

proof end;

theorem Th58: :: JORDAN4:58

for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 <> i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2

proof end;

theorem Th59: :: JORDAN4:59

for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part<_of f,i1,i2 & i1 <> i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2

proof end;

theorem Th60: :: JORDAN4:60

for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part_of f,i1,i2 & i1 <> i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2

proof end;

theorem :: JORDAN4:61

for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part_of f,i1,i2 & g . 1 <> g . (len g) holds
L~ g is_S-P_arc_joining f /. i1,f /. i2

proof end;

theorem Th62: :: JORDAN4:62

for f being non constant standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & i1 <> i2 holds
ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) )

proof end;

theorem :: JORDAN4:63

for f being non constant standard special_circular_sequence
for P being non empty Subset of (TOP-REAL 2) st P = L~ f holds
P is_simple_closed_curve

proof end;

theorem Th64: :: JORDAN4:64

for i1, i2 being Nat
for f being non constant standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st g1 is_a_part>_of f,i1,i2 & g2 is_a_part>_of f,i1,i2 holds
g1 = g2

proof end;

theorem Th65: :: JORDAN4:65

for i1, i2 being Nat
for f being non constant standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st g1 is_a_part<_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 holds
g1 = g2

proof end;

theorem Th66: :: JORDAN4:66

for i1, i2 being Nat
for f being non constant standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st i1 <> i2 & g1 is_a_part>_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 holds
g1 . 2 <> g2 . 2

proof end;

theorem Th67: :: JORDAN4:67

for i1, i2 being Nat
for f being non constant standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st i1 <> i2 & g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & g1 . 2 = g2 . 2 holds
g1 = g2

proof end;

definition

let f be non constant standard special_circular_sequence;
let i1, i2 be Nat;
assume A1: ( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & i1 <> i2 ) ;
func Lower f,i1,i2 -> FinSequence of (TOP-REAL 2) means :: JORDAN4:def 5
( it is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies it . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 & (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies it . 2 = f . (S_Drop (i1 -' 1),f) ) );
correctness

proof end;

func Upper f,i1,i2 -> FinSequence of (TOP-REAL 2) means :: JORDAN4:def 6
( it is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies it . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies it . 2 = f . (S_Drop (i1 -' 1),f) ) );
correctness

proof end;

end;

:: deftheorem defines Lower JORDAN4:def 5 :

:: deftheorem defines Upper JORDAN4:def 6 :