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:
given i' being Element of NAT such that A3: ( 1 <= i' & i' + 1 <= len (Gauge C,n) ) and
A4: f /. 1 = (Gauge C,n) * i',(width (Gauge C,n)) and
A5: f /. 2 = (Gauge C,n) * (i' + 1),(width (Gauge C,n)) and
A6: N-min C in cell (Gauge C,n),i',((width (Gauge C,n)) -' 1) and
A7: N-min C <> (Gauge C,n) * i',((width (Gauge C,n)) -' 1) ; :: thesis:
A8: ( i' < len (Gauge C,n) & len (Gauge C,n) = width (Gauge C,n) ) by A3, JORDAN8:def 1, NAT_1:13;
A9: len f > 4 by GOBOARD7:36;
A10: ( len (Gauge C,n) = (2 |^ n) + 3 & len (Gauge C,n) = width (Gauge C,n) ) by JORDAN8:def 1;
then A11: len (Gauge C,n) >= 3 by NAT_1:12;
then A12: 1 < len (Gauge C,n) by XXREAL_0:2;
set W = W-bound C;
set S = S-bound C;
set E = E-bound C;
set N = N-bound C;
N-min (L~ f) in rng f by SPRECT_2:43;
then consider m being Nat such that
A13: m in dom f and
A14: f . m = N-min (L~ f) by FINSEQ_2:11;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A15: f /. m = f . m by A13, PARTFUN1:def 8;
A16: (N-min (L~ f)) `2 = N-bound (L~ f) by EUCLID:56;
A17: 2 |^ n > 0 by NEWTON:102;
N-bound C > S-bound C by JORDAN8:12;
then (N-bound C) - (S-bound C) > 0 by XREAL_1:52;
then A18: ((N-bound C) - (S-bound C)) / (2 |^ n) > 0 by A17, XREAL_1:141;
A19: ( 1 <= m & m <= len f ) by A13, FINSEQ_3:27;
consider i, j being Element of NAT such that
A20: [i,j] in Indices (Gauge C,n) and
A21: f /. m = (Gauge C,n) * i,j by A1, A13, GOBOARD1:def 11;
A22: ( 1 <= i & i <= len (Gauge C,n) & 1 <= j & j <= width (Gauge C,n) ) by A20, MATRIX_1:39;
(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 A20, JORDAN8:def 1;
then A23: (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)) = N-bound (L~ f) by A14, A15, A16, A21, EUCLID:56;
1 in dom f by FINSEQ_5:6;
then A24: f /. 1 in L~ f by A9, GOBOARD1:16, XXREAL_0:2;
then A25: N-bound (L~ f) >= (f /. 1) `2 by PSCOMP_1:71;
( ((Gauge C,n) * i',j) `2 = ((Gauge C,n) * 1,j) `2 & ((Gauge C,n) * i,j) `2 = ((Gauge C,n) * 1,j) `2 ) by A3, A8, A22, GOBOARD5:2;
then ((Gauge C,n) * i,j) `2 <= ((Gauge C,n) * i',(len (Gauge C,n))) `2 by A3, A8, A22, SPRECT_3:24;
then A26: N-bound (L~ f) = (f /. 1) `2 by A4, A8, A14, A15, A16, A21, A25, XXREAL_0:1;
[i',(len (Gauge C,n))] in Indices (Gauge C,n) by A3, A8, A12, MATRIX_1:37;
then (Gauge C,n) * i',(len (Gauge C,n)) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i' - 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 A4, A8, A26, EUCLID:56;
then A27: (len (Gauge C,n)) - 2 = j - 2 by A18, A23, XCMPLX_1:5;
A28: ( (NW-corner C) `1 = W-bound C & (NE-corner C) `1 = E-bound C & (NW-corner C) `2 = N-bound C & (NE-corner C) `2 = N-bound C ) by EUCLID:56;
A29: ((Gauge C,n) * i',(len (Gauge C,n))) `1 = ((Gauge C,n) * i',1) `1 by A3, A8, A22, A27, GOBOARD5:3;
A30: ((Gauge C,n) * i,(len (Gauge C,n))) `1 = ((Gauge C,n) * i,1) `1 by A22, A27, GOBOARD5:3;
A31: ( (NW-corner (L~ f)) `1 = W-bound (L~ f) & (NE-corner (L~ f)) `1 = E-bound (L~ f) & (NW-corner (L~ f)) `2 = N-bound (L~ f) & (NE-corner (L~ f)) `2 = N-bound (L~ f) ) by EUCLID:56;
( W-bound (L~ f) <= (f /. 1) `1 & (f /. 1) `1 <= E-bound (L~ f) ) by A24, PSCOMP_1:71;
then f /. 1 in LSeg (NW-corner (L~ f)),(NE-corner (L~ f)) by A26, A31, GOBOARD7:9;
then f /. 1 in (LSeg (NW-corner (L~ f)),(NE-corner (L~ f))) /\ (L~ f) by A24, XBOOLE_0:def 4;
then A32: (N-min (L~ f)) `1 <= (f /. 1) `1 by PSCOMP_1:98;
A33: 1 <= (len (Gauge C,n)) -' 1 by A12, NAT_D:49;
then A34: (len (Gauge C,n)) -' 1 < len (Gauge C,n) by NAT_D:51;
A35: ((len (Gauge C,n)) -' 1) + 1 = len (Gauge C,n) by A11, XREAL_1:237, XXREAL_0:2;
then N-min C in { |[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))) `2 ) } by A3, A6, A8, A33, A34, GOBRD11:32;
then consider r', s' being Real such that
A36: N-min C = |[r',s']| and
A37: ( ((Gauge C,n) * i',1) `1 <= r' & r' <= ((Gauge C,n) * (i' + 1),1) `1 ) and
( ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 <= s' & s' <= ((Gauge C,n) * 1,(len (Gauge C,n))) `2 ) ;
A38: (f /. 1) `1 <= (N-min C) `1 by A4, A8, A29, A36, A37, EUCLID:56;
then A39: (N-min (L~ f)) `1 <= (N-min C) `1 by A32, XXREAL_0:2;
A40: ((Gauge C,n) * i',((len (Gauge C,n)) -' 1)) `1 = ((Gauge C,n) * i',1) `1 by A3, A8, A33, A34, GOBOARD5:3;
A41: N-min C = |[((N-min C) `1 ),((N-min C) `2 )]| by EUCLID:57;
A42: (Gauge C,n) * i',((len (Gauge C,n)) -' 1) = |[(((Gauge C,n) * i',((len (Gauge C,n)) -' 1)) `1 ),(((Gauge C,n) * i',((len (Gauge C,n)) -' 1)) `2 )]| by EUCLID:57;
A43: (N-min C) `2 = N-bound C by EUCLID:56;
A44: n in NAT by ORDINAL1:def 13;
then ((Gauge C,n) * i',((len (Gauge C,n)) -' 1)) `2 = N-bound C by A3, A8, JORDAN8:17;
then A45: ((Gauge C,n) * i',((len (Gauge C,n)) -' 1)) `1 < (N-min C) `1 by A4, A7, A8, A29, A38, A40, A41, A42, A43, XXREAL_0:1;
A46: i <= i' by A3, A4, A8, A14, A15, A21, A22, A27, A32, GOBOARD5:4;
then A47: i < len (Gauge C,n) by A8, XXREAL_0:2;
then A48: i + 1 <= len (Gauge C,n) by NAT_1:13;

per cases by A19, XXREAL_0:1;

suppose m = len f ; :: thesis:

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

end;

suppose m < len f ; :: thesis:

then A49: m + 1 <= len f by NAT_1:13;
then A50: right_cell f,m,(Gauge C,n) meets C by A2, A19;
then consider p being set such that
A51: ( p in right_cell f,m,(Gauge C,n) & p in C ) by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A51;
consider i1, j1, i2, j2 being Element of NAT such that
A52: ( [i1,j1] in Indices (Gauge C,n) & f /. m = (Gauge C,n) * i1,j1 ) and
A53: ( [i2,j2] in Indices (Gauge C,n) & f /. (m + 1) = (Gauge C,n) * i2,j2 ) and
A54: ( ( 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, A19, A49, JORDAN8:6;
A55: ( 1 <= i2 & i2 <= len (Gauge C,n) & 1 <= j2 & j2 <= len (Gauge C,n) ) by A10, A53, MATRIX_1:39;
A56: (N-min C) `2 = N-bound C by EUCLID:56;
then A57: p `2 <= (N-min C) `2 by A51, PSCOMP_1:71;
A58: ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 = N-bound C by A12, A44, JORDAN8:17;
A59: ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 < ((Gauge C,n) * 1,(len (Gauge C,n))) `2 by A10, A12, A33, A34, GOBOARD5:5;
A60: ( W-bound C <= p `1 & p `1 <= E-bound C ) by A51, PSCOMP_1:71;

now

per cases by A20, A21, A27, A52, A54, GOBOARD1:21;

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

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

end;

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

then A61: right_cell f,m,(Gauge C,n) = cell (Gauge C,n),i,((len (Gauge C,n)) -' 1) by A1, A19, A20, A21, A27, A49, A53, GOBRD13:25;
A62: 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 A10, A22, A33, A34, A47, GOBRD11:32;
then consider r, s being Real such that
A63: p = |[r,s]| and
A64: ( ((Gauge C,n) * i,1) `1 <= r & r <= ((Gauge C,n) * (i + 1),1) `1 ) and
A65: ( ((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, A61;
A66: ( p `1 = r & p `2 = s ) by A63, EUCLID:56;
then p `2 = N-bound C by A56, A57, A58, A65, XXREAL_0:1;
then p in LSeg (NW-corner C),(NE-corner C) by A28, A60, GOBOARD7:9;
then p in (LSeg (NW-corner C),(NE-corner C)) /\ C by A51, XBOOLE_0:def 4;
then (N-min C) `1 <= p `1 by PSCOMP_1:98;
then (N-min C) `1 <= ((Gauge C,n) * (i + 1),1) `1 by A64, A66, XXREAL_0:2;
then A67: N-min C in cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) by A8, A14, A15, A21, A27, A30, A35, A39, A41, A56, A58, A59, A62;
N-min C <> (Gauge C,n) * i,((len (Gauge C,n)) -' 1) by A8, A22, A33, A34, A45, A46, SPRECT_3:25;
hence N-min (L~ f) = f /. 1 by A3, A4, A6, A7, A8, A14, A15, A21, A22, A27, A48, A67, Th31; :: thesis:

end;

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

then A69: right_cell f,m,(Gauge C,n) = cell (Gauge C,n),i2,(len (Gauge C,n)) by A1, A19, A20, A21, A27, A49, A53, GOBRD13:27;
i2 < len (Gauge C,n) by A22, A68, NAT_1:13;
hence N-min (L~ f) = f /. 1 by A50, A69, JORDAN8:18; :: thesis:

end;

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

then A71: j2 = (len (Gauge C,n)) -' 1 by NAT_D:34;
then A72: right_cell f,m,(Gauge C,n) = cell (Gauge C,n),(i -' 1),((len (Gauge C,n)) -' 1) by A1, A19, A20, A21, A27, A49, A53, A70, GOBRD13:29;

now

assume A73: m = 1 ; :: thesis:
( 1 <= i' + 1 & i' + 1 <= len (Gauge C,n) ) by A3, NAT_1:13;
then ( ((Gauge C,n) * i',(len (Gauge C,n))) `2 = ((Gauge C,n) * 1,(len (Gauge C,n))) `2 & ((Gauge C,n) * (i' + 1),(len (Gauge C,n))) `2 = ((Gauge C,n) * 1,(len (Gauge C,n))) `2 ) by A3, A8, A12, GOBOARD5:2;
hence contradiction by A4, A5, A8, A21, A22, A27, A33, A34, A53, A70, A71, A73, GOBOARD5:5; :: thesis:

end;

then m > 1 by A19, XXREAL_0:1;
then A74: m -' 1 >= 1 by NAT_D:49;
A75: (m -' 1) + 1 = m by A19, XREAL_1:237;
m -' 1 <= m by NAT_D:35;
then A76: m -' 1 <= len f by A19, XXREAL_0:2;
consider i1', j1', i2', j2' being Element of NAT such that
A77: ( [i1',j1'] in Indices (Gauge C,n) & f /. (m -' 1) = (Gauge C,n) * i1',j1' ) and
A78: ( [i2',j2'] in Indices (Gauge C,n) & f /. m = (Gauge C,n) * i2',j2' ) and
A79: ( ( 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, A19, A74, A75, JORDAN8:6;
A80: ( 1 <= i1' & i1' <= len (Gauge C,n) & 1 <= j1' & j1' <= len (Gauge C,n) ) by A10, A77, MATRIX_1:39;

now

per cases by A20, A21, A27, A78, A79, GOBOARD1:21;

suppose A81: ( i1' = i & j1' + 1 = len (Gauge C,n) ) ; :: thesis:

then j1' = (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, A19, A20, A21, A27, A74, A75, A77, A81, GOBRD13:22;
hence contradiction by A2, A19, A50, A72, A74, A75; :: thesis:

end;

suppose A82: ( i1' + 1 = i & j1' = len (Gauge C,n) ) ; :: thesis:

then i1' < i by NAT_1:13;
then A83: (f /. (m -' 1)) `1 < (f /. m) `1 by A21, A22, A27, A77, A80, A82, GOBOARD5:4;
A84: ( ((Gauge C,n) * i1',j) `2 = ((Gauge C,n) * 1,j) `2 & ((Gauge C,n) * i,j) `2 = ((Gauge C,n) * 1,j) `2 ) by A22, A80, GOBOARD5:2;
m -' 1 in dom f by A74, A76, FINSEQ_3:27;
then A85: f /. (m -' 1) in L~ f by A9, 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 A14, A15, A16, A21, A27, A31, A77, A82, A84, GOBOARD7:9;
then f /. (m -' 1) in (LSeg (NW-corner (L~ f)),(NE-corner (L~ f))) /\ (L~ f) by A85, XBOOLE_0:def 4;
hence contradiction by A14, A15, A83, PSCOMP_1:98; :: thesis:

end;

suppose ( i1' = i + 1 & j1' = 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, A19, A20, A21, A27, A74, A75, A77, GOBRD13:27;
then cell (Gauge C,n),i,(len (Gauge C,n)) meets C by A2, A19, A74, A75;
hence contradiction by A22, JORDAN8:18; :: thesis:

end;

suppose ( i1' = i & j1' = (len (Gauge C,n)) + 1 ) ; :: thesis:

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

end;

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

end;

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

end;