:: by Yatsuka Nakamura and Adam Grabowski

::

:: Received June 8, 1998

:: Copyright (c) 1998-2019 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))

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

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

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 )

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 )

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

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

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 )

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 )

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

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

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

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

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

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

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

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

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

theorem :: JORDAN5D:20

theorem :: JORDAN5D:21

theorem :: JORDAN5D:22

theorem :: JORDAN5D:23

theorem :: JORDAN5D:24

theorem :: JORDAN5D:25

theorem :: JORDAN5D:26

theorem :: JORDAN5D:27

theorem :: JORDAN5D:28

theorem :: JORDAN5D:29

theorem :: JORDAN5D:30

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

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

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

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

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 )

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 )

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

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

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

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

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;

ex b_{1} being Nat st

( [1,b_{1}] in Indices (GoB g) & (GoB g) * (1,b_{1}) = W-min (L~ g) )

for b_{1}, b_{2} being Nat st [1,b_{1}] in Indices (GoB g) & (GoB g) * (1,b_{1}) = W-min (L~ g) & [1,b_{2}] in Indices (GoB g) & (GoB g) * (1,b_{2}) = W-min (L~ g) holds

b_{1} = b_{2}
by GOBOARD1:5;

ex b_{1} being Nat st

( [1,b_{1}] in Indices (GoB g) & (GoB g) * (1,b_{1}) = W-max (L~ g) )

for b_{1}, b_{2} being Nat st [1,b_{1}] in Indices (GoB g) & (GoB g) * (1,b_{1}) = W-max (L~ g) & [1,b_{2}] in Indices (GoB g) & (GoB g) * (1,b_{2}) = W-max (L~ g) holds

b_{1} = b_{2}
by GOBOARD1:5;

ex b_{1} being Nat st

( [(len (GoB g)),b_{1}] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b_{1}) = E-min (L~ g) )

for b_{1}, b_{2} being Nat st [(len (GoB g)),b_{1}] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b_{1}) = E-min (L~ g) & [(len (GoB g)),b_{2}] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b_{2}) = E-min (L~ g) holds

b_{1} = b_{2}
by GOBOARD1:5;

ex b_{1} being Nat st

( [(len (GoB g)),b_{1}] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b_{1}) = E-max (L~ g) )

for b_{1}, b_{2} being Nat st [(len (GoB g)),b_{1}] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b_{1}) = E-max (L~ g) & [(len (GoB g)),b_{2}] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b_{2}) = E-max (L~ g) holds

b_{1} = b_{2}
by GOBOARD1:5;

ex b_{1} being Nat st

( [b_{1},1] in Indices (GoB g) & (GoB g) * (b_{1},1) = S-min (L~ g) )

for b_{1}, b_{2} being Nat st [b_{1},1] in Indices (GoB g) & (GoB g) * (b_{1},1) = S-min (L~ g) & [b_{2},1] in Indices (GoB g) & (GoB g) * (b_{2},1) = S-min (L~ g) holds

b_{1} = b_{2}
by GOBOARD1:5;

ex b_{1} being Nat st

( [b_{1},1] in Indices (GoB g) & (GoB g) * (b_{1},1) = S-max (L~ g) )

for b_{1}, b_{2} being Nat st [b_{1},1] in Indices (GoB g) & (GoB g) * (b_{1},1) = S-max (L~ g) & [b_{2},1] in Indices (GoB g) & (GoB g) * (b_{2},1) = S-max (L~ g) holds

b_{1} = b_{2}
by GOBOARD1:5;

ex b_{1} being Nat st

( [b_{1},(width (GoB g))] in Indices (GoB g) & (GoB g) * (b_{1},(width (GoB g))) = N-min (L~ g) )

for b_{1}, b_{2} being Nat st [b_{1},(width (GoB g))] in Indices (GoB g) & (GoB g) * (b_{1},(width (GoB g))) = N-min (L~ g) & [b_{2},(width (GoB g))] in Indices (GoB g) & (GoB g) * (b_{2},(width (GoB g))) = N-min (L~ g) holds

b_{1} = b_{2}
by GOBOARD1:5;

ex b_{1} being Nat st

( [b_{1},(width (GoB g))] in Indices (GoB g) & (GoB g) * (b_{1},(width (GoB g))) = N-max (L~ g) )

for b_{1}, b_{2} being Nat st [b_{1},(width (GoB g))] in Indices (GoB g) & (GoB g) * (b_{1},(width (GoB g))) = N-max (L~ g) & [b_{2},(width (GoB g))] in Indices (GoB g) & (GoB g) * (b_{2},(width (GoB g))) = N-max (L~ g) holds

b_{1} = b_{2}
by GOBOARD1:5;

end;
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 ( [1,it] in Indices (GoB g) & (GoB g) * (1,it) = W-min (L~ g) );

ex b

( [1,b

proof end;

uniqueness for b

b

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 ( [1,it] in Indices (GoB g) & (GoB g) * (1,it) = W-max (L~ g) );

ex b

( [1,b

proof end;

uniqueness for b

b

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 ( [(len (GoB g)),it] in Indices (GoB g) & (GoB g) * ((len (GoB g)),it) = E-min (L~ g) );

ex b

( [(len (GoB g)),b

proof end;

uniqueness for b

b

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 ( [(len (GoB g)),it] in Indices (GoB g) & (GoB g) * ((len (GoB g)),it) = E-max (L~ g) );

ex b

( [(len (GoB g)),b

proof end;

uniqueness for b

b

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 ( [it,1] in Indices (GoB g) & (GoB g) * (it,1) = S-min (L~ g) );

ex b

( [b

proof end;

uniqueness for b

b

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 ( [it,1] in Indices (GoB g) & (GoB g) * (it,1) = S-max (L~ g) );

ex b

( [b

proof end;

uniqueness for b

b

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 ( [it,(width (GoB g))] in Indices (GoB g) & (GoB g) * (it,(width (GoB g))) = N-min (L~ g) );

ex b

( [b

proof end;

uniqueness for b

b

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 ( [it,(width (GoB g))] in Indices (GoB g) & (GoB g) * (it,(width (GoB g))) = N-max (L~ g) );

ex b

( [b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines i_s_w JORDAN5D:def 1 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = i_s_w g iff ( [1,b_{2}] in Indices (GoB g) & (GoB g) * (1,b_{2}) = W-min (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def2 defines i_n_w JORDAN5D:def 2 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = i_n_w g iff ( [1,b_{2}] in Indices (GoB g) & (GoB g) * (1,b_{2}) = W-max (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def3 defines i_s_e JORDAN5D:def 3 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = i_s_e g iff ( [(len (GoB g)),b_{2}] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b_{2}) = E-min (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def4 defines i_n_e JORDAN5D:def 4 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = i_n_e g iff ( [(len (GoB g)),b_{2}] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b_{2}) = E-max (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def5 defines i_w_s JORDAN5D:def 5 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = i_w_s g iff ( [b_{2},1] in Indices (GoB g) & (GoB g) * (b_{2},1) = S-min (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def6 defines i_e_s JORDAN5D:def 6 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = i_e_s g iff ( [b_{2},1] in Indices (GoB g) & (GoB g) * (b_{2},1) = S-max (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def7 defines i_w_n JORDAN5D:def 7 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = i_w_n g iff ( [b_{2},(width (GoB g))] in Indices (GoB g) & (GoB g) * (b_{2},(width (GoB g))) = N-min (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def8 defines i_e_n JORDAN5D:def 8 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = i_e_n g iff ( [b_{2},(width (GoB g))] in Indices (GoB g) & (GoB g) * (b_{2},(width (GoB g))) = N-max (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

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

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

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

ex b_{1} being Nat st

( 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = W-min (L~ g) )

for b_{1}, b_{2} being Nat st 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = W-min (L~ g) & 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = W-min (L~ g) holds

b_{1} = b_{2}
by Lm10;

ex b_{1} being Nat st

( 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = W-max (L~ g) )

for b_{1}, b_{2} being Nat st 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = W-max (L~ g) & 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = W-max (L~ g) holds

b_{1} = b_{2}
by Lm10;

ex b_{1} being Nat st

( 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = E-min (L~ g) )

for b_{1}, b_{2} being Nat st 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = E-min (L~ g) & 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = E-min (L~ g) holds

b_{1} = b_{2}
by Lm10;

ex b_{1} being Nat st

( 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = E-max (L~ g) )

for b_{1}, b_{2} being Nat st 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = E-max (L~ g) & 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = E-max (L~ g) holds

b_{1} = b_{2}
by Lm10;

ex b_{1} being Nat st

( 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = S-min (L~ g) )

for b_{1}, b_{2} being Nat st 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = S-min (L~ g) & 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = S-min (L~ g) holds

b_{1} = b_{2}
by Lm10;

ex b_{1} being Nat st

( 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = S-max (L~ g) )

for b_{1}, b_{2} being Nat st 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = S-max (L~ g) & 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = S-max (L~ g) holds

b_{1} = b_{2}
by Lm10;

ex b_{1} being Nat st

( 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = N-min (L~ g) )

for b_{1}, b_{2} being Nat st 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = N-min (L~ g) & 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = N-min (L~ g) holds

b_{1} = b_{2}
by Lm10;

ex b_{1} being Nat st

( 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = N-max (L~ g) )

for b_{1}, b_{2} being Nat st 1 <= b_{1} & b_{1} + 1 <= len g & g . b_{1} = N-max (L~ g) & 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = N-max (L~ g) holds

b_{1} = b_{2}
by Lm10;

end;
func n_s_w g -> Nat means :Def9: :: JORDAN5D:def 9

( 1 <= it & it + 1 <= len g & g . it = W-min (L~ g) );

existence ( 1 <= it & it + 1 <= len g & g . it = W-min (L~ g) );

ex b

( 1 <= b

proof end;

uniqueness for b

b

func n_n_w g -> Nat means :Def10: :: JORDAN5D:def 10

( 1 <= it & it + 1 <= len g & g . it = W-max (L~ g) );

existence ( 1 <= it & it + 1 <= len g & g . it = W-max (L~ g) );

ex b

( 1 <= b

proof end;

uniqueness for b

b

func n_s_e g -> Nat means :Def11: :: JORDAN5D:def 11

( 1 <= it & it + 1 <= len g & g . it = E-min (L~ g) );

existence ( 1 <= it & it + 1 <= len g & g . it = E-min (L~ g) );

ex b

( 1 <= b

proof end;

uniqueness for b

b

func n_n_e g -> Nat means :Def12: :: JORDAN5D:def 12

( 1 <= it & it + 1 <= len g & g . it = E-max (L~ g) );

existence ( 1 <= it & it + 1 <= len g & g . it = E-max (L~ g) );

ex b

( 1 <= b

proof end;

uniqueness for b

b

func n_w_s g -> Nat means :Def13: :: JORDAN5D:def 13

( 1 <= it & it + 1 <= len g & g . it = S-min (L~ g) );

existence ( 1 <= it & it + 1 <= len g & g . it = S-min (L~ g) );

ex b

( 1 <= b

proof end;

uniqueness for b

b

func n_e_s g -> Nat means :Def14: :: JORDAN5D:def 14

( 1 <= it & it + 1 <= len g & g . it = S-max (L~ g) );

existence ( 1 <= it & it + 1 <= len g & g . it = S-max (L~ g) );

ex b

( 1 <= b

proof end;

uniqueness for b

b

func n_w_n g -> Nat means :Def15: :: JORDAN5D:def 15

( 1 <= it & it + 1 <= len g & g . it = N-min (L~ g) );

existence ( 1 <= it & it + 1 <= len g & g . it = N-min (L~ g) );

ex b

( 1 <= b

proof end;

uniqueness for b

b

func n_e_n g -> Nat means :Def16: :: JORDAN5D:def 16

( 1 <= it & it + 1 <= len g & g . it = N-max (L~ g) );

existence ( 1 <= it & it + 1 <= len g & g . it = N-max (L~ g) );

ex b

( 1 <= b

proof end;

uniqueness for b

b

:: deftheorem Def9 defines n_s_w JORDAN5D:def 9 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = n_s_w g iff ( 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = W-min (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def10 defines n_n_w JORDAN5D:def 10 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = n_n_w g iff ( 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = W-max (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def11 defines n_s_e JORDAN5D:def 11 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = n_s_e g iff ( 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = E-min (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def12 defines n_n_e JORDAN5D:def 12 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = n_n_e g iff ( 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = E-max (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def13 defines n_w_s JORDAN5D:def 13 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = n_w_s g iff ( 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = S-min (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def14 defines n_e_s JORDAN5D:def 14 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = n_e_s g iff ( 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = S-max (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def15 defines n_w_n JORDAN5D:def 15 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = n_w_n g iff ( 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = N-min (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b

:: deftheorem Def16 defines n_e_n JORDAN5D:def 16 :

for g being non constant standard special_circular_sequence

for b_{2} being Nat holds

( b_{2} = n_e_n g iff ( 1 <= b_{2} & b_{2} + 1 <= len g & g . b_{2} = N-max (L~ g) ) );

for g being non constant standard special_circular_sequence

for b

( b