:: Bounding Boxes for Special Sequences in ${\calE}^2$
:: by Yatsuka Nakamura and Adam Grabowski
::
:: Received June 8, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users


theorem Th1: :: JORDAN5D:1
for n being Nat
for h being FinSequence of (TOP-REAL n) st len h >= 2 holds
h /. (len h) in LSeg (h,((len h) -' 1))
proof end;

theorem Th2: :: JORDAN5D:2
for i being Nat st 3 <= i holds
i mod (i -' 1) = 1
proof end;

theorem Th3: :: JORDAN5D:3
for p being Point of (TOP-REAL 2)
for h being non constant standard special_circular_sequence st p in rng h holds
ex i being Nat st
( 1 <= i & i + 1 <= len h & h . i = p )
proof end;

theorem Th4: :: JORDAN5D:4
for r being Real
for g being FinSequence of REAL st r in rng g holds
( (Incr g) . 1 <= r & r <= (Incr g) . (len (Incr g)) )
proof end;

theorem Th5: :: JORDAN5D:5
for h being non constant standard special_circular_sequence
for I, i being Nat st 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) holds
( ((GoB h) * (1,I)) `1 <= (h /. i) `1 & (h /. i) `1 <= ((GoB h) * ((len (GoB h)),I)) `1 )
proof end;

theorem Th6: :: JORDAN5D:6
for h being non constant standard special_circular_sequence
for I, i being Nat st 1 <= i & i <= len h & 1 <= I & I <= len (GoB h) holds
( ((GoB h) * (I,1)) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * (I,(width (GoB h)))) `2 )
proof end;

theorem Th7: :: JORDAN5D:7
for f being non empty FinSequence of (TOP-REAL 2)
for i being Nat st 1 <= i & i <= len (GoB f) holds
ex k, j being Nat st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
proof end;

theorem Th8: :: JORDAN5D:8
for f being non empty FinSequence of (TOP-REAL 2)
for j being Nat st 1 <= j & j <= width (GoB f) holds
ex k, i being Nat st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )
proof end;

theorem Th9: :: JORDAN5D:9
for f being non empty FinSequence of (TOP-REAL 2)
for i, j being Nat st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds
ex k being Nat st
( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `1 = ((GoB f) * (i,j)) `1 )
proof end;

theorem Th10: :: JORDAN5D:10
for f being non empty FinSequence of (TOP-REAL 2)
for i, j being Nat st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds
ex k being Nat st
( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 )
proof end;

theorem Th11: :: JORDAN5D:11
for h being non constant standard special_circular_sequence
for i being Nat st 1 <= i & i <= len h holds
( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) )
proof end;

theorem Th12: :: JORDAN5D:12
for h being non constant standard special_circular_sequence
for i being Nat st 1 <= i & i <= len h holds
( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) )
proof end;

theorem Th13: :: JORDAN5D:13
for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } holds
X = (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h)))
proof end;

theorem Th14: :: JORDAN5D:14
for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ h) & q in L~ h ) } holds
X = (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h)))
proof end;

theorem Th15: :: JORDAN5D:15
for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } holds
X = (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h)))
proof end;

theorem Th16: :: JORDAN5D:16
for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ h) & q in L~ h ) } holds
X = (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h)))
proof end;

theorem Th17: :: JORDAN5D:17
for g being FinSequence of (TOP-REAL 2)
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } holds
X = (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))
proof end;

theorem Th18: :: JORDAN5D:18
for g being FinSequence of (TOP-REAL 2)
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } holds
X = (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))
proof end;

theorem :: JORDAN5D:19
for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } holds
lower_bound X = lower_bound (proj2 | (W-most (L~ h))) by Th13;

theorem :: JORDAN5D:20
for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } holds
upper_bound X = upper_bound (proj2 | (W-most (L~ h))) by Th13;

theorem :: JORDAN5D:21
for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ h) & q in L~ h ) } holds
lower_bound X = lower_bound (proj2 | (E-most (L~ h))) by Th14;

theorem :: JORDAN5D:22
for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ h) & q in L~ h ) } holds
upper_bound X = upper_bound (proj2 | (E-most (L~ h))) by Th14;

theorem :: JORDAN5D:23
for g being FinSequence of (TOP-REAL 2)
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } holds
lower_bound X = lower_bound (proj1 | (L~ g)) by Th17;

theorem :: JORDAN5D:24
for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ h) & q in L~ h ) } holds
lower_bound X = lower_bound (proj1 | (S-most (L~ h))) by Th16;

theorem :: JORDAN5D:25
for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ h) & q in L~ h ) } holds
upper_bound X = upper_bound (proj1 | (S-most (L~ h))) by Th16;

theorem :: JORDAN5D:26
for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } holds
lower_bound X = lower_bound (proj1 | (N-most (L~ h))) by Th15;

theorem :: JORDAN5D:27
for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } holds
upper_bound X = upper_bound (proj1 | (N-most (L~ h))) by Th15;

theorem :: JORDAN5D:28
for g being FinSequence of (TOP-REAL 2)
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } holds
lower_bound X = lower_bound (proj2 | (L~ g)) by Th18;

theorem :: JORDAN5D:29
for g being FinSequence of (TOP-REAL 2)
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } holds
upper_bound X = upper_bound (proj1 | (L~ g)) by Th17;

theorem :: JORDAN5D:30
for g being FinSequence of (TOP-REAL 2)
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } holds
upper_bound X = upper_bound (proj2 | (L~ g)) by Th18;

theorem Th31: :: JORDAN5D:31
for p being Point of (TOP-REAL 2)
for h being non constant standard special_circular_sequence
for I being Nat st p in L~ h & 1 <= I & I <= width (GoB h) holds
((GoB h) * (1,I)) `1 <= p `1
proof end;

theorem Th32: :: JORDAN5D:32
for p being Point of (TOP-REAL 2)
for h being non constant standard special_circular_sequence
for I being Nat st p in L~ h & 1 <= I & I <= width (GoB h) holds
p `1 <= ((GoB h) * ((len (GoB h)),I)) `1
proof end;

theorem Th33: :: JORDAN5D:33
for p being Point of (TOP-REAL 2)
for h being non constant standard special_circular_sequence
for I being Nat st p in L~ h & 1 <= I & I <= len (GoB h) holds
((GoB h) * (I,1)) `2 <= p `2
proof end;

theorem Th34: :: JORDAN5D:34
for p being Point of (TOP-REAL 2)
for h being non constant standard special_circular_sequence
for I being Nat st p in L~ h & 1 <= I & I <= len (GoB h) holds
p `2 <= ((GoB h) * (I,(width (GoB h)))) `2
proof end;

theorem Th35: :: JORDAN5D:35
for h being non constant standard special_circular_sequence
for i, j being Nat st 1 <= i & i <= len (GoB h) & 1 <= j & j <= width (GoB h) holds
ex q being Point of (TOP-REAL 2) st
( q `1 = ((GoB h) * (i,j)) `1 & q in L~ h )
proof end;

theorem Th36: :: JORDAN5D:36
for h being non constant standard special_circular_sequence
for i, j being Nat st 1 <= i & i <= len (GoB h) & 1 <= j & j <= width (GoB h) holds
ex q being Point of (TOP-REAL 2) st
( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h )
proof end;

theorem Th37: :: JORDAN5D:37
for h being non constant standard special_circular_sequence holds W-bound (L~ h) = ((GoB h) * (1,1)) `1
proof end;

theorem Th38: :: JORDAN5D:38
for h being non constant standard special_circular_sequence holds S-bound (L~ h) = ((GoB h) * (1,1)) `2
proof end;

theorem Th39: :: JORDAN5D:39
for h being non constant standard special_circular_sequence holds E-bound (L~ h) = ((GoB h) * ((len (GoB h)),1)) `1
proof end;

theorem Th40: :: JORDAN5D:40
for h being non constant standard special_circular_sequence holds N-bound (L~ h) = ((GoB h) * (1,(width (GoB h)))) `2
proof end;

theorem Th41: :: JORDAN5D:41
for f being non empty FinSequence of (TOP-REAL 2)
for I, i1, i being Nat
for Y being non empty finite Subset of NAT st 1 <= i & i <= len f & 1 <= I & I <= len (GoB f) & Y = { j where j is Element of NAT : ( [I,j] in Indices (GoB f) & ex k being Nat st
( k in dom f & f /. k = (GoB f) * (I,j) ) ) } & (f /. i) `1 = ((GoB f) * (I,1)) `1 & i1 = min Y holds
((GoB f) * (I,i1)) `2 <= (f /. i) `2
proof end;

theorem Th42: :: JORDAN5D:42
for h being non constant standard special_circular_sequence
for I, i1, i being Nat
for Y being non empty finite Subset of NAT st 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) & Y = { j where j is Element of NAT : ( [j,I] in Indices (GoB h) & ex k being Nat st
( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = min Y holds
((GoB h) * (i1,I)) `1 <= (h /. i) `1
proof end;

theorem Th43: :: JORDAN5D:43
for h being non constant standard special_circular_sequence
for I, i1, i being Nat
for Y being non empty finite Subset of NAT st 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) & Y = { j where j is Element of NAT : ( [j,I] in Indices (GoB h) & ex k being Nat st
( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = max Y holds
((GoB h) * (i1,I)) `1 >= (h /. i) `1
proof end;

theorem Th44: :: JORDAN5D:44
for f being non empty FinSequence of (TOP-REAL 2)
for I, i1, i being Nat
for Y being non empty finite Subset of NAT st 1 <= i & i <= len f & 1 <= I & I <= len (GoB f) & Y = { j where j is Element of NAT : ( [I,j] in Indices (GoB f) & ex k being Nat st
( k in dom f & f /. k = (GoB f) * (I,j) ) ) } & (f /. i) `1 = ((GoB f) * (I,1)) `1 & i1 = max Y holds
((GoB f) * (I,i1)) `2 >= (f /. i) `2
proof end;

Lm1: for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `1 = W-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [1,j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = min Y holds
((GoB h) * (1,i1)) `2 <= p `2
proof end;

Lm2: for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `1 = W-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [1,j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = max Y holds
((GoB h) * (1,i1)) `2 >= p `2
proof end;

Lm3: for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `1 = E-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = min Y holds
((GoB h) * ((len (GoB h)),i1)) `2 <= p `2
proof end;

Lm4: for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `1 = E-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = max Y holds
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
proof end;

Lm5: for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `2 = S-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,1] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = min Y holds
((GoB h) * (i1,1)) `1 <= p `1
proof end;

Lm6: for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = min Y holds
((GoB h) * (i1,(width (GoB h)))) `1 <= p `1
proof end;

Lm7: for h being non constant standard special_circular_sequence
for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT st p `2 = S-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,1] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = max Y holds
((GoB h) * (i1,1)) `1 >= p `1
proof end;

Lm8: for h being non constant standard special_circular_sequence
for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT st p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y holds
((GoB h) * (i1,(width (GoB h)))) `1 >= p `1
proof end;

Lm9: for h being non constant standard special_circular_sequence holds len h >= 2
by GOBOARD7:34, XXREAL_0:2;

definition
let g be non constant standard special_circular_sequence;
func i_s_w g -> Nat means :Def1: :: JORDAN5D:def 1
( [1,it] in Indices (GoB g) & (GoB g) * (1,it) = W-min (L~ g) );
existence
ex b1 being Nat st
( [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-min (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-min (L~ g) & [1,b2] in Indices (GoB g) & (GoB g) * (1,b2) = W-min (L~ g) holds
b1 = b2 by GOBOARD1:5;
func i_n_w g -> Nat means :Def2: :: JORDAN5D:def 2
( [1,it] in Indices (GoB g) & (GoB g) * (1,it) = W-max (L~ g) );
existence
ex b1 being Nat st
( [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-max (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-max (L~ g) & [1,b2] in Indices (GoB g) & (GoB g) * (1,b2) = W-max (L~ g) holds
b1 = b2 by GOBOARD1:5;
func i_s_e g -> Nat means :Def3: :: JORDAN5D:def 3
( [(len (GoB g)),it] in Indices (GoB g) & (GoB g) * ((len (GoB g)),it) = E-min (L~ g) );
existence
ex b1 being Nat st
( [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-min (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-min (L~ g) & [(len (GoB g)),b2] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b2) = E-min (L~ g) holds
b1 = b2 by GOBOARD1:5;
func i_n_e g -> Nat means :Def4: :: JORDAN5D:def 4
( [(len (GoB g)),it] in Indices (GoB g) & (GoB g) * ((len (GoB g)),it) = E-max (L~ g) );
existence
ex b1 being Nat st
( [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-max (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-max (L~ g) & [(len (GoB g)),b2] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b2) = E-max (L~ g) holds
b1 = b2 by GOBOARD1:5;
func i_w_s g -> Nat means :Def5: :: JORDAN5D:def 5
( [it,1] in Indices (GoB g) & (GoB g) * (it,1) = S-min (L~ g) );
existence
ex b1 being Nat st
( [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-min (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-min (L~ g) & [b2,1] in Indices (GoB g) & (GoB g) * (b2,1) = S-min (L~ g) holds
b1 = b2 by GOBOARD1:5;
func i_e_s g -> Nat means :Def6: :: JORDAN5D:def 6
( [it,1] in Indices (GoB g) & (GoB g) * (it,1) = S-max (L~ g) );
existence
ex b1 being Nat st
( [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-max (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-max (L~ g) & [b2,1] in Indices (GoB g) & (GoB g) * (b2,1) = S-max (L~ g) holds
b1 = b2 by GOBOARD1:5;
func i_w_n g -> Nat means :Def7: :: JORDAN5D:def 7
( [it,(width (GoB g))] in Indices (GoB g) & (GoB g) * (it,(width (GoB g))) = N-min (L~ g) );
existence
ex b1 being Nat st
( [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-min (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-min (L~ g) & [b2,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b2,(width (GoB g))) = N-min (L~ g) holds
b1 = b2 by GOBOARD1:5;
func i_e_n g -> Nat means :Def8: :: JORDAN5D:def 8
( [it,(width (GoB g))] in Indices (GoB g) & (GoB g) * (it,(width (GoB g))) = N-max (L~ g) );
existence
ex b1 being Nat st
( [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-max (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-max (L~ g) & [b2,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b2,(width (GoB g))) = N-max (L~ g) holds
b1 = b2 by GOBOARD1:5;
end;

:: deftheorem Def1 defines i_s_w JORDAN5D:def 1 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_s_w g iff ( [1,b2] in Indices (GoB g) & (GoB g) * (1,b2) = W-min (L~ g) ) );

:: deftheorem Def2 defines i_n_w JORDAN5D:def 2 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_n_w g iff ( [1,b2] in Indices (GoB g) & (GoB g) * (1,b2) = W-max (L~ g) ) );

:: deftheorem Def3 defines i_s_e JORDAN5D:def 3 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_s_e g iff ( [(len (GoB g)),b2] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b2) = E-min (L~ g) ) );

:: deftheorem Def4 defines i_n_e JORDAN5D:def 4 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_n_e g iff ( [(len (GoB g)),b2] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b2) = E-max (L~ g) ) );

:: deftheorem Def5 defines i_w_s JORDAN5D:def 5 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_w_s g iff ( [b2,1] in Indices (GoB g) & (GoB g) * (b2,1) = S-min (L~ g) ) );

:: deftheorem Def6 defines i_e_s JORDAN5D:def 6 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_e_s g iff ( [b2,1] in Indices (GoB g) & (GoB g) * (b2,1) = S-max (L~ g) ) );

:: deftheorem Def7 defines i_w_n JORDAN5D:def 7 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_w_n g iff ( [b2,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b2,(width (GoB g))) = N-min (L~ g) ) );

:: deftheorem Def8 defines i_e_n JORDAN5D:def 8 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_e_n g iff ( [b2,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b2,(width (GoB g))) = N-max (L~ g) ) );

theorem :: JORDAN5D:45
for h being non constant standard special_circular_sequence holds
( 1 <= i_w_n h & i_w_n h <= len (GoB h) & 1 <= i_e_n h & i_e_n h <= len (GoB h) & 1 <= i_w_s h & i_w_s h <= len (GoB h) & 1 <= i_e_s h & i_e_s h <= len (GoB h) )
proof end;

theorem :: JORDAN5D:46
for h being non constant standard special_circular_sequence holds
( 1 <= i_n_e h & i_n_e h <= width (GoB h) & 1 <= i_s_e h & i_s_e h <= width (GoB h) & 1 <= i_n_w h & i_n_w h <= width (GoB h) & 1 <= i_s_w h & i_s_w h <= width (GoB h) )
proof end;

Lm10: for h being non constant standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 + 1 <= len h & 1 <= i2 & i2 + 1 <= len h & h . i1 = h . i2 holds
i1 = i2
proof end;

definition
let g be non constant standard special_circular_sequence;
func n_s_w g -> Nat means :Def9: :: JORDAN5D:def 9
( 1 <= it & it + 1 <= len g & g . it = W-min (L~ g) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = W-min (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len g & g . b1 = W-min (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = W-min (L~ g) holds
b1 = b2 by Lm10;
func n_n_w g -> Nat means :Def10: :: JORDAN5D:def 10
( 1 <= it & it + 1 <= len g & g . it = W-max (L~ g) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = W-max (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len g & g . b1 = W-max (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = W-max (L~ g) holds
b1 = b2 by Lm10;
func n_s_e g -> Nat means :Def11: :: JORDAN5D:def 11
( 1 <= it & it + 1 <= len g & g . it = E-min (L~ g) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = E-min (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len g & g . b1 = E-min (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = E-min (L~ g) holds
b1 = b2 by Lm10;
func n_n_e g -> Nat means :Def12: :: JORDAN5D:def 12
( 1 <= it & it + 1 <= len g & g . it = E-max (L~ g) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = E-max (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len g & g . b1 = E-max (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = E-max (L~ g) holds
b1 = b2 by Lm10;
func n_w_s g -> Nat means :Def13: :: JORDAN5D:def 13
( 1 <= it & it + 1 <= len g & g . it = S-min (L~ g) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = S-min (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len g & g . b1 = S-min (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = S-min (L~ g) holds
b1 = b2 by Lm10;
func n_e_s g -> Nat means :Def14: :: JORDAN5D:def 14
( 1 <= it & it + 1 <= len g & g . it = S-max (L~ g) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = S-max (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len g & g . b1 = S-max (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = S-max (L~ g) holds
b1 = b2 by Lm10;
func n_w_n g -> Nat means :Def15: :: JORDAN5D:def 15
( 1 <= it & it + 1 <= len g & g . it = N-min (L~ g) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = N-min (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len g & g . b1 = N-min (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = N-min (L~ g) holds
b1 = b2 by Lm10;
func n_e_n g -> Nat means :Def16: :: JORDAN5D:def 16
( 1 <= it & it + 1 <= len g & g . it = N-max (L~ g) );
existence
ex b1 being Nat st
( 1 <= b1 & b1 + 1 <= len g & g . b1 = N-max (L~ g) )
proof end;
uniqueness
for b1, b2 being Nat st 1 <= b1 & b1 + 1 <= len g & g . b1 = N-max (L~ g) & 1 <= b2 & b2 + 1 <= len g & g . b2 = N-max (L~ g) holds
b1 = b2 by Lm10;
end;

:: deftheorem Def9 defines n_s_w JORDAN5D:def 9 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_s_w g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = W-min (L~ g) ) );

:: deftheorem Def10 defines n_n_w JORDAN5D:def 10 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_n_w g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = W-max (L~ g) ) );

:: deftheorem Def11 defines n_s_e JORDAN5D:def 11 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_s_e g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = E-min (L~ g) ) );

:: deftheorem Def12 defines n_n_e JORDAN5D:def 12 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_n_e g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = E-max (L~ g) ) );

:: deftheorem Def13 defines n_w_s JORDAN5D:def 13 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_w_s g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = S-min (L~ g) ) );

:: deftheorem Def14 defines n_e_s JORDAN5D:def 14 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_e_s g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = S-max (L~ g) ) );

:: deftheorem Def15 defines n_w_n JORDAN5D:def 15 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_w_n g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = N-min (L~ g) ) );

:: deftheorem Def16 defines n_e_n JORDAN5D:def 16 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = n_e_n g iff ( 1 <= b2 & b2 + 1 <= len g & g . b2 = N-max (L~ g) ) );

theorem :: JORDAN5D:47
for h being non constant standard special_circular_sequence holds n_w_n h <> n_w_s h
proof end;

theorem :: JORDAN5D:48
for h being non constant standard special_circular_sequence holds n_s_w h <> n_s_e h
proof end;

theorem :: JORDAN5D:49
for h being non constant standard special_circular_sequence holds n_e_n h <> n_e_s h
proof end;

theorem :: JORDAN5D:50
for h being non constant standard special_circular_sequence holds n_n_w h <> n_n_e h
proof end;