let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
let n be Nat; :: thesis:
set G = Gauge C,n;
let f be non constant standard special_circular_sequence; :: thesis:
assume that
A1: f is_sequence_on Gauge C,n and
A2: for k being Element of NAT st 1 <= k & k + 1 <= len f holds
( left_cell f,k,(Gauge C,n) misses C & right_cell f,k,(Gauge C,n) meets C ) ; :: thesis:
N-min (L~ f) in rng f by SPRECT_2:43;
then consider m being Nat such that
A3: m in dom f and
A4: f . m = N-min (L~ f) by FINSEQ_2:11;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
consider i, j being Element of NAT such that
A5: [i,j] in Indices (Gauge C,n) and
A6: f /. m = (Gauge C,n) * i,j by A1, A3, GOBOARD1:def 11;
A7: f /. m = f . m by A3, PARTFUN1:def 8;
A8: (N-min (L~ f)) `2 = N-bound (L~ f) by EUCLID:56;
set W = W-bound C;
set S = S-bound C;
set E = E-bound C;
set N = N-bound C;
given i9 being Element of NAT such that A9: 1 <= i9 and
A10: i9 + 1 <= len (Gauge C,n) and
A11: f /. 1 = (Gauge C,n) * i9,(width (Gauge C,n)) and
A12: f /. 2 = (Gauge C,n) * (i9 + 1),(width (Gauge C,n)) and
A13: N-min C in cell (Gauge C,n),i9,((width (Gauge C,n)) -' 1) and
A14: N-min C <> (Gauge C,n) * i9,((width (Gauge C,n)) -' 1) ; :: thesis:
A15: ( (Gauge C,n) * i9,((len (Gauge C,n)) -' 1) = |[(((Gauge C,n) * i9,((len (Gauge C,n)) -' 1)) `1 ),(((Gauge C,n) * i9,((len (Gauge C,n)) -' 1)) `2 )]| & (N-min C) `2 = N-bound C ) by EUCLID:56, EUCLID:57;
(Gauge C,n) * i,j = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by A5, JORDAN8:def 1;
then A16: (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)) = N-bound (L~ f) by A4, A7, A8, A6, EUCLID:56;
N-bound C > S-bound C by JORDAN8:12;
then ( 2 |^ n > 0 & (N-bound C) - (S-bound C) > 0 ) by NEWTON:102, XREAL_1:52;
then A17: ((N-bound C) - (S-bound C)) / (2 |^ n) > 0 by XREAL_1:141;
A18: ( (NW-corner (L~ f)) `1 = W-bound (L~ f) & (NE-corner (L~ f)) `1 = E-bound (L~ f) ) by EUCLID:56;
A19: 1 <= i by A5, MATRIX_1:39;
A20: ( (NW-corner (L~ f)) `2 = N-bound (L~ f) & (NE-corner (L~ f)) `2 = N-bound (L~ f) ) by EUCLID:56;
A21: m <= len f by A3, FINSEQ_3:27;
A22: 1 <= j by A5, MATRIX_1:39;
len (Gauge C,n) = (2 |^ n) + 3 by JORDAN8:def 1;
then A23: len (Gauge C,n) >= 3 by NAT_1:12;
then A24: 1 < len (Gauge C,n) by XXREAL_0:2;
then A25: 1 <= (len (Gauge C,n)) -' 1 by NAT_D:49;
then A26: (len (Gauge C,n)) -' 1 < len (Gauge C,n) by NAT_D:51;
A27: i <= len (Gauge C,n) by A5, MATRIX_1:39;
A28: j <= width (Gauge C,n) by A5, MATRIX_1:39;
then A29: ((Gauge C,n) * i,j) `2 = ((Gauge C,n) * 1,j) `2 by A19, A27, A22, GOBOARD5:2;
A30: len f > 4 by GOBOARD7:36;
1 in dom f by FINSEQ_5:6;
then A31: f /. 1 in L~ f by A30, GOBOARD1:16, XXREAL_0:2;
then A32: N-bound (L~ f) >= (f /. 1) `2 by PSCOMP_1:71;
A33: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A34: i9 < len (Gauge C,n) by A10, NAT_1:13;
then ((Gauge C,n) * i9,j) `2 = ((Gauge C,n) * 1,j) `2 by A9, A22, A28, GOBOARD5:2;
then ((Gauge C,n) * i,j) `2 <= ((Gauge C,n) * i9,(len (Gauge C,n))) `2 by A9, A34, A33, A22, A28, A29, SPRECT_3:24;
then A35: N-bound (L~ f) = (f /. 1) `2 by A11, A33, A4, A7, A8, A6, A32, XXREAL_0:1;
[i9,(len (Gauge C,n))] in Indices (Gauge C,n) by A9, A34, A33, A24, MATRIX_1:37;
then (Gauge C,n) * i9,(len (Gauge C,n)) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i9 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge C,n)) - 2)))]| by JORDAN8:def 1;
then (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge C,n)) - 2)) = N-bound (L~ f) by A11, A33, A35, EUCLID:56;
then A36: (len (Gauge C,n)) - 2 = j - 2 by A17, A16, XCMPLX_1:5;
then A37: ((Gauge C,n) * i9,(len (Gauge C,n))) `1 = ((Gauge C,n) * i9,1) `1 by A9, A34, A33, A22, GOBOARD5:3;
( W-bound (L~ f) <= (f /. 1) `1 & (f /. 1) `1 <= E-bound (L~ f) ) by A31, PSCOMP_1:71;
then f /. 1 in LSeg (NW-corner (L~ f)),(NE-corner (L~ f)) by A35, A18, A20, GOBOARD7:9;
then f /. 1 in (LSeg (NW-corner (L~ f)),(NE-corner (L~ f))) /\ (L~ f) by A31, XBOOLE_0:def 4;
then A38: (N-min (L~ f)) `1 <= (f /. 1) `1 by PSCOMP_1:98;
then A39: i <= i9 by A9, A11, A33, A4, A7, A6, A27, A22, A36, GOBOARD5:4;
then A40: i < len (Gauge C,n) by A34, XXREAL_0:2;
then A41: i + 1 <= len (Gauge C,n) by NAT_1:13;
A42: ((len (Gauge C,n)) -' 1) + 1 = len (Gauge C,n) by A23, XREAL_1:237, XXREAL_0:2;
then N-min C in { |[r9,s9]| where r9, s9 is Real : ( ((Gauge C,n) * i9,1) `1 <= r9 & r9 <= ((Gauge C,n) * (i9 + 1),1) `1 & ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 <= s9 & s9 <= ((Gauge C,n) * 1,(len (Gauge C,n))) `2 ) } by A9, A13, A34, A33, A25, A26, GOBRD11:32;
then ex r9, s9 being Real st
( N-min C = |[r9,s9]| & ((Gauge C,n) * i9,1) `1 <= r9 & r9 <= ((Gauge C,n) * (i9 + 1),1) `1 & ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 <= s9 & s9 <= ((Gauge C,n) * 1,(len (Gauge C,n))) `2 ) ;
then A43: (f /. 1) `1 <= (N-min C) `1 by A11, A33, A37, EUCLID:56;
then A44: (N-min (L~ f)) `1 <= (N-min C) `1 by A38, XXREAL_0:2;
A45: 1 <= m by A3, FINSEQ_3:27;
A46: n in NAT by ORDINAL1:def 13;
then A47: ((Gauge C,n) * i9,((len (Gauge C,n)) -' 1)) `2 = N-bound C by A9, A34, JORDAN8:17;
A48: N-min C = |[((N-min C) `1 ),((N-min C) `2 )]| by EUCLID:57;
A49: ( (NW-corner C) `2 = N-bound C & (NE-corner C) `2 = N-bound C ) by EUCLID:56;
A50: ( (NW-corner C) `1 = W-bound C & (NE-corner C) `1 = E-bound C ) by EUCLID:56;
A51: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
((Gauge C,n) * i9,((len (Gauge C,n)) -' 1)) `1 = ((Gauge C,n) * i9,1) `1 by A9, A34, A33, A25, A26, GOBOARD5:3;
then A52: ((Gauge C,n) * i9,((len (Gauge C,n)) -' 1)) `1 < (N-min C) `1 by A11, A14, A33, A37, A43, A48, A15, A47, XXREAL_0:1;
A53: ((Gauge C,n) * i,(len (Gauge C,n))) `1 = ((Gauge C,n) * i,1) `1 by A19, A27, A22, A28, A36, GOBOARD5:3;

per cases by A21, XXREAL_0:1;

suppose m = len f ; :: thesis:

hence N-min (L~ f) = f /. 1 by A4, A7, FINSEQ_6:def 1; :: thesis:

end;

suppose m < len f ; :: thesis:

then A54: m + 1 <= len f by NAT_1:13;
then consider i1, j1, i2, j2 being Element of NAT such that
A55: ( [i1,j1] in Indices (Gauge C,n) & f /. m = (Gauge C,n) * i1,j1 ) and
A56: [i2,j2] in Indices (Gauge C,n) and
A57: f /. (m + 1) = (Gauge C,n) * i2,j2 and
A58: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A45, JORDAN8:6;
A59: right_cell f,m,(Gauge C,n) meets C by A2, A45, A54;
then consider p being set such that
A60: p in right_cell f,m,(Gauge C,n) and
A61: p in C by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A60;
A62: ( W-bound C <= p `1 & p `1 <= E-bound C ) by A61, PSCOMP_1:71;
A63: (N-min C) `2 = N-bound C by EUCLID:56;
then A64: p `2 <= (N-min C) `2 by A61, PSCOMP_1:71;
A65: ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 < ((Gauge C,n) * 1,(len (Gauge C,n))) `2 by A51, A24, A25, A26, GOBOARD5:5;
A66: ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 = N-bound C by A24, A46, JORDAN8:17;
A67: j2 <= len (Gauge C,n) by A51, A56, MATRIX_1:39;

now

per cases by A5, A6, A36, A55, A58, GOBOARD1:21;

suppose ( i = i2 & (len (Gauge C,n)) + 1 = j2 ) ; :: thesis:

hence N-min (L~ f) = f /. 1 by A67, NAT_1:13; :: thesis:

end;

suppose A68: ( i + 1 = i2 & len (Gauge C,n) = j2 ) ; :: thesis:

A69: cell (Gauge C,n),i,((len (Gauge C,n)) -' 1) = { |[r,s]| where r, s is Real : ( ((Gauge C,n) * i,1) `1 <= r & r <= ((Gauge C,n) * (i + 1),1) `1 & ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 <= s & s <= ((Gauge C,n) * 1,(((len (Gauge C,n)) -' 1) + 1)) `2 ) } by A51, A19, A25, A26, A40, GOBRD11:32;
right_cell f,m,(Gauge C,n) = cell (Gauge C,n),i,((len (Gauge C,n)) -' 1) by A1, A45, A5, A6, A36, A54, A56, A57, A68, GOBRD13:25;
then consider r, s being Real such that
A70: p = |[r,s]| and
((Gauge C,n) * i,1) `1 <= r and
A71: r <= ((Gauge C,n) * (i + 1),1) `1 and
A72: ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 <= s and
s <= ((Gauge C,n) * 1,(((len (Gauge C,n)) -' 1) + 1)) `2 by A60, A69;
p `2 = s by A70, EUCLID:56;
then p `2 = N-bound C by A63, A64, A66, A72, XXREAL_0:1;
then p in LSeg (NW-corner C),(NE-corner C) by A50, A49, A62, GOBOARD7:9;
then p in (LSeg (NW-corner C),(NE-corner C)) /\ C by A61, XBOOLE_0:def 4;
then A73: (N-min C) `1 <= p `1 by PSCOMP_1:98;
p `1 = r by A70, EUCLID:56;
then (N-min C) `1 <= ((Gauge C,n) * (i + 1),1) `1 by A71, A73, XXREAL_0:2;
then A74: N-min C in cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) by A33, A4, A7, A6, A36, A53, A42, A44, A48, A63, A66, A65, A69;
N-min C <> (Gauge C,n) * i,((len (Gauge C,n)) -' 1) by A34, A33, A19, A25, A26, A52, A39, SPRECT_3:25;
hence N-min (L~ f) = f /. 1 by A9, A10, A11, A13, A14, A33, A4, A7, A6, A19, A36, A41, A74, Th31; :: thesis:

end;

suppose ( i = i2 + 1 & len (Gauge C,n) = j2 ) ; :: thesis:

then ( right_cell f,m,(Gauge C,n) = cell (Gauge C,n),i2,(len (Gauge C,n)) & i2 < len (Gauge C,n) ) by A1, A45, A5, A6, A27, A36, A54, A56, A57, GOBRD13:27, NAT_1:13;
hence N-min (L~ f) = f /. 1 by A2, A45, A54, JORDAN8:18; :: thesis:

end;

suppose A75: ( i = i2 & len (Gauge C,n) = j2 + 1 ) ; :: thesis:

then A76: j2 = (len (Gauge C,n)) -' 1 by NAT_D:34;
then A77: right_cell f,m,(Gauge C,n) = cell (Gauge C,n),(i -' 1),((len (Gauge C,n)) -' 1) by A1, A45, A5, A6, A36, A54, A56, A57, A75, GOBRD13:29;
m -' 1 <= m by NAT_D:35;
then A78: m -' 1 <= len f by A21, XXREAL_0:2;

now

1 <= i9 + 1 by A9, NAT_1:13;
then A79: ((Gauge C,n) * (i9 + 1),(len (Gauge C,n))) `2 = ((Gauge C,n) * 1,(len (Gauge C,n))) `2 by A10, A33, A24, GOBOARD5:2;
assume A80: m = 1 ; :: thesis:
((Gauge C,n) * i9,(len (Gauge C,n))) `2 = ((Gauge C,n) * 1,(len (Gauge C,n))) `2 by A9, A34, A33, A24, GOBOARD5:2;
hence contradiction by A11, A12, A33, A6, A19, A27, A36, A25, A26, A57, A75, A76, A80, A79, GOBOARD5:5; :: thesis:

end;

then m > 1 by A45, XXREAL_0:1;
then A81: m -' 1 >= 1 by NAT_D:49;
A82: (m -' 1) + 1 = m by A45, XREAL_1:237;
then consider i19, j19, i29, j29 being Element of NAT such that
A83: [i19,j19] in Indices (Gauge C,n) and
A84: f /. (m -' 1) = (Gauge C,n) * i19,j19 and
A85: ( [i29,j29] in Indices (Gauge C,n) & f /. m = (Gauge C,n) * i29,j29 & ( ( i19 = i29 & j19 + 1 = j29 ) or ( i19 + 1 = i29 & j19 = j29 ) or ( i19 = i29 + 1 & j19 = j29 ) or ( i19 = i29 & j19 = j29 + 1 ) ) ) by A1, A21, A81, JORDAN8:6;
A86: 1 <= i19 by A83, MATRIX_1:39;
A87: i19 <= len (Gauge C,n) by A83, MATRIX_1:39;

now

per cases by A5, A6, A36, A85, GOBOARD1:21;

suppose A88: ( i19 = i & j19 + 1 = len (Gauge C,n) ) ; :: thesis:

then j19 = (len (Gauge C,n)) -' 1 by NAT_D:34;
then left_cell f,(m -' 1),(Gauge C,n) = cell (Gauge C,n),(i -' 1),((len (Gauge C,n)) -' 1) by A1, A21, A5, A6, A36, A81, A82, A83, A84, A88, GOBRD13:22;
hence contradiction by A2, A21, A59, A77, A81, A82; :: thesis:

end;

suppose A89: ( i19 + 1 = i & j19 = len (Gauge C,n) ) ; :: thesis:

A90: ( ((Gauge C,n) * i19,j) `2 = ((Gauge C,n) * 1,j) `2 & ((Gauge C,n) * i,j) `2 = ((Gauge C,n) * 1,j) `2 ) by A19, A27, A22, A28, A86, A87, GOBOARD5:2;
m -' 1 in dom f by A81, A78, FINSEQ_3:27;
then A91: f /. (m -' 1) in L~ f by A30, GOBOARD1:16, XXREAL_0:2;
then ( W-bound (L~ f) <= (f /. (m -' 1)) `1 & (f /. (m -' 1)) `1 <= E-bound (L~ f) ) by PSCOMP_1:71;
then f /. (m -' 1) in LSeg (NW-corner (L~ f)),(NE-corner (L~ f)) by A4, A7, A8, A6, A36, A18, A20, A84, A89, A90, GOBOARD7:9;
then A92: f /. (m -' 1) in (LSeg (NW-corner (L~ f)),(NE-corner (L~ f))) /\ (L~ f) by A91, XBOOLE_0:def 4;
i19 < i by A89, NAT_1:13;
then (f /. (m -' 1)) `1 < (f /. m) `1 by A6, A27, A22, A28, A36, A84, A86, A89, GOBOARD5:4;
hence contradiction by A4, A7, A92, PSCOMP_1:98; :: thesis:

end;

suppose ( i19 = i + 1 & j19 = len (Gauge C,n) ) ; :: thesis:

then right_cell f,(m -' 1),(Gauge C,n) = cell (Gauge C,n),i,(len (Gauge C,n)) by A1, A21, A5, A6, A36, A81, A82, A83, A84, GOBRD13:27;
hence contradiction by A2, A21, A27, A81, A82, JORDAN8:18; :: thesis:

end;

suppose ( i19 = i & j19 = (len (Gauge C,n)) + 1 ) ; :: thesis:

then (len (Gauge C,n)) + 1 <= (len (Gauge C,n)) + 0 by A51, A83, MATRIX_1:39;
hence contradiction by XREAL_1:8; :: thesis:

end;

end;

end;

hence N-min (L~ f) = f /. 1 ; :: thesis:

end;

end;

end;

hence N-min (L~ f) = f /. 1 ; :: thesis:

end;

end;