:: JORDAN5D semantic presentation begin theorem Th1: :: JORDAN5D:1 for n being Element of NAT for h being FinSequence of (TOP-REAL n) st len h >= 2 holds h /. (len h) in LSeg (h,((len h) -' 1)) proof let n be Element of NAT ; ::_thesis: for h being FinSequence of (TOP-REAL n) st len h >= 2 holds h /. (len h) in LSeg (h,((len h) -' 1)) let h be FinSequence of (TOP-REAL n); ::_thesis: ( len h >= 2 implies h /. (len h) in LSeg (h,((len h) -' 1)) ) set i = len h; assume A1: len h >= 2 ; ::_thesis: h /. (len h) in LSeg (h,((len h) -' 1)) then A2: 2 - 1 <= (len h) - 1 by XREAL_1:9; ((len h) -' 1) + 1 = len h by A1, XREAL_1:235, XXREAL_0:2; hence h /. (len h) in LSeg (h,((len h) -' 1)) by A2, TOPREAL1:21; ::_thesis: verum end; theorem Th2: :: JORDAN5D:2 for i being Element of NAT st 3 <= i holds i mod (i -' 1) = 1 proof let i be Element of NAT ; ::_thesis: ( 3 <= i implies i mod (i -' 1) = 1 ) assume A1: 3 <= i ; ::_thesis: i mod (i -' 1) = 1 then A2: i -' 1 = i - 1 by XREAL_1:233, XXREAL_0:2; 3 -' 1 = (2 + 1) -' 1 .= 2 by NAT_D:34 ; then 2 <= i -' 1 by A1, NAT_D:42; then 1 < i - 1 by A2, XXREAL_0:2; then 1 + i < (i - 1) + i by XREAL_1:8; then (1 + i) - 1 < ((i - 1) + i) - 1 by XREAL_1:14; then A3: i < (i - 1) + (i - 1) ; i -' 1 <= i by NAT_D:35; hence i mod (i -' 1) = i - (i - 1) by A2, A3, JORDAN4:2 .= 1 ; ::_thesis: verum 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 Element of NAT st ( 1 <= i & i + 1 <= len h & h . i = p ) proof let p be Point of (TOP-REAL 2); ::_thesis: for h being non constant standard special_circular_sequence st p in rng h holds ex i being Element of NAT st ( 1 <= i & i + 1 <= len h & h . i = p ) let h be non constant standard special_circular_sequence; ::_thesis: ( p in rng h implies ex i being Element of NAT st ( 1 <= i & i + 1 <= len h & h . i = p ) ) A1: 4 < len h by GOBOARD7:34; A2: 1 < len h by GOBOARD7:34, XXREAL_0:2; assume p in rng h ; ::_thesis: ex i being Element of NAT st ( 1 <= i & i + 1 <= len h & h . i = p ) then consider x being set such that A3: x in dom h and A4: p = h . x by FUNCT_1:def_3; reconsider i = x as Element of NAT by A3; A5: 1 <= i by A3, FINSEQ_3:25; set j = S_Drop (i,h); A6: i <= len h by A3, FINSEQ_3:25; ( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p ) proof A7: i <= ((len h) -' 1) + 1 by A5, A6, XREAL_1:235, XXREAL_0:2; percases ( i <= (len h) -' 1 or i = ((len h) -' 1) + 1 ) by A7, NAT_1:8; supposeA8: i <= (len h) -' 1 ; ::_thesis: ( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p ) then S_Drop (i,h) = i by A5, JORDAN4:22; then (S_Drop (i,h)) + 1 <= ((len h) -' 1) + 1 by A8, XREAL_1:7; hence ( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p ) by A4, A5, A2, A8, JORDAN4:22, XREAL_1:235; ::_thesis: verum end; supposeA9: i = ((len h) -' 1) + 1 ; ::_thesis: ( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p ) then i = len h by A1, XREAL_1:235, XXREAL_0:2; then i mod ((len h) -' 1) = 1 by A1, Th2, XXREAL_0:2; then A10: S_Drop (i,h) = 1 by JORDAN4:def_1; A11: 1 <= len h by GOBOARD7:34, XXREAL_0:2; then A12: len h in dom h by FINSEQ_3:25; 1 in dom h by A11, FINSEQ_3:25; then h . 1 = h /. 1 by PARTFUN1:def_6 .= h /. (len h) by FINSEQ_6:def_1 .= h . (len h) by A12, PARTFUN1:def_6 ; hence ( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p ) by A4, A1, A9, A10, XREAL_1:235, XXREAL_0:2; ::_thesis: verum end; end; end; hence ex i being Element of NAT st ( 1 <= i & i + 1 <= len h & h . i = p ) ; ::_thesis: verum 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 let r be Real; ::_thesis: for g being FinSequence of REAL st r in rng g holds ( (Incr g) . 1 <= r & r <= (Incr g) . (len (Incr g)) ) let g be FinSequence of REAL ; ::_thesis: ( r in rng g implies ( (Incr g) . 1 <= r & r <= (Incr g) . (len (Incr g)) ) ) assume r in rng g ; ::_thesis: ( (Incr g) . 1 <= r & r <= (Incr g) . (len (Incr g)) ) then r in rng (Incr g) by SEQ_4:def_21; then consider x being set such that A1: x in dom (Incr g) and A2: (Incr g) . x = r by FUNCT_1:def_3; reconsider j = x as Element of NAT by A1; A3: x in Seg (len (Incr g)) by A1, FINSEQ_1:def_3; then A4: j <= len (Incr g) by FINSEQ_1:1; A5: 1 <= j by A3, FINSEQ_1:1; then A6: 1 <= len (Incr g) by A4, XXREAL_0:2; then 1 in dom (Incr g) by FINSEQ_3:25; hence (Incr g) . 1 <= r by A1, A2, A5, SEQ_4:137; ::_thesis: r <= (Incr g) . (len (Incr g)) len (Incr g) in dom (Incr g) by A6, FINSEQ_3:25; hence r <= (Incr g) . (len (Incr g)) by A1, A2, A4, SEQ_4:137; ::_thesis: verum end; theorem Th5: :: JORDAN5D:5 for h being non constant standard special_circular_sequence for i, I being Element of 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 let h be non constant standard special_circular_sequence; ::_thesis: for i, I being Element of 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 ) let i, I be Element of NAT ; ::_thesis: ( 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) implies ( ((GoB h) * (1,I)) `1 <= (h /. i) `1 & (h /. i) `1 <= ((GoB h) * ((len (GoB h)),I)) `1 ) ) assume that A1: 1 <= i and A2: i <= len h and A3: 1 <= I and A4: I <= width (GoB h) ; ::_thesis: ( ((GoB h) * (1,I)) `1 <= (h /. i) `1 & (h /. i) `1 <= ((GoB h) * ((len (GoB h)),I)) `1 ) A5: I <= width (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A4, GOBOARD2:def_2; i <= len (X_axis h) by A2, GOBOARD1:def_1; then A6: i in dom (X_axis h) by A1, FINSEQ_3:25; then (X_axis h) . i = (h /. i) `1 by GOBOARD1:def_1; then A7: (h /. i) `1 in rng (X_axis h) by A6, FUNCT_1:def_3; A8: GoB h = GoB ((Incr (X_axis h)),(Incr (Y_axis h))) by GOBOARD2:def_2; then 1 <= len (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by GOBOARD7:32; then A9: [1,I] in Indices (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A3, A5, MATRIX_1:36; A10: 1 <= len (GoB h) by GOBOARD7:32; len (GoB h) <= len (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by GOBOARD2:def_2; then A11: [(len (GoB h)),I] in Indices (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A3, A5, A10, MATRIX_1:36; (GoB h) * ((len (GoB h)),I) = (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) * ((len (GoB h)),I) by GOBOARD2:def_2 .= |[((Incr (X_axis h)) . (len (GoB h))),((Incr (Y_axis h)) . I)]| by A11, GOBOARD2:def_1 ; then A12: ((GoB h) * ((len (GoB h)),I)) `1 = (Incr (X_axis h)) . (len (GoB h)) by EUCLID:52; (GoB h) * (1,I) = (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) * (1,I) by GOBOARD2:def_2 .= |[((Incr (X_axis h)) . 1),((Incr (Y_axis h)) . I)]| by A9, GOBOARD2:def_1 ; then A13: ((GoB h) * (1,I)) `1 = (Incr (X_axis h)) . 1 by EUCLID:52; len (GoB h) = len (Incr (X_axis h)) by A8, GOBOARD2:def_1; hence ( ((GoB h) * (1,I)) `1 <= (h /. i) `1 & (h /. i) `1 <= ((GoB h) * ((len (GoB h)),I)) `1 ) by A12, A13, A7, Th4; ::_thesis: verum end; theorem Th6: :: JORDAN5D:6 for h being non constant standard special_circular_sequence for i, I being Element of 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 let h be non constant standard special_circular_sequence; ::_thesis: for i, I being Element of 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 ) let i, I be Element of NAT ; ::_thesis: ( 1 <= i & i <= len h & 1 <= I & I <= len (GoB h) implies ( ((GoB h) * (I,1)) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * (I,(width (GoB h)))) `2 ) ) assume that A1: 1 <= i and A2: i <= len h and A3: 1 <= I and A4: I <= len (GoB h) ; ::_thesis: ( ((GoB h) * (I,1)) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * (I,(width (GoB h)))) `2 ) A5: GoB h = GoB ((Incr (X_axis h)),(Incr (Y_axis h))) by GOBOARD2:def_2; then A6: 1 <= width (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by GOBOARD7:33; i <= len (Y_axis h) by A2, GOBOARD1:def_2; then A7: i in dom (Y_axis h) by A1, FINSEQ_3:25; then (Y_axis h) . i = (h /. i) `2 by GOBOARD1:def_2; then A8: (h /. i) `2 in rng (Y_axis h) by A7, FUNCT_1:def_3; 1 <= width (GoB h) by GOBOARD7:33; then A9: [I,(width (GoB h))] in Indices (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A3, A4, A5, MATRIX_1:36; (GoB h) * (I,(width (GoB h))) = (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) * (I,(width (GoB h))) by GOBOARD2:def_2 .= |[((Incr (X_axis h)) . I),((Incr (Y_axis h)) . (width (GoB h)))]| by A9, GOBOARD2:def_1 ; then A10: ((GoB h) * (I,(width (GoB h)))) `2 = (Incr (Y_axis h)) . (width (GoB h)) by EUCLID:52; I <= len (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A4, GOBOARD2:def_2; then A11: [I,1] in Indices (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A3, A6, MATRIX_1:36; (GoB h) * (I,1) = (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) * (I,1) by GOBOARD2:def_2 .= |[((Incr (X_axis h)) . I),((Incr (Y_axis h)) . 1)]| by A11, GOBOARD2:def_1 ; then A12: ((GoB h) * (I,1)) `2 = (Incr (Y_axis h)) . 1 by EUCLID:52; width (GoB h) = len (Incr (Y_axis h)) by A5, GOBOARD2:def_1; hence ( ((GoB h) * (I,1)) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * (I,(width (GoB h)))) `2 ) by A10, A12, A8, Th4; ::_thesis: verum end; theorem Th7: :: JORDAN5D:7 for f being non empty FinSequence of (TOP-REAL 2) for i being Element of NAT st 1 <= i & i <= len (GoB f) holds ex k, j being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st 1 <= i & i <= len (GoB f) holds ex k, j being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len (GoB f) implies ex k, j being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) ) assume that A1: 1 <= i and A2: i <= len (GoB f) ; ::_thesis: ex k, j being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) A3: i in dom (GoB f) by A1, A2, FINSEQ_3:25; A4: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def_2; then len (Incr (X_axis f)) = len (GoB f) by GOBOARD2:def_1; then i in dom (Incr (X_axis f)) by A1, A2, FINSEQ_3:25; then (Incr (X_axis f)) . i in rng (Incr (X_axis f)) by FUNCT_1:def_3; then (Incr (X_axis f)) . i in rng (X_axis f) by SEQ_4:def_21; then consider k being Nat such that A5: k in dom (X_axis f) and A6: (X_axis f) . k = (Incr (X_axis f)) . i by FINSEQ_2:10; A7: len (X_axis f) = len f by GOBOARD1:def_1 .= len (Y_axis f) by GOBOARD1:def_2 ; then dom (X_axis f) = dom (Y_axis f) by FINSEQ_3:29; then (Y_axis f) . k in rng (Y_axis f) by A5, FUNCT_1:def_3; then (Y_axis f) . k in rng (Incr (Y_axis f)) by SEQ_4:def_21; then consider j being Nat such that A8: j in dom (Incr (Y_axis f)) and A9: (Y_axis f) . k = (Incr (Y_axis f)) . j by FINSEQ_2:10; reconsider k = k, j = j as Element of NAT by ORDINAL1:def_12; A10: (X_axis f) . k = (f /. k) `1 by A5, GOBOARD1:def_1; take k ; ::_thesis: ex j being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) take j ; ::_thesis: ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) len (X_axis f) = len f by GOBOARD1:def_1; hence k in dom f by A5, FINSEQ_3:29; ::_thesis: ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) j in Seg (len (Incr (Y_axis f))) by A8, FINSEQ_1:def_3; then j in Seg (width (GoB ((Incr (X_axis f)),(Incr (Y_axis f))))) by GOBOARD2:def_1; then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by A4, A3, ZFMISC_1:87; hence A11: [i,j] in Indices (GoB f) by MATRIX_1:def_4; ::_thesis: f /. k = (GoB f) * (i,j) dom (X_axis f) = dom (Y_axis f) by A7, FINSEQ_3:29; then (Y_axis f) . k = (f /. k) `2 by A5, GOBOARD1:def_2; hence f /. k = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A6, A9, A10, EUCLID:53 .= (GoB f) * (i,j) by A4, A11, GOBOARD2:def_1 ; ::_thesis: verum end; theorem Th8: :: JORDAN5D:8 for f being non empty FinSequence of (TOP-REAL 2) for j being Element of NAT st 1 <= j & j <= width (GoB f) holds ex k, i being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for j being Element of NAT st 1 <= j & j <= width (GoB f) holds ex k, i being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= width (GoB f) implies ex k, i being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) ) assume that A1: 1 <= j and A2: j <= width (GoB f) ; ::_thesis: ex k, i being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) A3: j in Seg (width (GoB f)) by A1, A2, FINSEQ_1:1; A4: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def_2; then len (Incr (Y_axis f)) = width (GoB f) by GOBOARD2:def_1; then j in dom (Incr (Y_axis f)) by A1, A2, FINSEQ_3:25; then (Incr (Y_axis f)) . j in rng (Incr (Y_axis f)) by FUNCT_1:def_3; then (Incr (Y_axis f)) . j in rng (Y_axis f) by SEQ_4:def_21; then consider k being Nat such that A5: k in dom (Y_axis f) and A6: (Y_axis f) . k = (Incr (Y_axis f)) . j by FINSEQ_2:10; A7: len (X_axis f) = len f by GOBOARD1:def_1 .= len (Y_axis f) by GOBOARD1:def_2 ; then k in dom (X_axis f) by A5, FINSEQ_3:29; then (X_axis f) . k in rng (X_axis f) by FUNCT_1:def_3; then (X_axis f) . k in rng (Incr (X_axis f)) by SEQ_4:def_21; then consider i being Nat such that A8: i in dom (Incr (X_axis f)) and A9: (X_axis f) . k = (Incr (X_axis f)) . i by FINSEQ_2:10; reconsider k = k, i = i as Element of NAT by ORDINAL1:def_12; k in dom (X_axis f) by A5, A7, FINSEQ_3:29; then A10: (X_axis f) . k = (f /. k) `1 by GOBOARD1:def_1; take k ; ::_thesis: ex i being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) take i ; ::_thesis: ( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) len (Y_axis f) = len f by GOBOARD1:def_2; hence k in dom f by A5, FINSEQ_3:29; ::_thesis: ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) len (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) = len (Incr (X_axis f)) by GOBOARD2:def_1; then i in dom (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) by A8, FINSEQ_3:29; then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by A4, A3, ZFMISC_1:87; hence A11: [i,j] in Indices (GoB f) by MATRIX_1:def_4; ::_thesis: f /. k = (GoB f) * (i,j) (Y_axis f) . k = (f /. k) `2 by A5, GOBOARD1:def_2; hence f /. k = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A6, A9, A10, EUCLID:53 .= (GoB f) * (i,j) by A4, A11, GOBOARD2:def_1 ; ::_thesis: verum end; theorem Th9: :: JORDAN5D:9 for f being non empty FinSequence of (TOP-REAL 2) for i, j being Element of NAT st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds ex k being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `1 = ((GoB f) * (i,j)) `1 ) proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds ex k being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `1 = ((GoB f) * (i,j)) `1 ) let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) implies ex k being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `1 = ((GoB f) * (i,j)) `1 ) ) assume that A1: 1 <= i and A2: i <= len (GoB f) and A3: 1 <= j and A4: j <= width (GoB f) ; ::_thesis: ex k being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `1 = ((GoB f) * (i,j)) `1 ) A5: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def_2; then len (Incr (Y_axis f)) = width (GoB f) by GOBOARD2:def_1; then j in dom (Incr (Y_axis f)) by A3, A4, FINSEQ_3:25; then j in Seg (len (Incr (Y_axis f))) by FINSEQ_1:def_3; then A6: j in Seg (width (GoB ((Incr (X_axis f)),(Incr (Y_axis f))))) by GOBOARD2:def_1; len (Incr (X_axis f)) = len (GoB f) by A5, GOBOARD2:def_1; then i in dom (Incr (X_axis f)) by A1, A2, FINSEQ_3:25; then (Incr (X_axis f)) . i in rng (Incr (X_axis f)) by FUNCT_1:def_3; then (Incr (X_axis f)) . i in rng (X_axis f) by SEQ_4:def_21; then consider k being Nat such that A7: k in dom (X_axis f) and A8: (X_axis f) . k = (Incr (X_axis f)) . i by FINSEQ_2:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; take k ; ::_thesis: ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `1 = ((GoB f) * (i,j)) `1 ) len (X_axis f) = len f by GOBOARD1:def_1; hence k in dom f by A7, FINSEQ_3:29; ::_thesis: ( [i,j] in Indices (GoB f) & (f /. k) `1 = ((GoB f) * (i,j)) `1 ) i in dom (GoB f) by A1, A2, FINSEQ_3:25; then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by A5, A6, ZFMISC_1:87; hence [i,j] in Indices (GoB f) by MATRIX_1:def_4; ::_thesis: (f /. k) `1 = ((GoB f) * (i,j)) `1 then A9: (GoB f) * (i,j) = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A5, GOBOARD2:def_1; thus (f /. k) `1 = (Incr (X_axis f)) . i by A7, A8, GOBOARD1:def_1 .= ((GoB f) * (i,j)) `1 by A9, EUCLID:52 ; ::_thesis: verum end; theorem Th10: :: JORDAN5D:10 for f being non empty FinSequence of (TOP-REAL 2) for i, j being Element of NAT st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds ex k being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 ) proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds ex k being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 ) let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) implies ex k being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 ) ) assume that A1: 1 <= i and A2: i <= len (GoB f) and A3: 1 <= j and A4: j <= width (GoB f) ; ::_thesis: ex k being Element of NAT st ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 ) A5: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def_2; then len (Incr (Y_axis f)) = width (GoB f) by GOBOARD2:def_1; then j in dom (Incr (Y_axis f)) by A3, A4, FINSEQ_3:25; then j in Seg (len (Incr (Y_axis f))) by FINSEQ_1:def_3; then A6: j in Seg (width (GoB ((Incr (X_axis f)),(Incr (Y_axis f))))) by GOBOARD2:def_1; len (Incr (Y_axis f)) = width (GoB f) by A5, GOBOARD2:def_1; then j in dom (Incr (Y_axis f)) by A3, A4, FINSEQ_3:25; then (Incr (Y_axis f)) . j in rng (Incr (Y_axis f)) by FUNCT_1:def_3; then (Incr (Y_axis f)) . j in rng (Y_axis f) by SEQ_4:def_21; then consider k being Nat such that A7: k in dom (Y_axis f) and A8: (Y_axis f) . k = (Incr (Y_axis f)) . j by FINSEQ_2:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; take k ; ::_thesis: ( k in dom f & [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 ) len (Y_axis f) = len f by GOBOARD1:def_2; hence k in dom f by A7, FINSEQ_3:29; ::_thesis: ( [i,j] in Indices (GoB f) & (f /. k) `2 = ((GoB f) * (i,j)) `2 ) i in dom (GoB f) by A1, A2, FINSEQ_3:25; then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by A5, A6, ZFMISC_1:87; hence [i,j] in Indices (GoB f) by MATRIX_1:def_4; ::_thesis: (f /. k) `2 = ((GoB f) * (i,j)) `2 then A9: (GoB f) * (i,j) = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A5, GOBOARD2:def_1; thus (f /. k) `2 = (Incr (Y_axis f)) . j by A7, A8, GOBOARD1:def_2 .= ((GoB f) * (i,j)) `2 by A9, EUCLID:52 ; ::_thesis: verum end; begin theorem Th11: :: JORDAN5D:11 for h being non constant standard special_circular_sequence for i being Element of NAT st 1 <= i & i <= len h holds ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) ) proof let h be non constant standard special_circular_sequence; ::_thesis: for i being Element of NAT st 1 <= i & i <= len h holds ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) ) let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len h implies ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) ) ) A1: len h > 4 by GOBOARD7:34; assume that A2: 1 <= i and A3: i <= len h ; ::_thesis: ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) ) i in dom h by A2, A3, FINSEQ_3:25; then h /. i in L~ h by A1, GOBOARD1:1, XXREAL_0:2; hence ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) ) by PSCOMP_1:24; ::_thesis: verum end; theorem Th12: :: JORDAN5D:12 for h being non constant standard special_circular_sequence for i being Element of NAT st 1 <= i & i <= len h holds ( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) ) proof let h be non constant standard special_circular_sequence; ::_thesis: for i being Element of NAT st 1 <= i & i <= len h holds ( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) ) let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len h implies ( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) ) ) A1: len h > 4 by GOBOARD7:34; assume that A2: 1 <= i and A3: i <= len h ; ::_thesis: ( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) ) i in dom h by A2, A3, FINSEQ_3:25; then h /. i in L~ h by A1, GOBOARD1:1, XXREAL_0:2; hence ( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) ) by PSCOMP_1:24; ::_thesis: verum 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 let h be non constant standard special_circular_sequence; ::_thesis: 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))) set T = (TOP-REAL 2) | (W-most (L~ h)); set F = proj2 | (W-most (L~ h)); let X be Subset of REAL; ::_thesis: ( X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } implies X = (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) ) assume A1: X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } ; ::_thesis: X = (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) thus X c= (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) :: according to XBOOLE_0:def_10 ::_thesis: (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) ) A2: dom (proj2 | (W-most (L~ h))) = the carrier of ((TOP-REAL 2) | (W-most (L~ h))) by FUNCT_2:def_1 .= [#] ((TOP-REAL 2) | (W-most (L~ h))) .= W-most (L~ h) by PRE_TOPC:def_5 ; assume x in X ; ::_thesis: x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) then consider q1 being Point of (TOP-REAL 2) such that A3: q1 `2 = x and A4: q1 `1 = W-bound (L~ h) and A5: q1 in L~ h by A1; A6: x = (proj2 | (W-most (L~ h))) . q1 by A3, A4, A5, PSCOMP_1:23, SPRECT_2:12; A7: q1 in W-most (L~ h) by A4, A5, SPRECT_2:12; then q1 in the carrier of ((TOP-REAL 2) | (W-most (L~ h))) by A2, FUNCT_2:def_1; hence x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) by A2, A7, A6, FUNCT_1:def_6; ::_thesis: verum end; thus (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) c= X ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) or x in X ) A8: W-most (L~ h) c= L~ h by XBOOLE_1:17; assume x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) ; ::_thesis: x in X then consider x1 being set such that x1 in dom (proj2 | (W-most (L~ h))) and A9: x1 in the carrier of ((TOP-REAL 2) | (W-most (L~ h))) and A10: x = (proj2 | (W-most (L~ h))) . x1 by FUNCT_1:def_6; x1 in [#] ((TOP-REAL 2) | (W-most (L~ h))) by A9; then A11: x1 in W-most (L~ h) by PRE_TOPC:def_5; then reconsider x2 = x1 as Element of (TOP-REAL 2) ; A12: x2 `1 = (W-min (L~ h)) `1 by A11, PSCOMP_1:31 .= W-bound (L~ h) by EUCLID:52 ; x = x2 `2 by A10, A11, PSCOMP_1:23; hence x in X by A1, A11, A12, A8; ::_thesis: verum end; 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 let h be non constant standard special_circular_sequence; ::_thesis: 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))) set T = (TOP-REAL 2) | (E-most (L~ h)); set F = proj2 | (E-most (L~ h)); let X be Subset of REAL; ::_thesis: ( X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ h) & q in L~ h ) } implies X = (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) ) assume A1: X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ h) & q in L~ h ) } ; ::_thesis: X = (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) thus X c= (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) :: according to XBOOLE_0:def_10 ::_thesis: (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) ) A2: dom (proj2 | (E-most (L~ h))) = the carrier of ((TOP-REAL 2) | (E-most (L~ h))) by FUNCT_2:def_1 .= [#] ((TOP-REAL 2) | (E-most (L~ h))) .= E-most (L~ h) by PRE_TOPC:def_5 ; assume x in X ; ::_thesis: x in (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) then consider q1 being Point of (TOP-REAL 2) such that A3: q1 `2 = x and A4: q1 `1 = E-bound (L~ h) and A5: q1 in L~ h by A1; A6: x = (proj2 | (E-most (L~ h))) . q1 by A3, A4, A5, PSCOMP_1:23, SPRECT_2:13; A7: q1 in E-most (L~ h) by A4, A5, SPRECT_2:13; then q1 in the carrier of ((TOP-REAL 2) | (E-most (L~ h))) by A2, FUNCT_2:def_1; hence x in (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) by A2, A7, A6, FUNCT_1:def_6; ::_thesis: verum end; thus (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) c= X ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) or x in X ) A8: E-most (L~ h) c= L~ h by XBOOLE_1:17; assume x in (proj2 | (E-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (E-most (L~ h))) ; ::_thesis: x in X then consider x1 being set such that x1 in dom (proj2 | (E-most (L~ h))) and A9: x1 in the carrier of ((TOP-REAL 2) | (E-most (L~ h))) and A10: x = (proj2 | (E-most (L~ h))) . x1 by FUNCT_1:def_6; x1 in [#] ((TOP-REAL 2) | (E-most (L~ h))) by A9; then A11: x1 in E-most (L~ h) by PRE_TOPC:def_5; then reconsider x2 = x1 as Element of (TOP-REAL 2) ; A12: x2 `1 = (E-min (L~ h)) `1 by A11, PSCOMP_1:47 .= E-bound (L~ h) by EUCLID:52 ; x = x2 `2 by A10, A11, PSCOMP_1:23; hence x in X by A1, A11, A12, A8; ::_thesis: verum end; 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 let h be non constant standard special_circular_sequence; ::_thesis: 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))) set T = (TOP-REAL 2) | (N-most (L~ h)); set F = proj1 | (N-most (L~ h)); let X be Subset of REAL; ::_thesis: ( X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } implies X = (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) ) assume A1: X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } ; ::_thesis: X = (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) thus X c= (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) :: according to XBOOLE_0:def_10 ::_thesis: (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) ) A2: dom (proj1 | (N-most (L~ h))) = the carrier of ((TOP-REAL 2) | (N-most (L~ h))) by FUNCT_2:def_1 .= [#] ((TOP-REAL 2) | (N-most (L~ h))) .= N-most (L~ h) by PRE_TOPC:def_5 ; assume x in X ; ::_thesis: x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) then consider q1 being Point of (TOP-REAL 2) such that A3: q1 `1 = x and A4: q1 `2 = N-bound (L~ h) and A5: q1 in L~ h by A1; A6: x = (proj1 | (N-most (L~ h))) . q1 by A3, A4, A5, PSCOMP_1:22, SPRECT_2:10; A7: q1 in N-most (L~ h) by A4, A5, SPRECT_2:10; then q1 in the carrier of ((TOP-REAL 2) | (N-most (L~ h))) by A2, FUNCT_2:def_1; hence x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) by A2, A7, A6, FUNCT_1:def_6; ::_thesis: verum end; thus (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) c= X ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) or x in X ) A8: N-most (L~ h) c= L~ h by XBOOLE_1:17; assume x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) ; ::_thesis: x in X then consider x1 being set such that x1 in dom (proj1 | (N-most (L~ h))) and A9: x1 in the carrier of ((TOP-REAL 2) | (N-most (L~ h))) and A10: x = (proj1 | (N-most (L~ h))) . x1 by FUNCT_1:def_6; x1 in [#] ((TOP-REAL 2) | (N-most (L~ h))) by A9; then A11: x1 in N-most (L~ h) by PRE_TOPC:def_5; then reconsider x2 = x1 as Element of (TOP-REAL 2) ; A12: x2 `2 = (N-min (L~ h)) `2 by A11, PSCOMP_1:39 .= N-bound (L~ h) by EUCLID:52 ; x = x2 `1 by A10, A11, PSCOMP_1:22; hence x in X by A1, A11, A12, A8; ::_thesis: verum end; 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 let h be non constant standard special_circular_sequence; ::_thesis: 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))) set T = (TOP-REAL 2) | (S-most (L~ h)); set F = proj1 | (S-most (L~ h)); let X be Subset of REAL; ::_thesis: ( X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ h) & q in L~ h ) } implies X = (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) ) assume A1: X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ h) & q in L~ h ) } ; ::_thesis: X = (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) thus X c= (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) :: according to XBOOLE_0:def_10 ::_thesis: (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) ) A2: dom (proj1 | (S-most (L~ h))) = the carrier of ((TOP-REAL 2) | (S-most (L~ h))) by FUNCT_2:def_1 .= [#] ((TOP-REAL 2) | (S-most (L~ h))) .= S-most (L~ h) by PRE_TOPC:def_5 ; assume x in X ; ::_thesis: x in (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) then consider q1 being Point of (TOP-REAL 2) such that A3: q1 `1 = x and A4: q1 `2 = S-bound (L~ h) and A5: q1 in L~ h by A1; A6: x = (proj1 | (S-most (L~ h))) . q1 by A3, A4, A5, PSCOMP_1:22, SPRECT_2:11; A7: q1 in S-most (L~ h) by A4, A5, SPRECT_2:11; then q1 in the carrier of ((TOP-REAL 2) | (S-most (L~ h))) by A2, FUNCT_2:def_1; hence x in (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) by A2, A7, A6, FUNCT_1:def_6; ::_thesis: verum end; thus (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) c= X ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) or x in X ) A8: S-most (L~ h) c= L~ h by XBOOLE_1:17; assume x in (proj1 | (S-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (S-most (L~ h))) ; ::_thesis: x in X then consider x1 being set such that x1 in dom (proj1 | (S-most (L~ h))) and A9: x1 in the carrier of ((TOP-REAL 2) | (S-most (L~ h))) and A10: x = (proj1 | (S-most (L~ h))) . x1 by FUNCT_1:def_6; x1 in [#] ((TOP-REAL 2) | (S-most (L~ h))) by A9; then A11: x1 in S-most (L~ h) by PRE_TOPC:def_5; then reconsider x2 = x1 as Element of (TOP-REAL 2) ; A12: x2 `2 = (S-min (L~ h)) `2 by A11, PSCOMP_1:55 .= S-bound (L~ h) by EUCLID:52 ; x = x2 `1 by A10, A11, PSCOMP_1:22; hence x in X by A1, A11, A12, A8; ::_thesis: verum end; 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 let g be FinSequence of (TOP-REAL 2); ::_thesis: 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)) set T = (TOP-REAL 2) | (L~ g); set F = proj1 | (L~ g); let X be Subset of REAL; ::_thesis: ( X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } implies X = (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) ) assume A1: X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } ; ::_thesis: X = (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) thus X c= (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) :: according to XBOOLE_0:def_10 ::_thesis: (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) ) assume x in X ; ::_thesis: x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) then consider q1 being Point of (TOP-REAL 2) such that A2: q1 `1 = x and A3: q1 in L~ g by A1; A4: x = (proj1 | (L~ g)) . q1 by A2, A3, PSCOMP_1:22; A5: dom (proj1 | (L~ g)) = the carrier of ((TOP-REAL 2) | (L~ g)) by FUNCT_2:def_1 .= [#] ((TOP-REAL 2) | (L~ g)) .= L~ g by PRE_TOPC:def_5 ; then q1 in the carrier of ((TOP-REAL 2) | (L~ g)) by A3, FUNCT_2:def_1; hence x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) by A3, A5, A4, FUNCT_1:def_6; ::_thesis: verum end; thus (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) c= X ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) or x in X ) assume x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) ; ::_thesis: x in X then consider x1 being set such that x1 in dom (proj1 | (L~ g)) and A6: x1 in the carrier of ((TOP-REAL 2) | (L~ g)) and A7: x = (proj1 | (L~ g)) . x1 by FUNCT_1:def_6; x1 in [#] ((TOP-REAL 2) | (L~ g)) by A6; then A8: x1 in L~ g by PRE_TOPC:def_5; then reconsider x2 = x1 as Element of (TOP-REAL 2) ; x = x2 `1 by A7, A8, PSCOMP_1:22; hence x in X by A1, A8; ::_thesis: verum end; 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 let g be FinSequence of (TOP-REAL 2); ::_thesis: 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)) set T = (TOP-REAL 2) | (L~ g); set F = proj2 | (L~ g); let X be Subset of REAL; ::_thesis: ( X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } implies X = (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) ) assume A1: X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } ; ::_thesis: X = (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) thus X c= (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) :: according to XBOOLE_0:def_10 ::_thesis: (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) ) assume x in X ; ::_thesis: x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) then consider q1 being Point of (TOP-REAL 2) such that A2: q1 `2 = x and A3: q1 in L~ g by A1; A4: x = (proj2 | (L~ g)) . q1 by A2, A3, PSCOMP_1:23; A5: dom (proj2 | (L~ g)) = the carrier of ((TOP-REAL 2) | (L~ g)) by FUNCT_2:def_1 .= [#] ((TOP-REAL 2) | (L~ g)) .= L~ g by PRE_TOPC:def_5 ; then q1 in the carrier of ((TOP-REAL 2) | (L~ g)) by A3, FUNCT_2:def_1; hence x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) by A3, A5, A4, FUNCT_1:def_6; ::_thesis: verum end; thus (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) c= X ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) or x in X ) assume x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) ; ::_thesis: x in X then consider x1 being set such that x1 in dom (proj2 | (L~ g)) and A6: x1 in the carrier of ((TOP-REAL 2) | (L~ g)) and A7: x = (proj2 | (L~ g)) . x1 by FUNCT_1:def_6; x1 in [#] ((TOP-REAL 2) | (L~ g)) by A6; then A8: x1 in L~ g by PRE_TOPC:def_5; then reconsider x2 = x1 as Element of (TOP-REAL 2) ; x = x2 `2 by A7, A8, PSCOMP_1:23; hence x in X by A1, A8; ::_thesis: verum end; 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 Element of NAT st p in L~ h & 1 <= I & I <= width (GoB h) holds ((GoB h) * (1,I)) `1 <= p `1 proof let p be Point of (TOP-REAL 2); ::_thesis: for h being non constant standard special_circular_sequence for I being Element of NAT st p in L~ h & 1 <= I & I <= width (GoB h) holds ((GoB h) * (1,I)) `1 <= p `1 let h be non constant standard special_circular_sequence; ::_thesis: for I being Element of NAT st p in L~ h & 1 <= I & I <= width (GoB h) holds ((GoB h) * (1,I)) `1 <= p `1 let I be Element of NAT ; ::_thesis: ( p in L~ h & 1 <= I & I <= width (GoB h) implies ((GoB h) * (1,I)) `1 <= p `1 ) assume that A1: p in L~ h and A2: 1 <= I and A3: I <= width (GoB h) ; ::_thesis: ((GoB h) * (1,I)) `1 <= p `1 consider i being Element of NAT such that A4: 1 <= i and A5: i + 1 <= len h and A6: p in LSeg ((h /. i),(h /. (i + 1))) by A1, SPPOL_2:14; i <= i + 1 by NAT_1:11; then i <= len h by A5, XXREAL_0:2; then A7: ((GoB h) * (1,I)) `1 <= (h /. i) `1 by A2, A3, A4, Th5; 1 <= i + 1 by NAT_1:11; then A8: ((GoB h) * (1,I)) `1 <= (h /. (i + 1)) `1 by A2, A3, A5, Th5; now__::_thesis:_(_(_(h_/._i)_`1_<=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(1,I))_`1_<=_p_`1_)_or_(_(h_/._i)_`1_>_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(1,I))_`1_<=_p_`1_)_) percases ( (h /. i) `1 <= (h /. (i + 1)) `1 or (h /. i) `1 > (h /. (i + 1)) `1 ) ; case (h /. i) `1 <= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (1,I)) `1 <= p `1 then (h /. i) `1 <= p `1 by A6, TOPREAL1:3; hence ((GoB h) * (1,I)) `1 <= p `1 by A7, XXREAL_0:2; ::_thesis: verum end; case (h /. i) `1 > (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (1,I)) `1 <= p `1 then (h /. (i + 1)) `1 <= p `1 by A6, TOPREAL1:3; hence ((GoB h) * (1,I)) `1 <= p `1 by A8, XXREAL_0:2; ::_thesis: verum end; end; end; hence ((GoB h) * (1,I)) `1 <= p `1 ; ::_thesis: verum 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 Element of NAT st p in L~ h & 1 <= I & I <= width (GoB h) holds p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 proof let p be Point of (TOP-REAL 2); ::_thesis: for h being non constant standard special_circular_sequence for I being Element of NAT st p in L~ h & 1 <= I & I <= width (GoB h) holds p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 let h be non constant standard special_circular_sequence; ::_thesis: for I being Element of NAT st p in L~ h & 1 <= I & I <= width (GoB h) holds p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 let I be Element of NAT ; ::_thesis: ( p in L~ h & 1 <= I & I <= width (GoB h) implies p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 ) assume that A1: p in L~ h and A2: 1 <= I and A3: I <= width (GoB h) ; ::_thesis: p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 consider i being Element of NAT such that A4: 1 <= i and A5: i + 1 <= len h and A6: p in LSeg ((h /. i),(h /. (i + 1))) by A1, SPPOL_2:14; i <= i + 1 by NAT_1:11; then i <= len h by A5, XXREAL_0:2; then A7: ((GoB h) * ((len (GoB h)),I)) `1 >= (h /. i) `1 by A2, A3, A4, Th5; 1 <= i + 1 by NAT_1:11; then A8: ((GoB h) * ((len (GoB h)),I)) `1 >= (h /. (i + 1)) `1 by A2, A3, A5, Th5; now__::_thesis:_(_(_(h_/._i)_`1_<=_(h_/._(i_+_1))_`1_&_p_`1_<=_((GoB_h)_*_((len_(GoB_h)),I))_`1_)_or_(_(h_/._i)_`1_>_(h_/._(i_+_1))_`1_&_p_`1_<=_((GoB_h)_*_((len_(GoB_h)),I))_`1_)_) percases ( (h /. i) `1 <= (h /. (i + 1)) `1 or (h /. i) `1 > (h /. (i + 1)) `1 ) ; case (h /. i) `1 <= (h /. (i + 1)) `1 ; ::_thesis: p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 then (h /. (i + 1)) `1 >= p `1 by A6, TOPREAL1:3; hence p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 by A8, XXREAL_0:2; ::_thesis: verum end; case (h /. i) `1 > (h /. (i + 1)) `1 ; ::_thesis: p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 then (h /. i) `1 >= p `1 by A6, TOPREAL1:3; hence p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 by A7, XXREAL_0:2; ::_thesis: verum end; end; end; hence p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 ; ::_thesis: verum 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 Element of NAT st p in L~ h & 1 <= I & I <= len (GoB h) holds ((GoB h) * (I,1)) `2 <= p `2 proof let p be Point of (TOP-REAL 2); ::_thesis: for h being non constant standard special_circular_sequence for I being Element of NAT st p in L~ h & 1 <= I & I <= len (GoB h) holds ((GoB h) * (I,1)) `2 <= p `2 let h be non constant standard special_circular_sequence; ::_thesis: for I being Element of NAT st p in L~ h & 1 <= I & I <= len (GoB h) holds ((GoB h) * (I,1)) `2 <= p `2 let I be Element of NAT ; ::_thesis: ( p in L~ h & 1 <= I & I <= len (GoB h) implies ((GoB h) * (I,1)) `2 <= p `2 ) assume that A1: p in L~ h and A2: 1 <= I and A3: I <= len (GoB h) ; ::_thesis: ((GoB h) * (I,1)) `2 <= p `2 consider i being Element of NAT such that A4: 1 <= i and A5: i + 1 <= len h and A6: p in LSeg ((h /. i),(h /. (i + 1))) by A1, SPPOL_2:14; i <= i + 1 by NAT_1:11; then i <= len h by A5, XXREAL_0:2; then A7: ((GoB h) * (I,1)) `2 <= (h /. i) `2 by A2, A3, A4, Th6; 1 <= i + 1 by NAT_1:11; then A8: ((GoB h) * (I,1)) `2 <= (h /. (i + 1)) `2 by A2, A3, A5, Th6; now__::_thesis:_(_(_(h_/._i)_`2_<=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(I,1))_`2_<=_p_`2_)_or_(_(h_/._i)_`2_>_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(I,1))_`2_<=_p_`2_)_) percases ( (h /. i) `2 <= (h /. (i + 1)) `2 or (h /. i) `2 > (h /. (i + 1)) `2 ) ; case (h /. i) `2 <= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (I,1)) `2 <= p `2 then (h /. i) `2 <= p `2 by A6, TOPREAL1:4; hence ((GoB h) * (I,1)) `2 <= p `2 by A7, XXREAL_0:2; ::_thesis: verum end; case (h /. i) `2 > (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (I,1)) `2 <= p `2 then (h /. (i + 1)) `2 <= p `2 by A6, TOPREAL1:4; hence ((GoB h) * (I,1)) `2 <= p `2 by A8, XXREAL_0:2; ::_thesis: verum end; end; end; hence ((GoB h) * (I,1)) `2 <= p `2 ; ::_thesis: verum 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 Element of NAT st p in L~ h & 1 <= I & I <= len (GoB h) holds p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 proof let p be Point of (TOP-REAL 2); ::_thesis: for h being non constant standard special_circular_sequence for I being Element of NAT st p in L~ h & 1 <= I & I <= len (GoB h) holds p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 let h be non constant standard special_circular_sequence; ::_thesis: for I being Element of NAT st p in L~ h & 1 <= I & I <= len (GoB h) holds p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 let I be Element of NAT ; ::_thesis: ( p in L~ h & 1 <= I & I <= len (GoB h) implies p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 ) assume that A1: p in L~ h and A2: 1 <= I and A3: I <= len (GoB h) ; ::_thesis: p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 consider i being Element of NAT such that A4: 1 <= i and A5: i + 1 <= len h and A6: p in LSeg ((h /. i),(h /. (i + 1))) by A1, SPPOL_2:14; i <= i + 1 by NAT_1:11; then i <= len h by A5, XXREAL_0:2; then A7: ((GoB h) * (I,(width (GoB h)))) `2 >= (h /. i) `2 by A2, A3, A4, Th6; 1 <= i + 1 by NAT_1:11; then A8: ((GoB h) * (I,(width (GoB h)))) `2 >= (h /. (i + 1)) `2 by A2, A3, A5, Th6; now__::_thesis:_(_(_(h_/._i)_`2_<=_(h_/._(i_+_1))_`2_&_p_`2_<=_((GoB_h)_*_(I,(width_(GoB_h))))_`2_)_or_(_(h_/._i)_`2_>_(h_/._(i_+_1))_`2_&_p_`2_<=_((GoB_h)_*_(I,(width_(GoB_h))))_`2_)_) percases ( (h /. i) `2 <= (h /. (i + 1)) `2 or (h /. i) `2 > (h /. (i + 1)) `2 ) ; case (h /. i) `2 <= (h /. (i + 1)) `2 ; ::_thesis: p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 then (h /. (i + 1)) `2 >= p `2 by A6, TOPREAL1:4; hence p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 by A8, XXREAL_0:2; ::_thesis: verum end; case (h /. i) `2 > (h /. (i + 1)) `2 ; ::_thesis: p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 then (h /. i) `2 >= p `2 by A6, TOPREAL1:4; hence p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 by A7, XXREAL_0:2; ::_thesis: verum end; end; end; hence p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 ; ::_thesis: verum end; theorem Th35: :: JORDAN5D:35 for h being non constant standard special_circular_sequence for i, j being Element of 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 let h be non constant standard special_circular_sequence; ::_thesis: for i, j being Element of 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 ) let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i <= len (GoB h) & 1 <= j & j <= width (GoB h) implies ex q being Point of (TOP-REAL 2) st ( q `1 = ((GoB h) * (i,j)) `1 & q in L~ h ) ) assume that A1: 1 <= i and A2: i <= len (GoB h) and A3: 1 <= j and A4: j <= width (GoB h) ; ::_thesis: ex q being Point of (TOP-REAL 2) st ( q `1 = ((GoB h) * (i,j)) `1 & q in L~ h ) consider k being Element of NAT such that A5: k in dom h and [i,j] in Indices (GoB h) and A6: (h /. k) `1 = ((GoB h) * (i,j)) `1 by A1, A2, A3, A4, Th9; take q = h /. k; ::_thesis: ( q `1 = ((GoB h) * (i,j)) `1 & q in L~ h ) thus q `1 = ((GoB h) * (i,j)) `1 by A6; ::_thesis: q in L~ h 4 < len h by GOBOARD7:34; hence q in L~ h by A5, GOBOARD1:1, XXREAL_0:2; ::_thesis: verum end; theorem Th36: :: JORDAN5D:36 for h being non constant standard special_circular_sequence for i, j being Element of 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 let h be non constant standard special_circular_sequence; ::_thesis: for i, j being Element of 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 ) let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i <= len (GoB h) & 1 <= j & j <= width (GoB h) implies ex q being Point of (TOP-REAL 2) st ( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h ) ) assume that A1: 1 <= i and A2: i <= len (GoB h) and A3: 1 <= j and A4: j <= width (GoB h) ; ::_thesis: ex q being Point of (TOP-REAL 2) st ( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h ) consider k being Element of NAT such that A5: k in dom h and [i,j] in Indices (GoB h) and A6: (h /. k) `2 = ((GoB h) * (i,j)) `2 by A1, A2, A3, A4, Th10; take q = h /. k; ::_thesis: ( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h ) thus q `2 = ((GoB h) * (i,j)) `2 by A6; ::_thesis: q in L~ h 4 < len h by GOBOARD7:34; hence q in L~ h by A5, GOBOARD1:1, XXREAL_0:2; ::_thesis: verum 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 let h be non constant standard special_circular_sequence; ::_thesis: W-bound (L~ h) = ((GoB h) * (1,1)) `1 set X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } ; set A = ((GoB h) * (1,1)) `1 ; consider a being set such that A1: a in L~ h by XBOOLE_0:def_1; A2: { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } c= REAL proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } or b in REAL ) assume b in { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } ; ::_thesis: b in REAL then ex qq being Point of (TOP-REAL 2) st ( b = qq `1 & qq in L~ h ) ; hence b in REAL ; ::_thesis: verum end; reconsider a = a as Point of (TOP-REAL 2) by A1; a `1 in { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } by A1; then reconsider X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } as non empty Subset of REAL by A2; lower_bound X = ((GoB h) * (1,1)) `1 proof A3: 1 <= width (GoB h) by GOBOARD7:33; A4: for p being real number st p in X holds p >= ((GoB h) * (1,1)) `1 proof let p be real number ; ::_thesis: ( p in X implies p >= ((GoB h) * (1,1)) `1 ) assume p in X ; ::_thesis: p >= ((GoB h) * (1,1)) `1 then ex s being Point of (TOP-REAL 2) st ( p = s `1 & s in L~ h ) ; hence p >= ((GoB h) * (1,1)) `1 by A3, Th31; ::_thesis: verum end; 1 <= len (GoB h) by GOBOARD7:32; then consider q1 being Point of (TOP-REAL 2) such that A5: q1 `1 = ((GoB h) * (1,1)) `1 and A6: q1 in L~ h by A3, Th35; reconsider q11 = q1 `1 as Real ; for q being real number st ( for p being real number st p in X holds p >= q ) holds ((GoB h) * (1,1)) `1 >= q proof A7: q11 in X by A6; let q be real number ; ::_thesis: ( ( for p being real number st p in X holds p >= q ) implies ((GoB h) * (1,1)) `1 >= q ) assume for p being real number st p in X holds p >= q ; ::_thesis: ((GoB h) * (1,1)) `1 >= q hence ((GoB h) * (1,1)) `1 >= q by A5, A7; ::_thesis: verum end; hence lower_bound X = ((GoB h) * (1,1)) `1 by A4, SEQ_4:44; ::_thesis: verum end; hence W-bound (L~ h) = ((GoB h) * (1,1)) `1 by Th17; ::_thesis: verum 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 let h be non constant standard special_circular_sequence; ::_thesis: S-bound (L~ h) = ((GoB h) * (1,1)) `2 set X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } ; set A = ((GoB h) * (1,1)) `2 ; consider a being set such that A1: a in L~ h by XBOOLE_0:def_1; A2: { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } c= REAL proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } or b in REAL ) assume b in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } ; ::_thesis: b in REAL then ex qq being Point of (TOP-REAL 2) st ( b = qq `2 & qq in L~ h ) ; hence b in REAL ; ::_thesis: verum end; reconsider a = a as Point of (TOP-REAL 2) by A1; a `2 in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } by A1; then reconsider X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } as non empty Subset of REAL by A2; lower_bound X = ((GoB h) * (1,1)) `2 proof A3: 1 <= len (GoB h) by GOBOARD7:32; A4: for p being real number st p in X holds p >= ((GoB h) * (1,1)) `2 proof let p be real number ; ::_thesis: ( p in X implies p >= ((GoB h) * (1,1)) `2 ) assume p in X ; ::_thesis: p >= ((GoB h) * (1,1)) `2 then ex s being Point of (TOP-REAL 2) st ( p = s `2 & s in L~ h ) ; hence p >= ((GoB h) * (1,1)) `2 by A3, Th33; ::_thesis: verum end; 1 <= width (GoB h) by GOBOARD7:33; then consider q1 being Point of (TOP-REAL 2) such that A5: q1 `2 = ((GoB h) * (1,1)) `2 and A6: q1 in L~ h by A3, Th36; reconsider q11 = q1 `2 as Real ; for q being real number st ( for p being real number st p in X holds p >= q ) holds ((GoB h) * (1,1)) `2 >= q proof A7: q11 in X by A6; let q be real number ; ::_thesis: ( ( for p being real number st p in X holds p >= q ) implies ((GoB h) * (1,1)) `2 >= q ) assume for p being real number st p in X holds p >= q ; ::_thesis: ((GoB h) * (1,1)) `2 >= q hence ((GoB h) * (1,1)) `2 >= q by A5, A7; ::_thesis: verum end; hence lower_bound X = ((GoB h) * (1,1)) `2 by A4, SEQ_4:44; ::_thesis: verum end; hence S-bound (L~ h) = ((GoB h) * (1,1)) `2 by Th18; ::_thesis: verum 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 let h be non constant standard special_circular_sequence; ::_thesis: E-bound (L~ h) = ((GoB h) * ((len (GoB h)),1)) `1 set X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } ; set A = ((GoB h) * ((len (GoB h)),1)) `1 ; consider a being set such that A1: a in L~ h by XBOOLE_0:def_1; A2: { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } c= REAL proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } or b in REAL ) assume b in { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } ; ::_thesis: b in REAL then ex qq being Point of (TOP-REAL 2) st ( b = qq `1 & qq in L~ h ) ; hence b in REAL ; ::_thesis: verum end; reconsider a = a as Point of (TOP-REAL 2) by A1; a `1 in { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } by A1; then reconsider X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ h } as non empty Subset of REAL by A2; upper_bound X = ((GoB h) * ((len (GoB h)),1)) `1 proof A3: for p being real number st p in X holds p <= ((GoB h) * ((len (GoB h)),1)) `1 proof let p be real number ; ::_thesis: ( p in X implies p <= ((GoB h) * ((len (GoB h)),1)) `1 ) assume p in X ; ::_thesis: p <= ((GoB h) * ((len (GoB h)),1)) `1 then A4: ex s being Point of (TOP-REAL 2) st ( p = s `1 & s in L~ h ) ; 1 <= width (GoB h) by GOBOARD7:33; hence p <= ((GoB h) * ((len (GoB h)),1)) `1 by A4, Th32; ::_thesis: verum end; A5: 1 <= width (GoB h) by GOBOARD7:33; 1 <= len (GoB h) by GOBOARD7:32; then consider q1 being Point of (TOP-REAL 2) such that A6: q1 `1 = ((GoB h) * ((len (GoB h)),1)) `1 and A7: q1 in L~ h by A5, Th35; reconsider q11 = q1 `1 as Real ; for q being real number st ( for p being real number st p in X holds p <= q ) holds ((GoB h) * ((len (GoB h)),1)) `1 <= q proof A8: q11 in X by A7; let q be real number ; ::_thesis: ( ( for p being real number st p in X holds p <= q ) implies ((GoB h) * ((len (GoB h)),1)) `1 <= q ) assume for p being real number st p in X holds p <= q ; ::_thesis: ((GoB h) * ((len (GoB h)),1)) `1 <= q hence ((GoB h) * ((len (GoB h)),1)) `1 <= q by A6, A8; ::_thesis: verum end; hence upper_bound X = ((GoB h) * ((len (GoB h)),1)) `1 by A3, SEQ_4:46; ::_thesis: verum end; hence E-bound (L~ h) = ((GoB h) * ((len (GoB h)),1)) `1 by Th17; ::_thesis: verum 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 let h be non constant standard special_circular_sequence; ::_thesis: N-bound (L~ h) = ((GoB h) * (1,(width (GoB h)))) `2 set X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } ; set A = ((GoB h) * (1,(width (GoB h)))) `2 ; consider a being set such that A1: a in L~ h by XBOOLE_0:def_1; A2: { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } c= REAL proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } or b in REAL ) assume b in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } ; ::_thesis: b in REAL then ex qq being Point of (TOP-REAL 2) st ( b = qq `2 & qq in L~ h ) ; hence b in REAL ; ::_thesis: verum end; reconsider a = a as Point of (TOP-REAL 2) by A1; a `2 in { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } by A1; then reconsider X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ h } as non empty Subset of REAL by A2; upper_bound X = ((GoB h) * (1,(width (GoB h)))) `2 proof A3: 1 <= len (GoB h) by GOBOARD7:32; A4: for p being real number st p in X holds p <= ((GoB h) * (1,(width (GoB h)))) `2 proof let p be real number ; ::_thesis: ( p in X implies p <= ((GoB h) * (1,(width (GoB h)))) `2 ) assume p in X ; ::_thesis: p <= ((GoB h) * (1,(width (GoB h)))) `2 then ex s being Point of (TOP-REAL 2) st ( p = s `2 & s in L~ h ) ; hence p <= ((GoB h) * (1,(width (GoB h)))) `2 by A3, Th34; ::_thesis: verum end; 1 <= width (GoB h) by GOBOARD7:33; then consider q1 being Point of (TOP-REAL 2) such that A5: q1 `2 = ((GoB h) * (1,(width (GoB h)))) `2 and A6: q1 in L~ h by A3, Th36; reconsider q11 = q1 `2 as Real ; for q being real number st ( for p being real number st p in X holds p <= q ) holds ((GoB h) * (1,(width (GoB h)))) `2 <= q proof A7: q11 in X by A6; let q be real number ; ::_thesis: ( ( for p being real number st p in X holds p <= q ) implies ((GoB h) * (1,(width (GoB h)))) `2 <= q ) assume for p being real number st p in X holds p <= q ; ::_thesis: ((GoB h) * (1,(width (GoB h)))) `2 <= q hence ((GoB h) * (1,(width (GoB h)))) `2 <= q by A5, A7; ::_thesis: verum end; hence upper_bound X = ((GoB h) * (1,(width (GoB h)))) `2 by A4, SEQ_4:46; ::_thesis: verum end; hence N-bound (L~ h) = ((GoB h) * (1,(width (GoB h)))) `2 by Th18; ::_thesis: verum end; theorem Th41: :: JORDAN5D:41 for f being non empty FinSequence of (TOP-REAL 2) for i, I, i1 being Element of 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 Element of 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 let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for i, I, i1 being Element of 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 Element of 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 let i, I, i1 be Element of NAT ; ::_thesis: 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 Element of 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 let Y be non empty finite Subset of NAT; ::_thesis: ( 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 Element of NAT st ( k in dom f & f /. k = (GoB f) * (I,j) ) ) } & (f /. i) `1 = ((GoB f) * (I,1)) `1 & i1 = min Y implies ((GoB f) * (I,i1)) `2 <= (f /. i) `2 ) A1: f /. i = |[((f /. i) `1),((f /. i) `2)]| by EUCLID:53; assume A2: ( 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 Element of NAT st ( k in dom f & f /. k = (GoB f) * (I,j) ) ) } & (f /. i) `1 = ((GoB f) * (I,1)) `1 & i1 = min Y ) ; ::_thesis: ((GoB f) * (I,i1)) `2 <= (f /. i) `2 then A3: i in dom f by FINSEQ_3:25; then consider i2, j2 being Element of NAT such that A4: [i2,j2] in Indices (GoB f) and A5: f /. i = (GoB f) * (i2,j2) by GOBOARD5:11; A6: j2 <= width (GoB f) by A4, MATRIX_1:38; A7: 1 <= j2 by A4, MATRIX_1:38; then A8: [I,j2] in Indices (GoB f) by A2, A6, MATRIX_1:36; A9: i2 <= len (GoB f) by A4, MATRIX_1:38; 1 <= i2 by A4, MATRIX_1:38; then A10: (f /. i) `2 = ((GoB f) * (1,j2)) `2 by A5, A9, A7, A6, GOBOARD5:1 .= ((GoB f) * (I,j2)) `2 by A2, A7, A6, GOBOARD5:1 ; i1 in Y by A2, XXREAL_2:def_7; then ex j being Element of NAT st ( i1 = j & [I,j] in Indices (GoB f) & ex k being Element of NAT st ( k in dom f & f /. k = (GoB f) * (I,j) ) ) by A2; then A11: 1 <= i1 by MATRIX_1:38; (f /. i) `1 = ((GoB f) * (I,j2)) `1 by A2, A7, A6, GOBOARD5:2; then f /. i = (GoB f) * (I,j2) by A10, A1, EUCLID:53; then j2 in Y by A2, A3, A8; then A12: i1 <= j2 by A2, XXREAL_2:def_7; A13: j2 <= width (GoB f) by A4, MATRIX_1:38; now__::_thesis:_(_(_i1_<_j2_&_((GoB_f)_*_(I,i1))_`2_<=_((GoB_f)_*_(I,j2))_`2_)_or_(_i1_>=_j2_&_((GoB_f)_*_(I,i1))_`2_<=_((GoB_f)_*_(I,j2))_`2_)_) percases ( i1 < j2 or i1 >= j2 ) ; case i1 < j2 ; ::_thesis: ((GoB f) * (I,i1)) `2 <= ((GoB f) * (I,j2)) `2 hence ((GoB f) * (I,i1)) `2 <= ((GoB f) * (I,j2)) `2 by A2, A11, A13, GOBOARD5:4; ::_thesis: verum end; case i1 >= j2 ; ::_thesis: ((GoB f) * (I,i1)) `2 <= ((GoB f) * (I,j2)) `2 hence ((GoB f) * (I,i1)) `2 <= ((GoB f) * (I,j2)) `2 by A12, XXREAL_0:1; ::_thesis: verum end; end; end; hence ((GoB f) * (I,i1)) `2 <= (f /. i) `2 by A10; ::_thesis: verum end; theorem Th42: :: JORDAN5D:42 for h being non constant standard special_circular_sequence for i, I, i1 being Element of 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 Element of 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 let h be non constant standard special_circular_sequence; ::_thesis: for i, I, i1 being Element of 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 Element of 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 let i, I, i1 be Element of NAT ; ::_thesis: 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 Element of 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 let Y be non empty finite Subset of NAT; ::_thesis: ( 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 Element of NAT st ( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = min Y implies ((GoB h) * (i1,I)) `1 <= (h /. i) `1 ) A1: h /. i = |[((h /. i) `1),((h /. i) `2)]| by EUCLID:53; assume A2: ( 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 Element of NAT st ( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = min Y ) ; ::_thesis: ((GoB h) * (i1,I)) `1 <= (h /. i) `1 then A3: i in dom h by FINSEQ_3:25; then consider i2, j2 being Element of NAT such that A4: [i2,j2] in Indices (GoB h) and A5: h /. i = (GoB h) * (i2,j2) by GOBOARD5:11; A6: i2 <= len (GoB h) by A4, MATRIX_1:38; A7: 1 <= i2 by A4, MATRIX_1:38; then A8: [i2,I] in Indices (GoB h) by A2, A6, MATRIX_1:36; A9: j2 <= width (GoB h) by A4, MATRIX_1:38; 1 <= j2 by A4, MATRIX_1:38; then A10: (h /. i) `1 = ((GoB h) * (i2,1)) `1 by A5, A7, A6, A9, GOBOARD5:2 .= ((GoB h) * (i2,I)) `1 by A2, A7, A6, GOBOARD5:2 ; i1 in Y by A2, XXREAL_2:def_7; then ex j being Element of NAT st ( i1 = j & [j,I] in Indices (GoB h) & ex k being Element of NAT st ( k in dom h & h /. k = (GoB h) * (j,I) ) ) by A2; then A11: 1 <= i1 by MATRIX_1:38; (h /. i) `2 = ((GoB h) * (i2,I)) `2 by A2, A7, A6, GOBOARD5:1; then h /. i = (GoB h) * (i2,I) by A10, A1, EUCLID:53; then i2 in Y by A2, A3, A8; then A12: i1 <= i2 by A2, XXREAL_2:def_7; A13: i2 <= len (GoB h) by A4, MATRIX_1:38; now__::_thesis:_(_(_i1_<_i2_&_((GoB_h)_*_(i1,I))_`1_<=_((GoB_h)_*_(i2,I))_`1_)_or_(_i1_>=_i2_&_((GoB_h)_*_(i1,I))_`1_<=_((GoB_h)_*_(i2,I))_`1_)_) percases ( i1 < i2 or i1 >= i2 ) ; case i1 < i2 ; ::_thesis: ((GoB h) * (i1,I)) `1 <= ((GoB h) * (i2,I)) `1 hence ((GoB h) * (i1,I)) `1 <= ((GoB h) * (i2,I)) `1 by A2, A11, A13, GOBOARD5:3; ::_thesis: verum end; case i1 >= i2 ; ::_thesis: ((GoB h) * (i1,I)) `1 <= ((GoB h) * (i2,I)) `1 hence ((GoB h) * (i1,I)) `1 <= ((GoB h) * (i2,I)) `1 by A12, XXREAL_0:1; ::_thesis: verum end; end; end; hence ((GoB h) * (i1,I)) `1 <= (h /. i) `1 by A10; ::_thesis: verum end; theorem Th43: :: JORDAN5D:43 for h being non constant standard special_circular_sequence for i, I, i1 being Element of 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 Element of 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 let h be non constant standard special_circular_sequence; ::_thesis: for i, I, i1 being Element of 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 Element of 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 let i, I, i1 be Element of NAT ; ::_thesis: 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 Element of 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 let Y be non empty finite Subset of NAT; ::_thesis: ( 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 Element of NAT st ( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = max Y implies ((GoB h) * (i1,I)) `1 >= (h /. i) `1 ) A1: h /. i = |[((h /. i) `1),((h /. i) `2)]| by EUCLID:53; assume A2: ( 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 Element of NAT st ( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = max Y ) ; ::_thesis: ((GoB h) * (i1,I)) `1 >= (h /. i) `1 then A3: i in dom h by FINSEQ_3:25; then consider i2, j2 being Element of NAT such that A4: [i2,j2] in Indices (GoB h) and A5: h /. i = (GoB h) * (i2,j2) by GOBOARD5:11; A6: 1 <= i2 by A4, MATRIX_1:38; A7: i2 <= len (GoB h) by A4, MATRIX_1:38; then A8: [i2,I] in Indices (GoB h) by A2, A6, MATRIX_1:36; A9: j2 <= width (GoB h) by A4, MATRIX_1:38; 1 <= j2 by A4, MATRIX_1:38; then A10: (h /. i) `1 = ((GoB h) * (i2,1)) `1 by A5, A6, A7, A9, GOBOARD5:2 .= ((GoB h) * (i2,I)) `1 by A2, A6, A7, GOBOARD5:2 ; i1 in Y by A2, XXREAL_2:def_8; then ex j being Element of NAT st ( i1 = j & [j,I] in Indices (GoB h) & ex k being Element of NAT st ( k in dom h & h /. k = (GoB h) * (j,I) ) ) by A2; then A11: i1 <= len (GoB h) by MATRIX_1:38; (h /. i) `2 = ((GoB h) * (i2,I)) `2 by A2, A6, A7, GOBOARD5:1; then h /. i = (GoB h) * (i2,I) by A10, A1, EUCLID:53; then i2 in Y by A2, A3, A8; then A12: i1 >= i2 by A2, XXREAL_2:def_8; now__::_thesis:_(_(_i1_>_i2_&_((GoB_h)_*_(i1,I))_`1_>=_((GoB_h)_*_(i2,I))_`1_)_or_(_i1_<=_i2_&_((GoB_h)_*_(i1,I))_`1_>=_((GoB_h)_*_(i2,I))_`1_)_) percases ( i1 > i2 or i1 <= i2 ) ; case i1 > i2 ; ::_thesis: ((GoB h) * (i1,I)) `1 >= ((GoB h) * (i2,I)) `1 hence ((GoB h) * (i1,I)) `1 >= ((GoB h) * (i2,I)) `1 by A2, A6, A11, GOBOARD5:3; ::_thesis: verum end; case i1 <= i2 ; ::_thesis: ((GoB h) * (i1,I)) `1 >= ((GoB h) * (i2,I)) `1 hence ((GoB h) * (i1,I)) `1 >= ((GoB h) * (i2,I)) `1 by A12, XXREAL_0:1; ::_thesis: verum end; end; end; hence ((GoB h) * (i1,I)) `1 >= (h /. i) `1 by A10; ::_thesis: verum end; theorem Th44: :: JORDAN5D:44 for f being non empty FinSequence of (TOP-REAL 2) for i, I, i1 being Element of 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 Element of 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 let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for i, I, i1 being Element of 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 Element of 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 let i, I, i1 be Element of NAT ; ::_thesis: 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 Element of 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 let Y be non empty finite Subset of NAT; ::_thesis: ( 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 Element of NAT st ( k in dom f & f /. k = (GoB f) * (I,j) ) ) } & (f /. i) `1 = ((GoB f) * (I,1)) `1 & i1 = max Y implies ((GoB f) * (I,i1)) `2 >= (f /. i) `2 ) A1: f /. i = |[((f /. i) `1),((f /. i) `2)]| by EUCLID:53; assume A2: ( 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 Element of NAT st ( k in dom f & f /. k = (GoB f) * (I,j) ) ) } & (f /. i) `1 = ((GoB f) * (I,1)) `1 & i1 = max Y ) ; ::_thesis: ((GoB f) * (I,i1)) `2 >= (f /. i) `2 then A3: i in dom f by FINSEQ_3:25; then consider i2, j2 being Element of NAT such that A4: [i2,j2] in Indices (GoB f) and A5: f /. i = (GoB f) * (i2,j2) by GOBOARD5:11; A6: 1 <= j2 by A4, MATRIX_1:38; A7: j2 <= width (GoB f) by A4, MATRIX_1:38; then A8: [I,j2] in Indices (GoB f) by A2, A6, MATRIX_1:36; A9: i2 <= len (GoB f) by A4, MATRIX_1:38; 1 <= i2 by A4, MATRIX_1:38; then A10: (f /. i) `2 = ((GoB f) * (1,j2)) `2 by A5, A9, A6, A7, GOBOARD5:1 .= ((GoB f) * (I,j2)) `2 by A2, A6, A7, GOBOARD5:1 ; i1 in Y by A2, XXREAL_2:def_8; then ex j being Element of NAT st ( i1 = j & [I,j] in Indices (GoB f) & ex k being Element of NAT st ( k in dom f & f /. k = (GoB f) * (I,j) ) ) by A2; then A11: i1 <= width (GoB f) by MATRIX_1:38; (f /. i) `1 = ((GoB f) * (I,j2)) `1 by A2, A6, A7, GOBOARD5:2; then f /. i = (GoB f) * (I,j2) by A10, A1, EUCLID:53; then j2 in Y by A2, A3, A8; then A12: i1 >= j2 by A2, XXREAL_2:def_8; now__::_thesis:_(_(_i1_>_j2_&_((GoB_f)_*_(I,i1))_`2_>=_((GoB_f)_*_(I,j2))_`2_)_or_(_i1_<=_j2_&_((GoB_f)_*_(I,i1))_`2_>=_((GoB_f)_*_(I,j2))_`2_)_) percases ( i1 > j2 or i1 <= j2 ) ; case i1 > j2 ; ::_thesis: ((GoB f) * (I,i1)) `2 >= ((GoB f) * (I,j2)) `2 hence ((GoB f) * (I,i1)) `2 >= ((GoB f) * (I,j2)) `2 by A2, A11, A6, GOBOARD5:4; ::_thesis: verum end; case i1 <= j2 ; ::_thesis: ((GoB f) * (I,i1)) `2 >= ((GoB f) * (I,j2)) `2 hence ((GoB f) * (I,i1)) `2 >= ((GoB f) * (I,j2)) `2 by A12, XXREAL_0:1; ::_thesis: verum end; end; end; hence ((GoB f) * (I,i1)) `2 >= (f /. i) `2 by A10; ::_thesis: verum end; Lm1: for i1 being Element of 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = min Y holds ((GoB h) * (1,i1)) `2 <= p `2 proof let i1 be Element of NAT ; ::_thesis: 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = min Y holds ((GoB h) * (1,i1)) `2 <= p `2 let p be Point of (TOP-REAL 2); ::_thesis: 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = min Y holds ((GoB h) * (1,i1)) `2 <= p `2 let Y be non empty finite Subset of NAT; ::_thesis: 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = min Y holds ((GoB h) * (1,i1)) `2 <= p `2 let h be non constant standard special_circular_sequence; ::_thesis: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = min Y implies ((GoB h) * (1,i1)) `2 <= p `2 ) A1: 1 <= len (GoB h) by GOBOARD7:32; assume A2: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = min Y ) ; ::_thesis: ((GoB h) * (1,i1)) `2 <= p `2 then consider i being Element of NAT such that A3: 1 <= i and A4: i + 1 <= len h and A5: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14; A6: 1 <= i + 1 by A3, XREAL_1:145; i <= i + 1 by NAT_1:11; then A7: i <= len h by A4, XXREAL_0:2; A8: p `1 = ((GoB h) * (1,1)) `1 by A2, Th37; A9: 1 <= width (GoB h) by GOBOARD7:33; now__::_thesis:_(_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_(1,i1))_`2_<=_p_`2_)_or_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_(1,i1))_`2_<=_p_`2_)_) percases ( LSeg (h,i) is vertical or LSeg (h,i) is horizontal ) by SPPOL_1:19; case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * (1,i1)) `2 <= p `2 then LSeg ((h /. i),(h /. (i + 1))) is vertical by A3, A4, TOPREAL1:def_3; then A10: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16; then A11: p `1 = (h /. i) `1 by A5, GOBOARD7:5; A12: p `1 = (h /. (i + 1)) `1 by A5, A10, GOBOARD7:5; now__::_thesis:_(_(_(h_/._i)_`2_<=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(1,i1))_`2_<=_p_`2_)_or_(_(h_/._i)_`2_>_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(1,i1))_`2_<=_p_`2_)_) percases ( (h /. i) `2 <= (h /. (i + 1)) `2 or (h /. i) `2 > (h /. (i + 1)) `2 ) ; case (h /. i) `2 <= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (1,i1)) `2 <= p `2 then A13: (h /. i) `2 <= p `2 by A5, TOPREAL1:4; ((GoB h) * (1,i1)) `2 <= (h /. i) `2 by A2, A8, A1, A3, A7, A11, Th41; hence ((GoB h) * (1,i1)) `2 <= p `2 by A13, XXREAL_0:2; ::_thesis: verum end; case (h /. i) `2 > (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (1,i1)) `2 <= p `2 then A14: (h /. (i + 1)) `2 <= p `2 by A5, TOPREAL1:4; ((GoB h) * (1,i1)) `2 <= (h /. (i + 1)) `2 by A2, A8, A1, A4, A6, A12, Th41; hence ((GoB h) * (1,i1)) `2 <= p `2 by A14, XXREAL_0:2; ::_thesis: verum end; end; end; hence ((GoB h) * (1,i1)) `2 <= p `2 ; ::_thesis: verum end; case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * (1,i1)) `2 <= p `2 then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A3, A4, TOPREAL1:def_3; then A15: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15; then A16: p `2 = (h /. i) `2 by A5, GOBOARD7:6; A17: p `2 = (h /. (i + 1)) `2 by A5, A15, GOBOARD7:6; now__::_thesis:_(_(_(h_/._i)_`1_<=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(1,i1))_`2_<=_p_`2_)_or_(_(h_/._i)_`1_>_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(1,i1))_`2_<=_p_`2_)_) percases ( (h /. i) `1 <= (h /. (i + 1)) `1 or (h /. i) `1 > (h /. (i + 1)) `1 ) ; case (h /. i) `1 <= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (1,i1)) `2 <= p `2 then A18: (h /. i) `1 <= ((GoB h) * (1,1)) `1 by A8, A5, TOPREAL1:3; (h /. i) `1 >= ((GoB h) * (1,1)) `1 by A9, A3, A7, Th5; then (h /. i) `1 = ((GoB h) * (1,1)) `1 by A18, XXREAL_0:1; hence ((GoB h) * (1,i1)) `2 <= p `2 by A2, A1, A3, A7, A16, Th41; ::_thesis: verum end; case (h /. i) `1 > (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (1,i1)) `2 <= p `2 then A19: (h /. (i + 1)) `1 <= ((GoB h) * (1,1)) `1 by A8, A5, TOPREAL1:3; (h /. (i + 1)) `1 >= ((GoB h) * (1,1)) `1 by A9, A4, A6, Th5; then (h /. (i + 1)) `1 = ((GoB h) * (1,1)) `1 by A19, XXREAL_0:1; hence ((GoB h) * (1,i1)) `2 <= p `2 by A2, A1, A4, A6, A17, Th41; ::_thesis: verum end; end; end; hence ((GoB h) * (1,i1)) `2 <= p `2 ; ::_thesis: verum end; end; end; hence ((GoB h) * (1,i1)) `2 <= p `2 ; ::_thesis: verum end; Lm2: for i1 being Element of 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = max Y holds ((GoB h) * (1,i1)) `2 >= p `2 proof let i1 be Element of NAT ; ::_thesis: 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = max Y holds ((GoB h) * (1,i1)) `2 >= p `2 let p be Point of (TOP-REAL 2); ::_thesis: 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = max Y holds ((GoB h) * (1,i1)) `2 >= p `2 let Y be non empty finite Subset of NAT; ::_thesis: 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = max Y holds ((GoB h) * (1,i1)) `2 >= p `2 let h be non constant standard special_circular_sequence; ::_thesis: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = max Y implies ((GoB h) * (1,i1)) `2 >= p `2 ) A1: 1 <= len (GoB h) by GOBOARD7:32; assume A2: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = max Y ) ; ::_thesis: ((GoB h) * (1,i1)) `2 >= p `2 then consider i being Element of NAT such that A3: 1 <= i and A4: i + 1 <= len h and A5: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14; A6: 1 <= i + 1 by A3, XREAL_1:145; i <= i + 1 by NAT_1:11; then A7: i <= len h by A4, XXREAL_0:2; A8: p `1 = ((GoB h) * (1,1)) `1 by A2, Th37; A9: 1 <= width (GoB h) by GOBOARD7:33; now__::_thesis:_(_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_(1,i1))_`2_>=_p_`2_)_or_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_(1,i1))_`2_>=_p_`2_)_) percases ( LSeg (h,i) is vertical or LSeg (h,i) is horizontal ) by SPPOL_1:19; case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * (1,i1)) `2 >= p `2 then LSeg ((h /. i),(h /. (i + 1))) is vertical by A3, A4, TOPREAL1:def_3; then A10: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16; then A11: p `1 = (h /. i) `1 by A5, GOBOARD7:5; A12: p `1 = (h /. (i + 1)) `1 by A5, A10, GOBOARD7:5; now__::_thesis:_(_(_(h_/._i)_`2_>=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(1,i1))_`2_>=_p_`2_)_or_(_(h_/._i)_`2_<_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(1,i1))_`2_>=_p_`2_)_) percases ( (h /. i) `2 >= (h /. (i + 1)) `2 or (h /. i) `2 < (h /. (i + 1)) `2 ) ; case (h /. i) `2 >= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (1,i1)) `2 >= p `2 then A13: (h /. i) `2 >= p `2 by A5, TOPREAL1:4; ((GoB h) * (1,i1)) `2 >= (h /. i) `2 by A2, A8, A3, A1, A7, A11, Th44; hence ((GoB h) * (1,i1)) `2 >= p `2 by A13, XXREAL_0:2; ::_thesis: verum end; case (h /. i) `2 < (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (1,i1)) `2 >= p `2 then A14: (h /. (i + 1)) `2 >= p `2 by A5, TOPREAL1:4; ((GoB h) * (1,i1)) `2 >= (h /. (i + 1)) `2 by A2, A8, A4, A1, A6, A12, Th44; hence ((GoB h) * (1,i1)) `2 >= p `2 by A14, XXREAL_0:2; ::_thesis: verum end; end; end; hence ((GoB h) * (1,i1)) `2 >= p `2 ; ::_thesis: verum end; case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * (1,i1)) `2 >= p `2 then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A3, A4, TOPREAL1:def_3; then A15: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15; then A16: p `2 = (h /. i) `2 by A5, GOBOARD7:6; A17: p `2 = (h /. (i + 1)) `2 by A5, A15, GOBOARD7:6; now__::_thesis:_(_(_(h_/._i)_`1_<=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(1,i1))_`2_>=_p_`2_)_or_(_(h_/._i)_`1_>_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(1,i1))_`2_>=_p_`2_)_) percases ( (h /. i) `1 <= (h /. (i + 1)) `1 or (h /. i) `1 > (h /. (i + 1)) `1 ) ; case (h /. i) `1 <= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (1,i1)) `2 >= p `2 then A18: (h /. i) `1 <= ((GoB h) * (1,1)) `1 by A8, A5, TOPREAL1:3; (h /. i) `1 >= ((GoB h) * (1,1)) `1 by A3, A9, A7, Th5; then (h /. i) `1 = ((GoB h) * (1,1)) `1 by A18, XXREAL_0:1; hence ((GoB h) * (1,i1)) `2 >= p `2 by A2, A3, A1, A7, A16, Th44; ::_thesis: verum end; case (h /. i) `1 > (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (1,i1)) `2 >= p `2 then A19: (h /. (i + 1)) `1 <= ((GoB h) * (1,1)) `1 by A8, A5, TOPREAL1:3; (h /. (i + 1)) `1 >= ((GoB h) * (1,1)) `1 by A4, A9, A6, Th5; then (h /. (i + 1)) `1 = ((GoB h) * (1,1)) `1 by A19, XXREAL_0:1; hence ((GoB h) * (1,i1)) `2 >= p `2 by A2, A4, A1, A6, A17, Th44; ::_thesis: verum end; end; end; hence ((GoB h) * (1,i1)) `2 >= p `2 ; ::_thesis: verum end; end; end; hence ((GoB h) * (1,i1)) `2 >= p `2 ; ::_thesis: verum end; Lm3: for i1 being Element of 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 Element of 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 let i1 be Element of NAT ; ::_thesis: 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 Element of 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 let p be Point of (TOP-REAL 2); ::_thesis: 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 Element of 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 let Y be non empty finite Subset of NAT; ::_thesis: 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 Element of 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 let h be non constant standard special_circular_sequence; ::_thesis: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = min Y implies ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 ) A1: 1 <= len (GoB h) by GOBOARD7:32; assume A2: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = min Y ) ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 then consider i being Element of NAT such that A3: 1 <= i and A4: i + 1 <= len h and A5: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14; A6: 1 <= i + 1 by A3, XREAL_1:145; i <= i + 1 by NAT_1:11; then A7: i <= len h by A4, XXREAL_0:2; A8: p `1 = ((GoB h) * ((len (GoB h)),1)) `1 by A2, Th39; A9: 1 <= width (GoB h) by GOBOARD7:33; now__::_thesis:_(_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_<=_p_`2_)_or_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_<=_p_`2_)_) percases ( LSeg (h,i) is vertical or LSeg (h,i) is horizontal ) by SPPOL_1:19; case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 then LSeg ((h /. i),(h /. (i + 1))) is vertical by A3, A4, TOPREAL1:def_3; then A10: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16; then A11: p `1 = (h /. i) `1 by A5, GOBOARD7:5; A12: p `1 = (h /. (i + 1)) `1 by A5, A10, GOBOARD7:5; now__::_thesis:_(_(_(h_/._i)_`2_<=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_<=_p_`2_)_or_(_(h_/._i)_`2_>_(h_/._(i_+_1))_`2_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_<=_p_`2_)_) percases ( (h /. i) `2 <= (h /. (i + 1)) `2 or (h /. i) `2 > (h /. (i + 1)) `2 ) ; case (h /. i) `2 <= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 then A13: (h /. i) `2 <= p `2 by A5, TOPREAL1:4; ((GoB h) * ((len (GoB h)),i1)) `2 <= (h /. i) `2 by A2, A8, A3, A7, A1, A11, Th41; hence ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 by A13, XXREAL_0:2; ::_thesis: verum end; case (h /. i) `2 > (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 then A14: (h /. (i + 1)) `2 <= p `2 by A5, TOPREAL1:4; ((GoB h) * ((len (GoB h)),i1)) `2 <= (h /. (i + 1)) `2 by A2, A8, A4, A6, A1, A12, Th41; hence ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 by A14, XXREAL_0:2; ::_thesis: verum end; end; end; hence ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 ; ::_thesis: verum end; case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A3, A4, TOPREAL1:def_3; then A15: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15; then A16: p `2 = (h /. i) `2 by A5, GOBOARD7:6; A17: p `2 = (h /. (i + 1)) `2 by A5, A15, GOBOARD7:6; now__::_thesis:_(_(_(h_/._i)_`1_>=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_<=_p_`2_)_or_(_(h_/._i)_`1_<_(h_/._(i_+_1))_`1_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_<=_p_`2_)_) percases ( (h /. i) `1 >= (h /. (i + 1)) `1 or (h /. i) `1 < (h /. (i + 1)) `1 ) ; case (h /. i) `1 >= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 then A18: (h /. i) `1 >= ((GoB h) * ((len (GoB h)),1)) `1 by A8, A5, TOPREAL1:3; (h /. i) `1 <= ((GoB h) * ((len (GoB h)),1)) `1 by A9, A3, A7, Th5; then (h /. i) `1 = ((GoB h) * ((len (GoB h)),1)) `1 by A18, XXREAL_0:1; hence ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 by A2, A3, A7, A1, A16, Th41; ::_thesis: verum end; case (h /. i) `1 < (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 then A19: (h /. (i + 1)) `1 >= ((GoB h) * ((len (GoB h)),1)) `1 by A8, A5, TOPREAL1:3; (h /. (i + 1)) `1 <= ((GoB h) * ((len (GoB h)),1)) `1 by A9, A4, A6, Th5; then (h /. (i + 1)) `1 = ((GoB h) * ((len (GoB h)),1)) `1 by A19, XXREAL_0:1; hence ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 by A2, A4, A6, A1, A17, Th41; ::_thesis: verum end; end; end; hence ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 ; ::_thesis: verum end; end; end; hence ((GoB h) * ((len (GoB h)),i1)) `2 <= p `2 ; ::_thesis: verum end; Lm4: for i1 being Element of 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 Element of 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 let i1 be Element of NAT ; ::_thesis: 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 Element of 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 let p be Point of (TOP-REAL 2); ::_thesis: 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 Element of 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 let Y be non empty finite Subset of NAT; ::_thesis: 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 Element of 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 let h be non constant standard special_circular_sequence; ::_thesis: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = max Y implies ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 ) A1: 1 <= len (GoB h) by GOBOARD7:32; assume A2: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = max Y ) ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 then consider i being Element of NAT such that A3: 1 <= i and A4: i + 1 <= len h and A5: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14; A6: 1 <= i + 1 by A3, XREAL_1:145; i <= i + 1 by NAT_1:11; then A7: i <= len h by A4, XXREAL_0:2; A8: p `1 = ((GoB h) * ((len (GoB h)),1)) `1 by A2, Th39; A9: 1 <= width (GoB h) by GOBOARD7:33; now__::_thesis:_(_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_>=_p_`2_)_or_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_>=_p_`2_)_) percases ( LSeg (h,i) is vertical or LSeg (h,i) is horizontal ) by SPPOL_1:19; case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 then LSeg ((h /. i),(h /. (i + 1))) is vertical by A3, A4, TOPREAL1:def_3; then A10: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16; then A11: p `1 = (h /. i) `1 by A5, GOBOARD7:5; A12: p `1 = (h /. (i + 1)) `1 by A5, A10, GOBOARD7:5; now__::_thesis:_(_(_(h_/._i)_`2_>=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_>=_p_`2_)_or_(_(h_/._i)_`2_<_(h_/._(i_+_1))_`2_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_>=_p_`2_)_) percases ( (h /. i) `2 >= (h /. (i + 1)) `2 or (h /. i) `2 < (h /. (i + 1)) `2 ) ; case (h /. i) `2 >= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 then A13: (h /. i) `2 >= p `2 by A5, TOPREAL1:4; ((GoB h) * ((len (GoB h)),i1)) `2 >= (h /. i) `2 by A2, A8, A1, A3, A7, A11, Th44; hence ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 by A13, XXREAL_0:2; ::_thesis: verum end; case (h /. i) `2 < (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 then A14: (h /. (i + 1)) `2 >= p `2 by A5, TOPREAL1:4; ((GoB h) * ((len (GoB h)),i1)) `2 >= (h /. (i + 1)) `2 by A2, A8, A1, A4, A6, A12, Th44; hence ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 by A14, XXREAL_0:2; ::_thesis: verum end; end; end; hence ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 ; ::_thesis: verum end; case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A3, A4, TOPREAL1:def_3; then A15: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15; then A16: p `2 = (h /. i) `2 by A5, GOBOARD7:6; A17: p `2 = (h /. (i + 1)) `2 by A5, A15, GOBOARD7:6; now__::_thesis:_(_(_(h_/._i)_`1_>=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_>=_p_`2_)_or_(_(h_/._i)_`1_<_(h_/._(i_+_1))_`1_&_((GoB_h)_*_((len_(GoB_h)),i1))_`2_>=_p_`2_)_) percases ( (h /. i) `1 >= (h /. (i + 1)) `1 or (h /. i) `1 < (h /. (i + 1)) `1 ) ; case (h /. i) `1 >= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 then A18: (h /. i) `1 >= ((GoB h) * ((len (GoB h)),1)) `1 by A8, A5, TOPREAL1:3; (h /. i) `1 <= ((GoB h) * ((len (GoB h)),1)) `1 by A9, A3, A7, Th5; then (h /. i) `1 = ((GoB h) * ((len (GoB h)),1)) `1 by A18, XXREAL_0:1; hence ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 by A2, A1, A3, A7, A16, Th44; ::_thesis: verum end; case (h /. i) `1 < (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 then A19: (h /. (i + 1)) `1 >= ((GoB h) * ((len (GoB h)),1)) `1 by A8, A5, TOPREAL1:3; (h /. (i + 1)) `1 <= ((GoB h) * ((len (GoB h)),1)) `1 by A9, A4, A6, Th5; then (h /. (i + 1)) `1 = ((GoB h) * ((len (GoB h)),1)) `1 by A19, XXREAL_0:1; hence ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 by A2, A1, A4, A6, A17, Th44; ::_thesis: verum end; end; end; hence ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 ; ::_thesis: verum end; end; end; hence ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 ; ::_thesis: verum end; Lm5: for i1 being Element of 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = min Y holds ((GoB h) * (i1,1)) `1 <= p `1 proof let i1 be Element of NAT ; ::_thesis: 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = min Y holds ((GoB h) * (i1,1)) `1 <= p `1 let p be Point of (TOP-REAL 2); ::_thesis: 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = min Y holds ((GoB h) * (i1,1)) `1 <= p `1 let Y be non empty finite Subset of NAT; ::_thesis: 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = min Y holds ((GoB h) * (i1,1)) `1 <= p `1 let h be non constant standard special_circular_sequence; ::_thesis: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = min Y implies ((GoB h) * (i1,1)) `1 <= p `1 ) A1: 1 <= width (GoB h) by GOBOARD7:33; assume A2: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = min Y ) ; ::_thesis: ((GoB h) * (i1,1)) `1 <= p `1 then consider i being Element of NAT such that A3: 1 <= i and A4: i + 1 <= len h and A5: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14; A6: 1 <= i + 1 by A3, XREAL_1:145; i <= i + 1 by NAT_1:11; then A7: i <= len h by A4, XXREAL_0:2; A8: p `2 = ((GoB h) * (1,1)) `2 by A2, Th38; A9: 1 <= len (GoB h) by GOBOARD7:32; now__::_thesis:_(_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_(i1,1))_`1_<=_p_`1_)_or_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_(i1,1))_`1_<=_p_`1_)_) percases ( LSeg (h,i) is horizontal or LSeg (h,i) is vertical ) by SPPOL_1:19; case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * (i1,1)) `1 <= p `1 then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A3, A4, TOPREAL1:def_3; then A10: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15; then A11: p `2 = (h /. i) `2 by A5, GOBOARD7:6; A12: p `2 = (h /. (i + 1)) `2 by A5, A10, GOBOARD7:6; now__::_thesis:_(_(_(h_/._i)_`1_<=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,1))_`1_<=_p_`1_)_or_(_(h_/._i)_`1_>_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,1))_`1_<=_p_`1_)_) percases ( (h /. i) `1 <= (h /. (i + 1)) `1 or (h /. i) `1 > (h /. (i + 1)) `1 ) ; case (h /. i) `1 <= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,1)) `1 <= p `1 then A13: (h /. i) `1 <= p `1 by A5, TOPREAL1:3; ((GoB h) * (i1,1)) `1 <= (h /. i) `1 by A2, A8, A3, A7, A1, A11, Th42; hence ((GoB h) * (i1,1)) `1 <= p `1 by A13, XXREAL_0:2; ::_thesis: verum end; case (h /. i) `1 > (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,1)) `1 <= p `1 then A14: (h /. (i + 1)) `1 <= p `1 by A5, TOPREAL1:3; ((GoB h) * (i1,1)) `1 <= (h /. (i + 1)) `1 by A2, A8, A4, A1, A6, A12, Th42; hence ((GoB h) * (i1,1)) `1 <= p `1 by A14, XXREAL_0:2; ::_thesis: verum end; end; end; hence ((GoB h) * (i1,1)) `1 <= p `1 ; ::_thesis: verum end; case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * (i1,1)) `1 <= p `1 then LSeg ((h /. i),(h /. (i + 1))) is vertical by A3, A4, TOPREAL1:def_3; then A15: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16; then A16: p `1 = (h /. i) `1 by A5, GOBOARD7:5; A17: p `1 = (h /. (i + 1)) `1 by A5, A15, GOBOARD7:5; now__::_thesis:_(_(_(h_/._i)_`2_<=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,1))_`1_<=_p_`1_)_or_(_(h_/._i)_`2_>_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,1))_`1_<=_p_`1_)_) percases ( (h /. i) `2 <= (h /. (i + 1)) `2 or (h /. i) `2 > (h /. (i + 1)) `2 ) ; case (h /. i) `2 <= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,1)) `1 <= p `1 then A18: (h /. i) `2 <= ((GoB h) * (1,1)) `2 by A8, A5, TOPREAL1:4; (h /. i) `2 >= ((GoB h) * (1,1)) `2 by A3, A7, A9, Th6; then (h /. i) `2 = ((GoB h) * (1,1)) `2 by A18, XXREAL_0:1; hence ((GoB h) * (i1,1)) `1 <= p `1 by A2, A3, A7, A1, A16, Th42; ::_thesis: verum end; case (h /. i) `2 > (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,1)) `1 <= p `1 then A19: (h /. (i + 1)) `2 <= ((GoB h) * (1,1)) `2 by A8, A5, TOPREAL1:4; (h /. (i + 1)) `2 >= ((GoB h) * (1,1)) `2 by A4, A9, A6, Th6; then (h /. (i + 1)) `2 = ((GoB h) * (1,1)) `2 by A19, XXREAL_0:1; hence ((GoB h) * (i1,1)) `1 <= p `1 by A2, A4, A1, A6, A17, Th42; ::_thesis: verum end; end; end; hence ((GoB h) * (i1,1)) `1 <= p `1 ; ::_thesis: verum end; end; end; hence ((GoB h) * (i1,1)) `1 <= p `1 ; ::_thesis: verum end; Lm6: for i1 being Element of 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 Element of 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 let i1 be Element of NAT ; ::_thesis: 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 Element of 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 let p be Point of (TOP-REAL 2); ::_thesis: 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 Element of 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 let Y be non empty finite Subset of NAT; ::_thesis: 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 Element of 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 let h be non constant standard special_circular_sequence; ::_thesis: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = min Y implies ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 ) set I = width (GoB h); A1: 1 <= width (GoB h) by GOBOARD7:33; assume A2: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = min Y ) ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 then consider i being Element of NAT such that A3: 1 <= i and A4: i + 1 <= len h and A5: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14; A6: p `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A2, Th40; i <= i + 1 by NAT_1:11; then A7: i <= len h by A4, XXREAL_0:2; A8: 1 <= i + 1 by A3, XREAL_1:145; now__::_thesis:_(_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_<=_p_`1_)_or_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_<=_p_`1_)_) percases ( LSeg (h,i) is horizontal or LSeg (h,i) is vertical ) by SPPOL_1:19; case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A3, A4, TOPREAL1:def_3; then A9: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15; then A10: p `2 = (h /. i) `2 by A5, GOBOARD7:6; A11: p `2 = (h /. (i + 1)) `2 by A5, A9, GOBOARD7:6; now__::_thesis:_(_(_(h_/._i)_`1_<=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_<=_p_`1_)_or_(_(h_/._i)_`1_>_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_<=_p_`1_)_) percases ( (h /. i) `1 <= (h /. (i + 1)) `1 or (h /. i) `1 > (h /. (i + 1)) `1 ) ; case (h /. i) `1 <= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 then A12: (h /. i) `1 <= p `1 by A5, TOPREAL1:3; ((GoB h) * (i1,(width (GoB h)))) `1 <= (h /. i) `1 by A2, A6, A1, A3, A7, A10, Th42; hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 by A12, XXREAL_0:2; ::_thesis: verum end; case (h /. i) `1 > (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 then A13: (h /. (i + 1)) `1 <= p `1 by A5, TOPREAL1:3; ((GoB h) * (i1,(width (GoB h)))) `1 <= (h /. (i + 1)) `1 by A2, A6, A1, A4, A8, A11, Th42; hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 by A13, XXREAL_0:2; ::_thesis: verum end; end; end; hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 ; ::_thesis: verum end; case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 then LSeg ((h /. i),(h /. (i + 1))) is vertical by A3, A4, TOPREAL1:def_3; then A14: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16; then A15: p `1 = (h /. i) `1 by A5, GOBOARD7:5; A16: 1 <= len (GoB h) by GOBOARD7:32; A17: p `1 = (h /. (i + 1)) `1 by A5, A14, GOBOARD7:5; now__::_thesis:_(_(_(h_/._i)_`2_>=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_<=_p_`1_)_or_(_(h_/._i)_`2_<_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_<=_p_`1_)_) percases ( (h /. i) `2 >= (h /. (i + 1)) `2 or (h /. i) `2 < (h /. (i + 1)) `2 ) ; case (h /. i) `2 >= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 then A18: (h /. i) `2 >= ((GoB h) * (1,(width (GoB h)))) `2 by A6, A5, TOPREAL1:4; (h /. i) `2 <= ((GoB h) * (1,(width (GoB h)))) `2 by A3, A7, A16, Th6; then (h /. i) `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A18, XXREAL_0:1; hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 by A2, A1, A3, A7, A15, Th42; ::_thesis: verum end; case (h /. i) `2 < (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 then A19: (h /. (i + 1)) `2 >= ((GoB h) * (1,(width (GoB h)))) `2 by A6, A5, TOPREAL1:4; (h /. (i + 1)) `2 <= ((GoB h) * (1,(width (GoB h)))) `2 by A4, A8, A16, Th6; then (h /. (i + 1)) `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A19, XXREAL_0:1; hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 by A2, A1, A4, A8, A17, Th42; ::_thesis: verum end; end; end; hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 ; ::_thesis: verum end; end; end; hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 ; ::_thesis: verum end; Lm7: for h being non constant standard special_circular_sequence for i1 being Element of 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = max Y holds ((GoB h) * (i1,1)) `1 >= p `1 proof let h be non constant standard special_circular_sequence; ::_thesis: for i1 being Element of 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = max Y holds ((GoB h) * (i1,1)) `1 >= p `1 let i1 be Element of NAT ; ::_thesis: 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = max Y holds ((GoB h) * (i1,1)) `1 >= p `1 let p be Point of (TOP-REAL 2); ::_thesis: 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = max Y holds ((GoB h) * (i1,1)) `1 >= p `1 let Y be non empty finite Subset of NAT; ::_thesis: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = max Y implies ((GoB h) * (i1,1)) `1 >= p `1 ) A1: 1 <= width (GoB h) by GOBOARD7:33; assume A2: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = max Y ) ; ::_thesis: ((GoB h) * (i1,1)) `1 >= p `1 then consider i being Element of NAT such that A3: 1 <= i and A4: i + 1 <= len h and A5: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14; A6: 1 <= i + 1 by A3, XREAL_1:145; i <= i + 1 by NAT_1:11; then A7: i <= len h by A4, XXREAL_0:2; A8: p `2 = ((GoB h) * (1,1)) `2 by A2, Th38; A9: 1 <= len (GoB h) by GOBOARD7:32; now__::_thesis:_(_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_(i1,1))_`1_>=_p_`1_)_or_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_(i1,1))_`1_>=_p_`1_)_) percases ( LSeg (h,i) is horizontal or LSeg (h,i) is vertical ) by SPPOL_1:19; case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * (i1,1)) `1 >= p `1 then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A3, A4, TOPREAL1:def_3; then A10: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15; then A11: p `2 = (h /. i) `2 by A5, GOBOARD7:6; A12: p `2 = (h /. (i + 1)) `2 by A5, A10, GOBOARD7:6; now__::_thesis:_(_(_(h_/._i)_`1_>=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,1))_`1_>=_p_`1_)_or_(_(h_/._i)_`1_<_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,1))_`1_>=_p_`1_)_) percases ( (h /. i) `1 >= (h /. (i + 1)) `1 or (h /. i) `1 < (h /. (i + 1)) `1 ) ; case (h /. i) `1 >= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,1)) `1 >= p `1 then A13: (h /. i) `1 >= p `1 by A5, TOPREAL1:3; ((GoB h) * (i1,1)) `1 >= (h /. i) `1 by A2, A8, A3, A7, A1, A11, Th43; hence ((GoB h) * (i1,1)) `1 >= p `1 by A13, XXREAL_0:2; ::_thesis: verum end; case (h /. i) `1 < (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,1)) `1 >= p `1 then A14: (h /. (i + 1)) `1 >= p `1 by A5, TOPREAL1:3; ((GoB h) * (i1,1)) `1 >= (h /. (i + 1)) `1 by A2, A8, A4, A1, A6, A12, Th43; hence ((GoB h) * (i1,1)) `1 >= p `1 by A14, XXREAL_0:2; ::_thesis: verum end; end; end; hence ((GoB h) * (i1,1)) `1 >= p `1 ; ::_thesis: verum end; case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * (i1,1)) `1 >= p `1 then LSeg ((h /. i),(h /. (i + 1))) is vertical by A3, A4, TOPREAL1:def_3; then A15: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16; then A16: p `1 = (h /. i) `1 by A5, GOBOARD7:5; A17: p `1 = (h /. (i + 1)) `1 by A5, A15, GOBOARD7:5; now__::_thesis:_(_(_(h_/._i)_`2_<=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,1))_`1_>=_p_`1_)_or_(_(h_/._i)_`2_>_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,1))_`1_>=_p_`1_)_) percases ( (h /. i) `2 <= (h /. (i + 1)) `2 or (h /. i) `2 > (h /. (i + 1)) `2 ) ; case (h /. i) `2 <= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,1)) `1 >= p `1 then A18: (h /. i) `2 <= ((GoB h) * (1,1)) `2 by A8, A5, TOPREAL1:4; (h /. i) `2 >= ((GoB h) * (1,1)) `2 by A3, A7, A9, Th6; then (h /. i) `2 = ((GoB h) * (1,1)) `2 by A18, XXREAL_0:1; hence ((GoB h) * (i1,1)) `1 >= p `1 by A2, A3, A7, A1, A16, Th43; ::_thesis: verum end; case (h /. i) `2 > (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,1)) `1 >= p `1 then A19: (h /. (i + 1)) `2 <= ((GoB h) * (1,1)) `2 by A8, A5, TOPREAL1:4; (h /. (i + 1)) `2 >= ((GoB h) * (1,1)) `2 by A4, A9, A6, Th6; then (h /. (i + 1)) `2 = ((GoB h) * (1,1)) `2 by A19, XXREAL_0:1; hence ((GoB h) * (i1,1)) `1 >= p `1 by A2, A4, A1, A6, A17, Th43; ::_thesis: verum end; end; end; hence ((GoB h) * (i1,1)) `1 >= p `1 ; ::_thesis: verum end; end; end; hence ((GoB h) * (i1,1)) `1 >= p `1 ; ::_thesis: verum end; Lm8: for h being non constant standard special_circular_sequence for i1 being Element of 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 Element of 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 let h be non constant standard special_circular_sequence; ::_thesis: for i1 being Element of 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 Element of 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 let i1 be Element of NAT ; ::_thesis: 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 Element of 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 let p be Point of (TOP-REAL 2); ::_thesis: 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 Element of 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 let Y be non empty finite Subset of NAT; ::_thesis: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y implies ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 ) assume A1: ( 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 Element of NAT st ( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y ) ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 then consider i being Element of NAT such that A2: 1 <= i and A3: i + 1 <= len h and A4: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14; A5: p `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A1, Th40; i <= i + 1 by NAT_1:11; then A6: i <= len h by A3, XXREAL_0:2; A7: 1 <= i + 1 by A2, XREAL_1:145; now__::_thesis:_(_(_LSeg_(h,i)_is_horizontal_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_>=_p_`1_)_or_(_LSeg_(h,i)_is_vertical_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_>=_p_`1_)_) percases ( LSeg (h,i) is horizontal or LSeg (h,i) is vertical ) by SPPOL_1:19; case LSeg (h,i) is horizontal ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 then LSeg ((h /. i),(h /. (i + 1))) is horizontal by A2, A3, TOPREAL1:def_3; then A8: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15; then A9: p `2 = (h /. i) `2 by A4, GOBOARD7:6; A10: p `2 = (h /. (i + 1)) `2 by A4, A8, GOBOARD7:6; now__::_thesis:_(_(_(h_/._i)_`1_>=_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_>=_p_`1_)_or_(_(h_/._i)_`1_<_(h_/._(i_+_1))_`1_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_>=_p_`1_)_) percases ( (h /. i) `1 >= (h /. (i + 1)) `1 or (h /. i) `1 < (h /. (i + 1)) `1 ) ; caseA11: (h /. i) `1 >= (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 1 <= width (GoB h) by GOBOARD7:33; then A12: ((GoB h) * (i1,(width (GoB h)))) `1 >= (h /. i) `1 by A1, A5, A2, A6, A9, Th43; (h /. i) `1 >= p `1 by A4, A11, TOPREAL1:3; hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A12, XXREAL_0:2; ::_thesis: verum end; caseA13: (h /. i) `1 < (h /. (i + 1)) `1 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 1 <= width (GoB h) by GOBOARD7:33; then A14: ((GoB h) * (i1,(width (GoB h)))) `1 >= (h /. (i + 1)) `1 by A1, A5, A3, A7, A10, Th43; (h /. (i + 1)) `1 >= p `1 by A4, A13, TOPREAL1:3; hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A14, XXREAL_0:2; ::_thesis: verum end; end; end; hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 ; ::_thesis: verum end; case LSeg (h,i) is vertical ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 then LSeg ((h /. i),(h /. (i + 1))) is vertical by A2, A3, TOPREAL1:def_3; then A15: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16; then A16: p `1 = (h /. i) `1 by A4, GOBOARD7:5; A17: 1 <= len (GoB h) by GOBOARD7:32; A18: p `1 = (h /. (i + 1)) `1 by A4, A15, GOBOARD7:5; now__::_thesis:_(_(_(h_/._i)_`2_>=_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_>=_p_`1_)_or_(_(h_/._i)_`2_<_(h_/._(i_+_1))_`2_&_((GoB_h)_*_(i1,(width_(GoB_h))))_`1_>=_p_`1_)_) percases ( (h /. i) `2 >= (h /. (i + 1)) `2 or (h /. i) `2 < (h /. (i + 1)) `2 ) ; case (h /. i) `2 >= (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 then A19: (h /. i) `2 >= ((GoB h) * (1,(width (GoB h)))) `2 by A5, A4, TOPREAL1:4; (h /. i) `2 <= ((GoB h) * (1,(width (GoB h)))) `2 by A2, A6, A17, Th6; then A20: (h /. i) `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A19, XXREAL_0:1; 1 <= width (GoB h) by GOBOARD7:33; hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A1, A2, A6, A16, A20, Th43; ::_thesis: verum end; case (h /. i) `2 < (h /. (i + 1)) `2 ; ::_thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 then A21: (h /. (i + 1)) `2 >= ((GoB h) * (1,(width (GoB h)))) `2 by A5, A4, TOPREAL1:4; (h /. (i + 1)) `2 <= ((GoB h) * (1,(width (GoB h)))) `2 by A3, A7, A17, Th6; then A22: (h /. (i + 1)) `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A21, XXREAL_0:1; 1 <= width (GoB h) by GOBOARD7:33; hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A1, A3, A7, A18, A22, Th43; ::_thesis: verum end; end; end; hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 ; ::_thesis: verum end; end; end; hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 ; ::_thesis: verum end; Lm9: for h being non constant standard special_circular_sequence holds len h >= 2 by GOBOARD7:34, XXREAL_0:2; begin definition let g be non constant standard special_circular_sequence; func i_s_w g -> Element of NAT means :Def1: :: JORDAN5D:def 1 ( [1,it] in Indices (GoB g) & (GoB g) * (1,it) = W-min (L~ g) ); existence ex b1 being Element of NAT st ( [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-min (L~ g) ) proof { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } c= REAL proof let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } or X in REAL ) assume X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL then ex q being Point of (TOP-REAL 2) st ( X = q `2 & q `1 = W-bound (L~ g) & q in L~ g ) ; hence X in REAL ; ::_thesis: verum end; then reconsider B = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } as Subset of REAL ; set s1 = ((GoB g) * (1,1)) `2 ; defpred S1[ Element of NAT ] means ( [1,\$1] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (1,\$1) ) ); set Y = { j where j is Element of NAT : S1[j] } ; A1: { j where j is Element of NAT : S1[j] } c= Seg (width (GoB g)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in Seg (width (GoB g)) ) assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in Seg (width (GoB g)) then ex j being Element of NAT st ( y = j & [1,j] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (1,j) ) ) ; then [1,y] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4; hence y in Seg (width (GoB g)) by ZFMISC_1:87; ::_thesis: verum end; A2: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7(); A3: 1 <= len (GoB g) by GOBOARD7:32; then consider i, j being Element of NAT such that A4: i in dom g and A5: [1,j] in Indices (GoB g) and A6: g /. i = (GoB g) * (1,j) by Th7; j in { j where j is Element of NAT : S1[j] } by A4, A5, A6; then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A1, A2; set i1 = min Y; min Y in Y by XXREAL_2:def_7; then consider j being Element of NAT such that A7: j = min Y and A8: [1,j] in Indices (GoB g) and A9: ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (1,j) ) ; A10: min Y <= width (GoB g) by A7, A8, MATRIX_1:38; A11: 1 <= len (GoB g) by A8, MATRIX_1:38; 1 <= min Y by A7, A8, MATRIX_1:38; then A12: ((GoB g) * (1,(min Y))) `1 = ((GoB g) * (1,1)) `1 by A11, A10, GOBOARD5:2; then A13: ((GoB g) * (1,(min Y))) `1 = W-bound (L~ g) by Th37; consider i being Element of NAT such that A14: i in dom g and A15: g /. i = (GoB g) * (1,j) by A9; A16: i <= len g by A14, FINSEQ_3:25; A17: 1 <= i by A14, FINSEQ_3:25; A18: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_(1,(min_Y))_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_(1,(min_Y))_in_L~_g_)_) percases ( i < len g or i = len g ) by A16, XXREAL_0:1; case i < len g ; ::_thesis: (GoB g) * (1,(min Y)) in L~ g then i + 1 <= len g by NAT_1:13; then g /. i in LSeg (g,i) by A17, TOPREAL1:21; hence (GoB g) * (1,(min Y)) in L~ g by A7, A15, SPPOL_2:17; ::_thesis: verum end; case i = len g ; ::_thesis: (GoB g) * (1,(min Y)) in L~ g then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1; hence (GoB g) * (1,(min Y)) in L~ g by A7, A15, SPPOL_2:17; ::_thesis: verum end; end; end; ((GoB g) * (1,(min Y))) `1 = W-bound (L~ g) by A12, Th37; then A19: ((GoB g) * (1,(min Y))) `2 in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } by A18; for r being real number st r in B holds r >= ((GoB g) * (1,(min Y))) `2 proof let r be real number ; ::_thesis: ( r in B implies r >= ((GoB g) * (1,(min Y))) `2 ) assume r in B ; ::_thesis: r >= ((GoB g) * (1,(min Y))) `2 then ex q being Point of (TOP-REAL 2) st ( r = q `2 & q `1 = W-bound (L~ g) & q in L~ g ) ; hence r >= ((GoB g) * (1,(min Y))) `2 by Lm1; ::_thesis: verum end; then A20: lower_bound B >= ((GoB g) * (1,(min Y))) `2 by A19, SEQ_4:43; ((GoB g) * (1,1)) `2 is LowerBound of B proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in B or ((GoB g) * (1,1)) `2 <= r ) assume r in B ; ::_thesis: ((GoB g) * (1,1)) `2 <= r then ex q being Point of (TOP-REAL 2) st ( r = q `2 & q `1 = W-bound (L~ g) & q in L~ g ) ; hence ((GoB g) * (1,1)) `2 <= r by A3, Th33; ::_thesis: verum end; then B is bounded_below by XXREAL_2:def_9; then lower_bound B <= ((GoB g) * (1,(min Y))) `2 by A19, SEQ_4:def_2; then ((GoB g) * (1,(min Y))) `2 = lower_bound B by A20, XXREAL_0:1 .= lower_bound (proj2 | (W-most (L~ g))) by Th13 ; hence ex b1 being Element of NAT st ( [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-min (L~ g) ) by A7, A8, A13, EUCLID:53; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 -> Element of NAT means :Def2: :: JORDAN5D:def 2 ( [1,it] in Indices (GoB g) & (GoB g) * (1,it) = W-max (L~ g) ); existence ex b1 being Element of NAT st ( [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-max (L~ g) ) proof { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } c= REAL proof let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } or X in REAL ) assume X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL then ex q being Point of (TOP-REAL 2) st ( X = q `2 & q `1 = W-bound (L~ g) & q in L~ g ) ; hence X in REAL ; ::_thesis: verum end; then reconsider B = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } as Subset of REAL ; set s1 = ((GoB g) * (1,(width (GoB g)))) `2 ; defpred S1[ Element of NAT ] means ( [1,\$1] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (1,\$1) ) ); set Y = { j where j is Element of NAT : S1[j] } ; A21: { j where j is Element of NAT : S1[j] } c= Seg (width (GoB g)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in Seg (width (GoB g)) ) assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in Seg (width (GoB g)) then ex j being Element of NAT st ( y = j & [1,j] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (1,j) ) ) ; then [1,y] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4; hence y in Seg (width (GoB g)) by ZFMISC_1:87; ::_thesis: verum end; A22: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7(); A23: 1 <= len (GoB g) by GOBOARD7:32; then consider i, j being Element of NAT such that A24: i in dom g and A25: [1,j] in Indices (GoB g) and A26: g /. i = (GoB g) * (1,j) by Th7; j in { j where j is Element of NAT : S1[j] } by A24, A25, A26; then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A21, A22; reconsider i1 = max Y as Element of NAT by ORDINAL1:def_12; i1 in Y by XXREAL_2:def_8; then consider j being Element of NAT such that A27: j = i1 and A28: [1,j] in Indices (GoB g) and A29: ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (1,j) ) ; A30: i1 <= width (GoB g) by A27, A28, MATRIX_1:38; A31: 1 <= len (GoB g) by A28, MATRIX_1:38; 1 <= i1 by A27, A28, MATRIX_1:38; then A32: ((GoB g) * (1,i1)) `1 = ((GoB g) * (1,1)) `1 by A31, A30, GOBOARD5:2; then A33: ((GoB g) * (1,i1)) `1 = W-bound (L~ g) by Th37; consider i being Element of NAT such that A34: i in dom g and A35: g /. i = (GoB g) * (1,j) by A29; A36: i <= len g by A34, FINSEQ_3:25; A37: 1 <= i by A34, FINSEQ_3:25; A38: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_(1,i1)_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_(1,i1)_in_L~_g_)_) percases ( i < len g or i = len g ) by A36, XXREAL_0:1; case i < len g ; ::_thesis: (GoB g) * (1,i1) in L~ g then i + 1 <= len g by NAT_1:13; then g /. i in LSeg (g,i) by A37, TOPREAL1:21; hence (GoB g) * (1,i1) in L~ g by A27, A35, SPPOL_2:17; ::_thesis: verum end; case i = len g ; ::_thesis: (GoB g) * (1,i1) in L~ g then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1; hence (GoB g) * (1,i1) in L~ g by A27, A35, SPPOL_2:17; ::_thesis: verum end; end; end; ((GoB g) * (1,i1)) `1 = W-bound (L~ g) by A32, Th37; then A39: ((GoB g) * (1,i1)) `2 in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ g) & q in L~ g ) } by A38; for r being real number st r in B holds r <= ((GoB g) * (1,i1)) `2 proof let r be real number ; ::_thesis: ( r in B implies r <= ((GoB g) * (1,i1)) `2 ) assume r in B ; ::_thesis: r <= ((GoB g) * (1,i1)) `2 then ex q being Point of (TOP-REAL 2) st ( r = q `2 & q `1 = W-bound (L~ g) & q in L~ g ) ; hence r <= ((GoB g) * (1,i1)) `2 by Lm2; ::_thesis: verum end; then A40: upper_bound B <= ((GoB g) * (1,i1)) `2 by A39, SEQ_4:45; ((GoB g) * (1,(width (GoB g)))) `2 is UpperBound of B proof let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in B or r <= ((GoB g) * (1,(width (GoB g)))) `2 ) assume r in B ; ::_thesis: r <= ((GoB g) * (1,(width (GoB g)))) `2 then ex q being Point of (TOP-REAL 2) st ( r = q `2 & q `1 = W-bound (L~ g) & q in L~ g ) ; hence r <= ((GoB g) * (1,(width (GoB g)))) `2 by A23, Th34; ::_thesis: verum end; then B is bounded_above by XXREAL_2:def_10; then upper_bound B >= ((GoB g) * (1,i1)) `2 by A39, SEQ_4:def_1; then ((GoB g) * (1,i1)) `2 = upper_bound B by A40, XXREAL_0:1 .= upper_bound (proj2 | (W-most (L~ g))) by Th13 ; hence ex b1 being Element of NAT st ( [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-max (L~ g) ) by A27, A28, A33, EUCLID:53; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 -> Element of 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 Element of NAT st ( [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-min (L~ g) ) proof { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } c= REAL proof let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } or X in REAL ) assume X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL then ex q being Point of (TOP-REAL 2) st ( X = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ; hence X in REAL ; ::_thesis: verum end; then reconsider B = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } as Subset of REAL ; set s1 = ((GoB g) * ((len (GoB g)),1)) `2 ; defpred S1[ Element of NAT ] means ( [(len (GoB g)),\$1] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * ((len (GoB g)),\$1) ) ); set Y = { j where j is Element of NAT : S1[j] } ; A41: { j where j is Element of NAT : S1[j] } c= Seg (width (GoB g)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in Seg (width (GoB g)) ) assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in Seg (width (GoB g)) then ex j being Element of NAT st ( y = j & [(len (GoB g)),j] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * ((len (GoB g)),j) ) ) ; then [(len (GoB g)),y] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4; hence y in Seg (width (GoB g)) by ZFMISC_1:87; ::_thesis: verum end; A42: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7(); A43: 1 <= len (GoB g) by GOBOARD7:32; then consider i, j being Element of NAT such that A44: i in dom g and A45: [(len (GoB g)),j] in Indices (GoB g) and A46: g /. i = (GoB g) * ((len (GoB g)),j) by Th7; j in { j where j is Element of NAT : S1[j] } by A44, A45, A46; then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A41, A42; set i1 = min Y; min Y in Y by XXREAL_2:def_7; then consider j being Element of NAT such that A47: j = min Y and A48: [(len (GoB g)),j] in Indices (GoB g) and A49: ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * ((len (GoB g)),j) ) ; A50: min Y <= width (GoB g) by A47, A48, MATRIX_1:38; A51: 1 <= len (GoB g) by A48, MATRIX_1:38; 1 <= min Y by A47, A48, MATRIX_1:38; then A52: ((GoB g) * ((len (GoB g)),(min Y))) `1 = ((GoB g) * ((len (GoB g)),1)) `1 by A51, A50, GOBOARD5:2; then A53: ((GoB g) * ((len (GoB g)),(min Y))) `1 = E-bound (L~ g) by Th39; consider i being Element of NAT such that A54: i in dom g and A55: g /. i = (GoB g) * ((len (GoB g)),j) by A49; A56: i <= len g by A54, FINSEQ_3:25; A57: 1 <= i by A54, FINSEQ_3:25; A58: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_((len_(GoB_g)),(min_Y))_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_((len_(GoB_g)),(min_Y))_in_L~_g_)_) percases ( i < len g or i = len g ) by A56, XXREAL_0:1; case i < len g ; ::_thesis: (GoB g) * ((len (GoB g)),(min Y)) in L~ g then i + 1 <= len g by NAT_1:13; then g /. i in LSeg (g,i) by A57, TOPREAL1:21; hence (GoB g) * ((len (GoB g)),(min Y)) in L~ g by A47, A55, SPPOL_2:17; ::_thesis: verum end; case i = len g ; ::_thesis: (GoB g) * ((len (GoB g)),(min Y)) in L~ g then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1; hence (GoB g) * ((len (GoB g)),(min Y)) in L~ g by A47, A55, SPPOL_2:17; ::_thesis: verum end; end; end; ((GoB g) * ((len (GoB g)),(min Y))) `1 = E-bound (L~ g) by A52, Th39; then A59: ((GoB g) * ((len (GoB g)),(min Y))) `2 in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } by A58; for r being real number st r in B holds r >= ((GoB g) * ((len (GoB g)),(min Y))) `2 proof let r be real number ; ::_thesis: ( r in B implies r >= ((GoB g) * ((len (GoB g)),(min Y))) `2 ) assume r in B ; ::_thesis: r >= ((GoB g) * ((len (GoB g)),(min Y))) `2 then ex q being Point of (TOP-REAL 2) st ( r = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ; hence r >= ((GoB g) * ((len (GoB g)),(min Y))) `2 by Lm3; ::_thesis: verum end; then A60: lower_bound B >= ((GoB g) * ((len (GoB g)),(min Y))) `2 by A59, SEQ_4:43; ((GoB g) * ((len (GoB g)),1)) `2 is LowerBound of B proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in B or ((GoB g) * ((len (GoB g)),1)) `2 <= r ) assume r in B ; ::_thesis: ((GoB g) * ((len (GoB g)),1)) `2 <= r then ex q being Point of (TOP-REAL 2) st ( r = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ; hence ((GoB g) * ((len (GoB g)),1)) `2 <= r by A43, Th33; ::_thesis: verum end; then B is bounded_below by XXREAL_2:def_9; then lower_bound B <= ((GoB g) * ((len (GoB g)),(min Y))) `2 by A59, SEQ_4:def_2; then ((GoB g) * ((len (GoB g)),(min Y))) `2 = lower_bound B by A60, XXREAL_0:1 .= lower_bound (proj2 | (E-most (L~ g))) by Th14 ; hence ex b1 being Element of NAT st ( [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-min (L~ g) ) by A47, A48, A53, EUCLID:53; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 -> Element of 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 Element of NAT st ( [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-max (L~ g) ) proof { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } c= REAL proof let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } or X in REAL ) assume X in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL then ex q being Point of (TOP-REAL 2) st ( X = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ; hence X in REAL ; ::_thesis: verum end; then reconsider B = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } as Subset of REAL ; defpred S1[ Element of NAT ] means ( [(len (GoB g)),\$1] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * ((len (GoB g)),\$1) ) ); set Y = { j where j is Element of NAT : S1[j] } ; A61: { j where j is Element of NAT : S1[j] } c= Seg (width (GoB g)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in Seg (width (GoB g)) ) assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in Seg (width (GoB g)) then ex j being Element of NAT st ( y = j & [(len (GoB g)),j] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * ((len (GoB g)),j) ) ) ; then [(len (GoB g)),y] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4; hence y in Seg (width (GoB g)) by ZFMISC_1:87; ::_thesis: verum end; A62: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7(); 0 <> len (GoB g) by GOBOARD1:def_3; then 1 <= len (GoB g) by NAT_1:14; then consider i, j being Element of NAT such that A63: i in dom g and A64: [(len (GoB g)),j] in Indices (GoB g) and A65: g /. i = (GoB g) * ((len (GoB g)),j) by Th7; j in { j where j is Element of NAT : S1[j] } by A63, A64, A65; then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A61, A62; reconsider i1 = max Y as Element of NAT by ORDINAL1:def_12; set s1 = ((GoB g) * ((len (GoB g)),(width (GoB g)))) `2 ; i1 in Y by XXREAL_2:def_8; then consider j being Element of NAT such that A66: j = i1 and A67: [(len (GoB g)),j] in Indices (GoB g) and A68: ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * ((len (GoB g)),j) ) ; A69: i1 <= width (GoB g) by A66, A67, MATRIX_1:38; A70: 1 <= len (GoB g) by A67, MATRIX_1:38; 1 <= i1 by A66, A67, MATRIX_1:38; then A71: ((GoB g) * ((len (GoB g)),i1)) `1 = ((GoB g) * ((len (GoB g)),1)) `1 by A70, A69, GOBOARD5:2; then A72: ((GoB g) * ((len (GoB g)),i1)) `1 = E-bound (L~ g) by Th39; consider i being Element of NAT such that A73: i in dom g and A74: g /. i = (GoB g) * ((len (GoB g)),j) by A68; A75: i <= len g by A73, FINSEQ_3:25; A76: 1 <= i by A73, FINSEQ_3:25; A77: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_((len_(GoB_g)),i1)_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_((len_(GoB_g)),i1)_in_L~_g_)_) percases ( i < len g or i = len g ) by A75, XXREAL_0:1; case i < len g ; ::_thesis: (GoB g) * ((len (GoB g)),i1) in L~ g then i + 1 <= len g by NAT_1:13; then g /. i in LSeg (g,i) by A76, TOPREAL1:21; hence (GoB g) * ((len (GoB g)),i1) in L~ g by A66, A74, SPPOL_2:17; ::_thesis: verum end; case i = len g ; ::_thesis: (GoB g) * ((len (GoB g)),i1) in L~ g then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1; hence (GoB g) * ((len (GoB g)),i1) in L~ g by A66, A74, SPPOL_2:17; ::_thesis: verum end; end; end; ((GoB g) * ((len (GoB g)),i1)) `1 = E-bound (L~ g) by A71, Th39; then A78: ((GoB g) * ((len (GoB g)),i1)) `2 in { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } by A77; for r being real number st r in B holds r <= ((GoB g) * ((len (GoB g)),i1)) `2 proof let r be real number ; ::_thesis: ( r in B implies r <= ((GoB g) * ((len (GoB g)),i1)) `2 ) assume r in B ; ::_thesis: r <= ((GoB g) * ((len (GoB g)),i1)) `2 then ex q being Point of (TOP-REAL 2) st ( r = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ; hence r <= ((GoB g) * ((len (GoB g)),i1)) `2 by Lm4; ::_thesis: verum end; then A79: upper_bound B <= ((GoB g) * ((len (GoB g)),i1)) `2 by A78, SEQ_4:45; ((GoB g) * ((len (GoB g)),(width (GoB g)))) `2 is UpperBound of B proof let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in B or r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `2 ) assume r in B ; ::_thesis: r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `2 then A80: ex q being Point of (TOP-REAL 2) st ( r = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ; 1 <= len (GoB g) by GOBOARD7:32; hence r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `2 by A80, Th34; ::_thesis: verum end; then B is bounded_above by XXREAL_2:def_10; then upper_bound B >= ((GoB g) * ((len (GoB g)),i1)) `2 by A78, SEQ_4:def_1; then ((GoB g) * ((len (GoB g)),i1)) `2 = upper_bound B by A79, XXREAL_0:1 .= upper_bound (proj2 | (E-most (L~ g))) by Th14 ; hence ex b1 being Element of NAT st ( [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-max (L~ g) ) by A66, A67, A72, EUCLID:53; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 -> Element of NAT means :Def5: :: JORDAN5D:def 5 ( [it,1] in Indices (GoB g) & (GoB g) * (it,1) = S-min (L~ g) ); existence ex b1 being Element of NAT st ( [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-min (L~ g) ) proof { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } c= REAL proof let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } or X in REAL ) assume X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL then ex q being Point of (TOP-REAL 2) st ( X = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ; hence X in REAL ; ::_thesis: verum end; then reconsider B = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } as Subset of REAL ; set s1 = ((GoB g) * (1,1)) `1 ; defpred S1[ Element of NAT ] means ( [\$1,1] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (\$1,1) ) ); set Y = { j where j is Element of NAT : S1[j] } ; A81: { j where j is Element of NAT : S1[j] } c= dom (GoB g) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in dom (GoB g) ) assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in dom (GoB g) then ex j being Element of NAT st ( y = j & [j,1] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (j,1) ) ) ; then [y,1] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4; hence y in dom (GoB g) by ZFMISC_1:87; ::_thesis: verum end; A82: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7(); A83: 1 <= width (GoB g) by GOBOARD7:33; then consider i, j being Element of NAT such that A84: i in dom g and A85: [j,1] in Indices (GoB g) and A86: g /. i = (GoB g) * (j,1) by Th8; j in { j where j is Element of NAT : S1[j] } by A84, A85, A86; then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A81, A82; set i1 = min Y; min Y in Y by XXREAL_2:def_7; then consider j being Element of NAT such that A87: j = min Y and A88: [j,1] in Indices (GoB g) and A89: ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (j,1) ) ; A90: min Y <= len (GoB g) by A87, A88, MATRIX_1:38; A91: 1 <= width (GoB g) by A88, MATRIX_1:38; 1 <= min Y by A87, A88, MATRIX_1:38; then A92: ((GoB g) * ((min Y),1)) `2 = ((GoB g) * (1,1)) `2 by A90, A91, GOBOARD5:1; then A93: ((GoB g) * ((min Y),1)) `2 = S-bound (L~ g) by Th38; consider i being Element of NAT such that A94: i in dom g and A95: g /. i = (GoB g) * (j,1) by A89; A96: i <= len g by A94, FINSEQ_3:25; A97: 1 <= i by A94, FINSEQ_3:25; A98: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_((min_Y),1)_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_((min_Y),1)_in_L~_g_)_) percases ( i < len g or i = len g ) by A96, XXREAL_0:1; case i < len g ; ::_thesis: (GoB g) * ((min Y),1) in L~ g then i + 1 <= len g by NAT_1:13; then g /. i in LSeg (g,i) by A97, TOPREAL1:21; hence (GoB g) * ((min Y),1) in L~ g by A87, A95, SPPOL_2:17; ::_thesis: verum end; case i = len g ; ::_thesis: (GoB g) * ((min Y),1) in L~ g then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1; hence (GoB g) * ((min Y),1) in L~ g by A87, A95, SPPOL_2:17; ::_thesis: verum end; end; end; ((GoB g) * ((min Y),1)) `2 = S-bound (L~ g) by A92, Th38; then A99: ((GoB g) * ((min Y),1)) `1 in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } by A98; for r being real number st r in B holds r >= ((GoB g) * ((min Y),1)) `1 proof let r be real number ; ::_thesis: ( r in B implies r >= ((GoB g) * ((min Y),1)) `1 ) assume r in B ; ::_thesis: r >= ((GoB g) * ((min Y),1)) `1 then ex q being Point of (TOP-REAL 2) st ( r = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ; hence r >= ((GoB g) * ((min Y),1)) `1 by Lm5; ::_thesis: verum end; then A100: lower_bound B >= ((GoB g) * ((min Y),1)) `1 by A99, SEQ_4:43; ((GoB g) * (1,1)) `1 is LowerBound of B proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in B or ((GoB g) * (1,1)) `1 <= r ) assume r in B ; ::_thesis: ((GoB g) * (1,1)) `1 <= r then ex q being Point of (TOP-REAL 2) st ( r = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ; hence ((GoB g) * (1,1)) `1 <= r by A83, Th31; ::_thesis: verum end; then B is bounded_below by XXREAL_2:def_9; then lower_bound B <= ((GoB g) * ((min Y),1)) `1 by A99, SEQ_4:def_2; then ((GoB g) * ((min Y),1)) `1 = lower_bound B by A100, XXREAL_0:1 .= lower_bound (proj1 | (S-most (L~ g))) by Th16 ; hence ex b1 being Element of NAT st ( [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-min (L~ g) ) by A87, A88, A93, EUCLID:53; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 -> Element of NAT means :Def6: :: JORDAN5D:def 6 ( [it,1] in Indices (GoB g) & (GoB g) * (it,1) = S-max (L~ g) ); existence ex b1 being Element of NAT st ( [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-max (L~ g) ) proof { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } c= REAL proof let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } or X in REAL ) assume X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL then ex q being Point of (TOP-REAL 2) st ( X = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ; hence X in REAL ; ::_thesis: verum end; then reconsider B = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } as Subset of REAL ; defpred S1[ Element of NAT ] means ( [\$1,1] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (\$1,1) ) ); set Y = { j where j is Element of NAT : S1[j] } ; A101: { j where j is Element of NAT : S1[j] } c= dom (GoB g) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in dom (GoB g) ) assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in dom (GoB g) then ex j being Element of NAT st ( y = j & [j,1] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (j,1) ) ) ; then [y,1] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4; hence y in dom (GoB g) by ZFMISC_1:87; ::_thesis: verum end; A102: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7(); 1 <= width (GoB g) by GOBOARD7:33; then consider i, j being Element of NAT such that A103: i in dom g and A104: [j,1] in Indices (GoB g) and A105: g /. i = (GoB g) * (j,1) by Th8; j in { j where j is Element of NAT : S1[j] } by A103, A104, A105; then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A101, A102; reconsider i1 = max Y as Element of NAT by ORDINAL1:def_12; set s1 = ((GoB g) * ((len (GoB g)),1)) `1 ; i1 in Y by XXREAL_2:def_8; then consider j being Element of NAT such that A106: j = i1 and A107: [j,1] in Indices (GoB g) and A108: ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (j,1) ) ; A109: i1 <= len (GoB g) by A106, A107, MATRIX_1:38; A110: 1 <= width (GoB g) by A107, MATRIX_1:38; 1 <= i1 by A106, A107, MATRIX_1:38; then A111: ((GoB g) * (i1,1)) `2 = ((GoB g) * (1,1)) `2 by A109, A110, GOBOARD5:1; then A112: ((GoB g) * (i1,1)) `2 = S-bound (L~ g) by Th38; consider i being Element of NAT such that A113: i in dom g and A114: g /. i = (GoB g) * (j,1) by A108; A115: i <= len g by A113, FINSEQ_3:25; A116: 1 <= i by A113, FINSEQ_3:25; A117: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_(i1,1)_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_(i1,1)_in_L~_g_)_) percases ( i < len g or i = len g ) by A115, XXREAL_0:1; case i < len g ; ::_thesis: (GoB g) * (i1,1) in L~ g then i + 1 <= len g by NAT_1:13; then g /. i in LSeg (g,i) by A116, TOPREAL1:21; hence (GoB g) * (i1,1) in L~ g by A106, A114, SPPOL_2:17; ::_thesis: verum end; case i = len g ; ::_thesis: (GoB g) * (i1,1) in L~ g then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1; hence (GoB g) * (i1,1) in L~ g by A106, A114, SPPOL_2:17; ::_thesis: verum end; end; end; ((GoB g) * (i1,1)) `2 = S-bound (L~ g) by A111, Th38; then A118: ((GoB g) * (i1,1)) `1 in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ g) & q in L~ g ) } by A117; for r being real number st r in B holds r <= ((GoB g) * (i1,1)) `1 proof let r be real number ; ::_thesis: ( r in B implies r <= ((GoB g) * (i1,1)) `1 ) assume r in B ; ::_thesis: r <= ((GoB g) * (i1,1)) `1 then ex q being Point of (TOP-REAL 2) st ( r = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ; hence r <= ((GoB g) * (i1,1)) `1 by Lm7; ::_thesis: verum end; then A119: upper_bound B <= ((GoB g) * (i1,1)) `1 by A118, SEQ_4:45; ((GoB g) * ((len (GoB g)),1)) `1 is UpperBound of B proof let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in B or r <= ((GoB g) * ((len (GoB g)),1)) `1 ) assume r in B ; ::_thesis: r <= ((GoB g) * ((len (GoB g)),1)) `1 then A120: ex q being Point of (TOP-REAL 2) st ( r = q `1 & q `2 = S-bound (L~ g) & q in L~ g ) ; 1 <= width (GoB g) by GOBOARD7:33; hence r <= ((GoB g) * ((len (GoB g)),1)) `1 by A120, Th32; ::_thesis: verum end; then B is bounded_above by XXREAL_2:def_10; then upper_bound B >= ((GoB g) * (i1,1)) `1 by A118, SEQ_4:def_1; then ((GoB g) * (i1,1)) `1 = upper_bound B by A119, XXREAL_0:1 .= upper_bound (proj1 | (S-most (L~ g))) by Th16 ; hence ex b1 being Element of NAT st ( [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-max (L~ g) ) by A106, A107, A112, EUCLID:53; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 -> Element of 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 Element of NAT st ( [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-min (L~ g) ) proof { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } c= REAL proof let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } or X in REAL ) assume X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL then ex q being Point of (TOP-REAL 2) st ( X = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ; hence X in REAL ; ::_thesis: verum end; then reconsider B = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } as Subset of REAL ; defpred S1[ Element of NAT ] means ( [\$1,(width (GoB g))] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (\$1,(width (GoB g))) ) ); set Y = { j where j is Element of NAT : S1[j] } ; A121: { j where j is Element of NAT : S1[j] } c= dom (GoB g) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in dom (GoB g) ) assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in dom (GoB g) then ex j being Element of NAT st ( y = j & [j,(width (GoB g))] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (j,(width (GoB g))) ) ) ; then [y,(width (GoB g))] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4; hence y in dom (GoB g) by ZFMISC_1:87; ::_thesis: verum end; A122: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7(); 1 <= width (GoB g) by GOBOARD7:33; then consider i, j being Element of NAT such that A123: i in dom g and A124: [j,(width (GoB g))] in Indices (GoB g) and A125: g /. i = (GoB g) * (j,(width (GoB g))) by Th8; j in { j where j is Element of NAT : S1[j] } by A123, A124, A125; then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A121, A122; set i1 = min Y; set s1 = ((GoB g) * (1,(width (GoB g)))) `1 ; min Y in Y by XXREAL_2:def_7; then consider j being Element of NAT such that A126: j = min Y and A127: [j,(width (GoB g))] in Indices (GoB g) and A128: ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (j,(width (GoB g))) ) ; A129: min Y <= len (GoB g) by A126, A127, MATRIX_1:38; A130: 1 <= width (GoB g) by A127, MATRIX_1:38; 1 <= min Y by A126, A127, MATRIX_1:38; then A131: ((GoB g) * ((min Y),(width (GoB g)))) `2 = ((GoB g) * (1,(width (GoB g)))) `2 by A129, A130, GOBOARD5:1; then A132: ((GoB g) * ((min Y),(width (GoB g)))) `2 = N-bound (L~ g) by Th40; consider i being Element of NAT such that A133: i in dom g and A134: g /. i = (GoB g) * (j,(width (GoB g))) by A128; A135: i <= len g by A133, FINSEQ_3:25; A136: 1 <= i by A133, FINSEQ_3:25; A137: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_((min_Y),(width_(GoB_g)))_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_((min_Y),(width_(GoB_g)))_in_L~_g_)_) percases ( i < len g or i = len g ) by A135, XXREAL_0:1; case i < len g ; ::_thesis: (GoB g) * ((min Y),(width (GoB g))) in L~ g then i + 1 <= len g by NAT_1:13; then g /. i in LSeg (g,i) by A136, TOPREAL1:21; hence (GoB g) * ((min Y),(width (GoB g))) in L~ g by A126, A134, SPPOL_2:17; ::_thesis: verum end; case i = len g ; ::_thesis: (GoB g) * ((min Y),(width (GoB g))) in L~ g then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1; hence (GoB g) * ((min Y),(width (GoB g))) in L~ g by A126, A134, SPPOL_2:17; ::_thesis: verum end; end; end; ((GoB g) * ((min Y),(width (GoB g)))) `2 = N-bound (L~ g) by A131, Th40; then A138: ((GoB g) * ((min Y),(width (GoB g)))) `1 in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } by A137; for r being real number st r in B holds r >= ((GoB g) * ((min Y),(width (GoB g)))) `1 proof let r be real number ; ::_thesis: ( r in B implies r >= ((GoB g) * ((min Y),(width (GoB g)))) `1 ) assume r in B ; ::_thesis: r >= ((GoB g) * ((min Y),(width (GoB g)))) `1 then ex q being Point of (TOP-REAL 2) st ( r = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ; hence r >= ((GoB g) * ((min Y),(width (GoB g)))) `1 by Lm6; ::_thesis: verum end; then A139: lower_bound B >= ((GoB g) * ((min Y),(width (GoB g)))) `1 by A138, SEQ_4:43; ((GoB g) * (1,(width (GoB g)))) `1 is LowerBound of B proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in B or ((GoB g) * (1,(width (GoB g)))) `1 <= r ) assume r in B ; ::_thesis: ((GoB g) * (1,(width (GoB g)))) `1 <= r then A140: ex q1 being Point of (TOP-REAL 2) st ( r = q1 `1 & q1 `2 = N-bound (L~ g) & q1 in L~ g ) ; 1 <= width (GoB g) by GOBOARD7:33; hence ((GoB g) * (1,(width (GoB g)))) `1 <= r by A140, Th31; ::_thesis: verum end; then B is bounded_below by XXREAL_2:def_9; then lower_bound B <= ((GoB g) * ((min Y),(width (GoB g)))) `1 by A138, SEQ_4:def_2; then ((GoB g) * ((min Y),(width (GoB g)))) `1 = lower_bound B by A139, XXREAL_0:1 .= lower_bound (proj1 | (N-most (L~ g))) by Th15 ; hence ex b1 being Element of NAT st ( [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-min (L~ g) ) by A126, A127, A132, EUCLID:53; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 -> Element of 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 Element of NAT st ( [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-max (L~ g) ) proof { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } c= REAL proof let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } or X in REAL ) assume X in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } ; ::_thesis: X in REAL then ex q being Point of (TOP-REAL 2) st ( X = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ; hence X in REAL ; ::_thesis: verum end; then reconsider B = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } as Subset of REAL ; defpred S1[ Element of NAT ] means ( [\$1,(width (GoB g))] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (\$1,(width (GoB g))) ) ); set Y = { j where j is Element of NAT : S1[j] } ; A141: { j where j is Element of NAT : S1[j] } c= dom (GoB g) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { j where j is Element of NAT : S1[j] } or y in dom (GoB g) ) assume y in { j where j is Element of NAT : S1[j] } ; ::_thesis: y in dom (GoB g) then ex j being Element of NAT st ( y = j & [j,(width (GoB g))] in Indices (GoB g) & ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (j,(width (GoB g))) ) ) ; then [y,(width (GoB g))] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def_4; hence y in dom (GoB g) by ZFMISC_1:87; ::_thesis: verum end; A142: { j where j is Element of NAT : S1[j] } is Subset of NAT from DOMAIN_1:sch_7(); 1 <= width (GoB g) by GOBOARD7:33; then consider i, j being Element of NAT such that A143: i in dom g and A144: [j,(width (GoB g))] in Indices (GoB g) and A145: g /. i = (GoB g) * (j,(width (GoB g))) by Th8; j in { j where j is Element of NAT : S1[j] } by A143, A144, A145; then reconsider Y = { j where j is Element of NAT : S1[j] } as non empty finite Subset of NAT by A141, A142; reconsider i1 = max Y as Element of NAT by ORDINAL1:def_12; set s1 = ((GoB g) * ((len (GoB g)),(width (GoB g)))) `1 ; i1 in Y by XXREAL_2:def_8; then consider j being Element of NAT such that A146: j = i1 and A147: [j,(width (GoB g))] in Indices (GoB g) and A148: ex i being Element of NAT st ( i in dom g & g /. i = (GoB g) * (j,(width (GoB g))) ) ; A149: i1 <= len (GoB g) by A146, A147, MATRIX_1:38; A150: 1 <= width (GoB g) by A147, MATRIX_1:38; 1 <= i1 by A146, A147, MATRIX_1:38; then A151: ((GoB g) * (i1,(width (GoB g)))) `2 = ((GoB g) * (1,(width (GoB g)))) `2 by A149, A150, GOBOARD5:1; then A152: ((GoB g) * (i1,(width (GoB g)))) `2 = N-bound (L~ g) by Th40; consider i being Element of NAT such that A153: i in dom g and A154: g /. i = (GoB g) * (j,(width (GoB g))) by A148; A155: i <= len g by A153, FINSEQ_3:25; A156: 1 <= i by A153, FINSEQ_3:25; A157: now__::_thesis:_(_(_i_<_len_g_&_(GoB_g)_*_(i1,(width_(GoB_g)))_in_L~_g_)_or_(_i_=_len_g_&_(GoB_g)_*_(i1,(width_(GoB_g)))_in_L~_g_)_) percases ( i < len g or i = len g ) by A155, XXREAL_0:1; case i < len g ; ::_thesis: (GoB g) * (i1,(width (GoB g))) in L~ g then i + 1 <= len g by NAT_1:13; then g /. i in LSeg (g,i) by A156, TOPREAL1:21; hence (GoB g) * (i1,(width (GoB g))) in L~ g by A146, A154, SPPOL_2:17; ::_thesis: verum end; case i = len g ; ::_thesis: (GoB g) * (i1,(width (GoB g))) in L~ g then g /. i in LSeg (g,(i -' 1)) by Lm9, Th1; hence (GoB g) * (i1,(width (GoB g))) in L~ g by A146, A154, SPPOL_2:17; ::_thesis: verum end; end; end; ((GoB g) * (i1,(width (GoB g)))) `2 = N-bound (L~ g) by A151, Th40; then A158: ((GoB g) * (i1,(width (GoB g)))) `1 in { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } by A157; for r being real number st r in B holds r <= ((GoB g) * (i1,(width (GoB g)))) `1 proof let r be real number ; ::_thesis: ( r in B implies r <= ((GoB g) * (i1,(width (GoB g)))) `1 ) assume r in B ; ::_thesis: r <= ((GoB g) * (i1,(width (GoB g)))) `1 then ex q being Point of (TOP-REAL 2) st ( r = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ; hence r <= ((GoB g) * (i1,(width (GoB g)))) `1 by Lm8; ::_thesis: verum end; then A159: upper_bound B <= ((GoB g) * (i1,(width (GoB g)))) `1 by A158, SEQ_4:45; ((GoB g) * ((len (GoB g)),(width (GoB g)))) `1 is UpperBound of B proof let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in B or r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `1 ) assume r in B ; ::_thesis: r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `1 then A160: ex q being Point of (TOP-REAL 2) st ( r = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ; 1 <= width (GoB g) by GOBOARD7:33; hence r <= ((GoB g) * ((len (GoB g)),(width (GoB g)))) `1 by A160, Th32; ::_thesis: verum end; then B is bounded_above by XXREAL_2:def_10; then upper_bound B >= ((GoB g) * (i1,(width (GoB g)))) `1 by A158, SEQ_4:def_1; then ((GoB g) * (i1,(width (GoB g)))) `1 = upper_bound B by A159, XXREAL_0:1 .= upper_bound (proj1 | (N-most (L~ g))) by Th15 ; hence ex b1 being Element of NAT st ( [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-max (L~ g) ) by A146, A147, A152, EUCLID:53; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 let h be non constant standard special_circular_sequence; ::_thesis: ( 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) ) A1: [(i_e_n h),(width (GoB h))] in Indices (GoB h) by Def8; A2: [(i_w_s h),1] in Indices (GoB h) by Def5; A3: [(i_e_s h),1] in Indices (GoB h) by Def6; [(i_w_n h),(width (GoB h))] in Indices (GoB h) by Def7; hence ( 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) ) by A1, A2, A3, MATRIX_1:38; ::_thesis: verum 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 let h be non constant standard special_circular_sequence; ::_thesis: ( 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) ) A1: [(len (GoB h)),(i_s_e h)] in Indices (GoB h) by Def3; A2: [1,(i_n_w h)] in Indices (GoB h) by Def2; A3: [1,(i_s_w h)] in Indices (GoB h) by Def1; [(len (GoB h)),(i_n_e h)] in Indices (GoB h) by Def4; hence ( 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) ) by A1, A2, A3, MATRIX_1:38; ::_thesis: verum end; Lm10: for h being non constant standard special_circular_sequence for i1, i2 being Element of NAT st 1 <= i1 & i1 + 1 <= len h & 1 <= i2 & i2 + 1 <= len h & h . i1 = h . i2 holds i1 = i2 proof let h be non constant standard special_circular_sequence; ::_thesis: for i1, i2 being Element of NAT st 1 <= i1 & i1 + 1 <= len h & 1 <= i2 & i2 + 1 <= len h & h . i1 = h . i2 holds i1 = i2 let i1, i2 be Element of NAT ; ::_thesis: ( 1 <= i1 & i1 + 1 <= len h & 1 <= i2 & i2 + 1 <= len h & h . i1 = h . i2 implies i1 = i2 ) assume that A1: 1 <= i1 and A2: i1 + 1 <= len h ; ::_thesis: ( not 1 <= i2 or not i2 + 1 <= len h or not h . i1 = h . i2 or i1 = i2 ) A3: i1 < len h by A2, NAT_1:13; assume that A4: 1 <= i2 and A5: i2 + 1 <= len h and A6: h . i1 = h . i2 ; ::_thesis: i1 = i2 A7: i2 < len h by A5, NAT_1:13; then A8: i2 in dom h by A4, FINSEQ_3:25; assume A9: i1 <> i2 ; ::_thesis: contradiction A10: now__::_thesis:_h_/._i1_<>_h_/._i2 percases ( i1 < i2 or i2 < i1 ) by A9, XXREAL_0:1; suppose i1 < i2 ; ::_thesis: h /. i1 <> h /. i2 hence h /. i1 <> h /. i2 by A1, A7, GOBOARD7:36; ::_thesis: verum end; suppose i2 < i1 ; ::_thesis: h /. i1 <> h /. i2 hence h /. i1 <> h /. i2 by A4, A3, GOBOARD7:36; ::_thesis: verum end; end; end; i1 in dom h by A1, A3, FINSEQ_3:25; then h /. i1 = h . i2 by A6, PARTFUN1:def_6 .= h /. i2 by A8, PARTFUN1:def_6 ; hence contradiction by A10; ::_thesis: verum end; definition let g be non constant standard special_circular_sequence; func n_s_w g -> Element of NAT means :Def9: :: JORDAN5D:def 9 ( 1 <= it & it + 1 <= len g & g . it = W-min (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = W-min (L~ g) ) proof W-min (L~ g) in rng g by SPRECT_2:43; hence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = W-min (L~ g) ) by Th3; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 -> Element of NAT means :Def10: :: JORDAN5D:def 10 ( 1 <= it & it + 1 <= len g & g . it = W-max (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = W-max (L~ g) ) proof W-max (L~ g) in rng g by SPRECT_2:44; hence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = W-max (L~ g) ) by Th3; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 -> Element of NAT means :Def11: :: JORDAN5D:def 11 ( 1 <= it & it + 1 <= len g & g . it = E-min (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = E-min (L~ g) ) proof E-min (L~ g) in rng g by SPRECT_2:45; hence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = E-min (L~ g) ) by Th3; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 -> Element of NAT means :Def12: :: JORDAN5D:def 12 ( 1 <= it & it + 1 <= len g & g . it = E-max (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = E-max (L~ g) ) proof E-max (L~ g) in rng g by SPRECT_2:46; hence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = E-max (L~ g) ) by Th3; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 -> Element of NAT means :Def13: :: JORDAN5D:def 13 ( 1 <= it & it + 1 <= len g & g . it = S-min (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = S-min (L~ g) ) proof S-min (L~ g) in rng g by SPRECT_2:41; hence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = S-min (L~ g) ) by Th3; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 -> Element of NAT means :Def14: :: JORDAN5D:def 14 ( 1 <= it & it + 1 <= len g & g . it = S-max (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = S-max (L~ g) ) proof S-max (L~ g) in rng g by SPRECT_2:42; hence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = S-max (L~ g) ) by Th3; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 -> Element of NAT means :Def15: :: JORDAN5D:def 15 ( 1 <= it & it + 1 <= len g & g . it = N-min (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = N-min (L~ g) ) proof N-min (L~ g) in rng g by SPRECT_2:39; hence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = N-min (L~ g) ) by Th3; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 -> Element of NAT means :Def16: :: JORDAN5D:def 16 ( 1 <= it & it + 1 <= len g & g . it = N-max (L~ g) ); existence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = N-max (L~ g) ) proof N-max (L~ g) in rng g by SPRECT_2:40; hence ex b1 being Element of NAT st ( 1 <= b1 & b1 + 1 <= len g & g . b1 = N-max (L~ g) ) by Th3; ::_thesis: verum end; uniqueness for b1, b2 being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 let h be non constant standard special_circular_sequence; ::_thesis: n_w_n h <> n_w_s h set i1 = n_w_n h; set i2 = n_w_s h; A1: n_w_n h <= (n_w_n h) + 1 by NAT_1:11; A2: 1 <= n_w_n h by Def15; (n_w_n h) + 1 <= len h by Def15; then n_w_n h <= len h by A1, XXREAL_0:2; then n_w_n h in dom h by A2, FINSEQ_3:25; then A3: h . (n_w_n h) = h /. (n_w_n h) by PARTFUN1:def_6; A4: n_w_s h <= (n_w_s h) + 1 by NAT_1:11; A5: h . (n_w_s h) = S-min (L~ h) by Def13; A6: 1 <= n_w_s h by Def13; (n_w_s h) + 1 <= len h by Def13; then n_w_s h <= len h by A4, XXREAL_0:2; then n_w_s h in dom h by A6, FINSEQ_3:25; then A7: h . (n_w_s h) = h /. (n_w_s h) by PARTFUN1:def_6; A8: h . (n_w_n h) = N-min (L~ h) by Def15; thus n_w_n h <> n_w_s h ::_thesis: verum proof assume n_w_n h = n_w_s h ; ::_thesis: contradiction then A9: N-bound (L~ h) = (h /. (n_w_s h)) `2 by A8, A3, EUCLID:52 .= S-bound (L~ h) by A5, A7, EUCLID:52 ; A10: 1 <= len h by GOBOARD7:34, XXREAL_0:2; then A11: (h /. 1) `2 >= S-bound (L~ h) by Th11; consider ii being Element of NAT such that A12: ii in dom h and A13: (h /. ii) `2 <> (h /. 1) `2 by GOBOARD7:31; A14: ii <= len h by A12, FINSEQ_3:25; A15: 1 <= ii by A12, FINSEQ_3:25; then A16: (h /. ii) `2 <= N-bound (L~ h) by A14, Th11; A17: (h /. ii) `2 >= S-bound (L~ h) by A15, A14, Th11; (h /. 1) `2 <= N-bound (L~ h) by A10, Th11; then (h /. 1) `2 = N-bound (L~ h) by A9, A11, XXREAL_0:1; hence contradiction by A9, A13, A16, A17, XXREAL_0:1; ::_thesis: verum end; end; theorem :: JORDAN5D:48 for h being non constant standard special_circular_sequence holds n_s_w h <> n_s_e h proof let h be non constant standard special_circular_sequence; ::_thesis: n_s_w h <> n_s_e h set i1 = n_s_w h; set i2 = n_s_e h; A1: n_s_w h <= (n_s_w h) + 1 by NAT_1:11; A2: 1 <= n_s_w h by Def9; (n_s_w h) + 1 <= len h by Def9; then n_s_w h <= len h by A1, XXREAL_0:2; then n_s_w h in dom h by A2, FINSEQ_3:25; then A3: h . (n_s_w h) = h /. (n_s_w h) by PARTFUN1:def_6; A4: n_s_e h <= (n_s_e h) + 1 by NAT_1:11; A5: h . (n_s_e h) = E-min (L~ h) by Def11; A6: 1 <= n_s_e h by Def11; (n_s_e h) + 1 <= len h by Def11; then n_s_e h <= len h by A4, XXREAL_0:2; then n_s_e h in dom h by A6, FINSEQ_3:25; then A7: h . (n_s_e h) = h /. (n_s_e h) by PARTFUN1:def_6; A8: h . (n_s_w h) = W-min (L~ h) by Def9; thus n_s_w h <> n_s_e h ::_thesis: verum proof assume n_s_w h = n_s_e h ; ::_thesis: contradiction then A9: W-bound (L~ h) = (h /. (n_s_e h)) `1 by A8, A3, EUCLID:52 .= E-bound (L~ h) by A5, A7, EUCLID:52 ; A10: 1 <= len h by GOBOARD7:34, XXREAL_0:2; then A11: (h /. 1) `1 >= W-bound (L~ h) by Th12; consider ii being Element of NAT such that A12: ii in dom h and A13: (h /. ii) `1 <> (h /. 1) `1 by GOBOARD7:30; A14: ii <= len h by A12, FINSEQ_3:25; A15: 1 <= ii by A12, FINSEQ_3:25; then A16: (h /. ii) `1 <= E-bound (L~ h) by A14, Th12; A17: (h /. ii) `1 >= W-bound (L~ h) by A15, A14, Th12; (h /. 1) `1 <= E-bound (L~ h) by A10, Th12; then (h /. 1) `1 = W-bound (L~ h) by A9, A11, XXREAL_0:1; hence contradiction by A9, A13, A16, A17, XXREAL_0:1; ::_thesis: verum end; end; theorem :: JORDAN5D:49 for h being non constant standard special_circular_sequence holds n_e_n h <> n_e_s h proof let h be non constant standard special_circular_sequence; ::_thesis: n_e_n h <> n_e_s h set i1 = n_e_n h; set i2 = n_e_s h; A1: n_e_n h <= (n_e_n h) + 1 by NAT_1:11; A2: 1 <= n_e_n h by Def16; (n_e_n h) + 1 <= len h by Def16; then n_e_n h <= len h by A1, XXREAL_0:2; then n_e_n h in dom h by A2, FINSEQ_3:25; then A3: h . (n_e_n h) = h /. (n_e_n h) by PARTFUN1:def_6; A4: n_e_s h <= (n_e_s h) + 1 by NAT_1:11; A5: h . (n_e_s h) = S-max (L~ h) by Def14; A6: 1 <= n_e_s h by Def14; (n_e_s h) + 1 <= len h by Def14; then n_e_s h <= len h by A4, XXREAL_0:2; then n_e_s h in dom h by A6, FINSEQ_3:25; then A7: h . (n_e_s h) = h /. (n_e_s h) by PARTFUN1:def_6; A8: h . (n_e_n h) = N-max (L~ h) by Def16; thus n_e_n h <> n_e_s h ::_thesis: verum proof assume n_e_n h = n_e_s h ; ::_thesis: contradiction then A9: N-bound (L~ h) = (h /. (n_e_s h)) `2 by A8, A3, EUCLID:52 .= S-bound (L~ h) by A5, A7, EUCLID:52 ; A10: 1 <= len h by GOBOARD7:34, XXREAL_0:2; then A11: (h /. 1) `2 >= S-bound (L~ h) by Th11; consider ii being Element of NAT such that A12: ii in dom h and A13: (h /. ii) `2 <> (h /. 1) `2 by GOBOARD7:31; A14: ii <= len h by A12, FINSEQ_3:25; A15: 1 <= ii by A12, FINSEQ_3:25; then A16: (h /. ii) `2 <= N-bound (L~ h) by A14, Th11; A17: (h /. ii) `2 >= S-bound (L~ h) by A15, A14, Th11; (h /. 1) `2 <= N-bound (L~ h) by A10, Th11; then (h /. 1) `2 = N-bound (L~ h) by A9, A11, XXREAL_0:1; hence contradiction by A9, A13, A16, A17, XXREAL_0:1; ::_thesis: verum end; end; theorem :: JORDAN5D:50 for h being non constant standard special_circular_sequence holds n_n_w h <> n_n_e h proof let h be non constant standard special_circular_sequence; ::_thesis: n_n_w h <> n_n_e h set i1 = n_n_w h; set i2 = n_n_e h; A1: n_n_w h <= (n_n_w h) + 1 by NAT_1:11; A2: 1 <= n_n_w h by Def10; (n_n_w h) + 1 <= len h by Def10; then n_n_w h <= len h by A1, XXREAL_0:2; then n_n_w h in dom h by A2, FINSEQ_3:25; then A3: h . (n_n_w h) = h /. (n_n_w h) by PARTFUN1:def_6; A4: n_n_e h <= (n_n_e h) + 1 by NAT_1:11; A5: h . (n_n_e h) = E-max (L~ h) by Def12; A6: 1 <= n_n_e h by Def12; (n_n_e h) + 1 <= len h by Def12; then n_n_e h <= len h by A4, XXREAL_0:2; then n_n_e h in dom h by A6, FINSEQ_3:25; then A7: h . (n_n_e h) = h /. (n_n_e h) by PARTFUN1:def_6; A8: h . (n_n_w h) = W-max (L~ h) by Def10; thus n_n_w h <> n_n_e h ::_thesis: verum proof assume n_n_w h = n_n_e h ; ::_thesis: contradiction then A9: W-bound (L~ h) = (h /. (n_n_e h)) `1 by A8, A3, EUCLID:52 .= E-bound (L~ h) by A5, A7, EUCLID:52 ; A10: 1 <= len h by GOBOARD7:34, XXREAL_0:2; then A11: (h /. 1) `1 >= W-bound (L~ h) by Th12; consider ii being Element of NAT such that A12: ii in dom h and A13: (h /. ii) `1 <> (h /. 1) `1 by GOBOARD7:30; A14: ii <= len h by A12, FINSEQ_3:25; A15: 1 <= ii by A12, FINSEQ_3:25; then A16: (h /. ii) `1 <= E-bound (L~ h) by A14, Th12; A17: (h /. ii) `1 >= W-bound (L~ h) by A15, A14, Th12; (h /. 1) `1 <= E-bound (L~ h) by A10, Th12; then (h /. 1) `1 = W-bound (L~ h) by A9, A11, XXREAL_0:1; hence contradiction by A9, A13, A16, A17, XXREAL_0:1; ::_thesis: verum end; end;