set W = W-bound C;
set E = E-bound C;
set S = S-bound C;
set N = N-bound C;
set G = Gauge (C,n);
defpred S₁[ Nat, set , set ] means ( ( $1 = 0 implies ex i being Nat st
( 1 <= i & i + 1 <= len (Gauge (C,n)) & N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) & $3 = <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ) ) & ( $1 = 1 implies ex i being Nat st
( 1 <= i & i + 1 <= len (Gauge (C,n)) & N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) & $3 = <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))))*> ) ) & ( $1 > 1 & $2 is FinSequence of (TOP-REAL 2) implies for f being FinSequence of (TOP-REAL 2) st $2 = f holds
( ( len f = $1 implies ( ( f is_sequence_on Gauge (C,n) & right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C implies ( ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) misses C & front_right_cell (f,((len f) -' 1),(Gauge (C,n))) misses C implies ex i, j being Nat st
( f ^ <*((Gauge (C,n)) * (i,j))*> turns_right (len f) -' 1, Gauge (C,n) & $3 = f ^ <*((Gauge (C,n)) * (i,j))*> ) ) & ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) misses C & front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C implies ex i, j being Nat st
( f ^ <*((Gauge (C,n)) * (i,j))*> goes_straight (len f) -' 1, Gauge (C,n) & $3 = f ^ <*((Gauge (C,n)) * (i,j))*> ) ) & ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C implies ex i, j being Nat st
( f ^ <*((Gauge (C,n)) * (i,j))*> turns_left (len f) -' 1, Gauge (C,n) & $3 = f ^ <*((Gauge (C,n)) * (i,j))*> ) ) ) ) & ( ( not f is_sequence_on Gauge (C,n) or right_cell (f,((len f) -' 1),(Gauge (C,n))) misses C ) implies $3 = f ^ <*((Gauge (C,n)) * (1,1))*> ) ) ) & ( len f <> $1 implies $3 = {} ) ) ) & ( $1 > 1 & $2 is not FinSequence of (TOP-REAL 2) implies $3 = {} ) );
A2: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
A3: for k being Nat
for x being set ex y being set st S₁[k,x,y]

let k be Nat; :: thesis:
let x be set ; :: thesis:
consider m being Nat such that
A4: ( 1 <= m & m + 1 <= len (Gauge (C,n)) & N-min C in cell ((Gauge (C,n)),m,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (m,((width (Gauge (C,n))) -' 1)) ) by Th28;

per cases by NAT_1:25;

suppose A5: k = 0 ; :: thesis:

take <*((Gauge (C,n)) * (m,(width (Gauge (C,n)))))*> ; :: thesis:
thus S₁[k,x,<*((Gauge (C,n)) * (m,(width (Gauge (C,n)))))*>] by A4, A5; :: thesis:

end;

suppose A6: k = 1 ; :: thesis:

take <*((Gauge (C,n)) * (m,(width (Gauge (C,n))))),((Gauge (C,n)) * ((m + 1),(width (Gauge (C,n)))))*> ; :: thesis:
thus S₁[k,x,<*((Gauge (C,n)) * (m,(width (Gauge (C,n))))),((Gauge (C,n)) * ((m + 1),(width (Gauge (C,n)))))*>] by A4, A6; :: thesis:

end;

suppose that A7: k > 1 and
A8: x is FinSequence of (TOP-REAL 2) ; :: thesis:

reconsider f = x as FinSequence of (TOP-REAL 2) by A8;

per cases ;

suppose A9: len f = k ; :: thesis:

per cases ;

suppose A10: ( f is_sequence_on Gauge (C,n) & right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C ) ; :: thesis:

A11: ((len f) -' 1) + 1 = len f by A7, A9, XREAL_1:235;
then A12: ((len f) -' 1) + (1 + 1) = (len f) + 1 ;
A13: ((len f) -' 1) + 1 in dom f by A7, A9, A11, FINSEQ_3:25;
A14: 1 <= (len f) -' 1 by A7, A9, NAT_D:49;
then consider i1, j1, i2, j2 being Nat such that
A15: [i1,j1] in Indices (Gauge (C,n)) and
A16: f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) and
A17: [i2,j2] in Indices (Gauge (C,n)) and
A18: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i2,j2) and
A19: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10, A11, JORDAN8:3;
A20: i1 <= len (Gauge (C,n)) by A15, MATRIX_0:32;
A21: 1 <= j2 + 1 by NAT_1:12;
A22: 1 <= i2 by A17, MATRIX_0:32;
A23: j1 <= width (Gauge (C,n)) by A15, MATRIX_0:32;
A24: 1 <= i2 + 1 by NAT_1:12;
A25: 1 <= j2 by A17, MATRIX_0:32;
(len f) -' 1 <= len f by NAT_D:35;
then A26: (len f) -' 1 in dom f by A14, FINSEQ_3:25;
A27: j2 <= width (Gauge (C,n)) by A17, MATRIX_0:32;
then A28: j2 -' 1 <= width (Gauge (C,n)) by NAT_D:44;
A29: i2 <= len (Gauge (C,n)) by A17, MATRIX_0:32;
then A30: i2 -' 1 <= len (Gauge (C,n)) by NAT_D:44;

per cases ;

suppose A31: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) misses C & front_right_cell (f,((len f) -' 1),(Gauge (C,n))) misses C ) ; :: thesis:

per cases by A19;

suppose A32: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

take f1 = f ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*>; :: thesis:

now :: thesis:

take i = i2 + 1; :: thesis:
take j = j2; :: thesis:
thus f1 turns_right (len f) -' 1, Gauge (C,n) :: thesis:

proof

let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 6 :: thesis:
assume that
A33: [i19,j19] in Indices (Gauge (C,n)) and
A34: [i29,j29] in Indices (Gauge (C,n)) and
A35: f1 /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) and
A36: f1 /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A37: f /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) by A26, A35, FINSEQ_4:68;
then A38: i1 = i19 by A15, A16, A33, GOBOARD1:5;
A39: j1 = j19 by A15, A16, A33, A37, GOBOARD1:5;
A40: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A13, A36, FINSEQ_4:68;
then A41: i2 = i29 by A17, A18, A34, GOBOARD1:5;
A42: j2 = j29 by A17, A18, A34, A40, GOBOARD1:5;

per cases by A15, A16, A19, A33, A37, A41, A42, GOBOARD1:5;

case ( i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

now :: thesis:

assume i2 + 1 > len (Gauge (C,n)) ; :: thesis:
then A43: (len (Gauge (C,n))) + 1 <= i2 + 1 by NAT_1:13;
i2 + 1 <= (len (Gauge (C,n))) + 1 by A29, XREAL_1:6;
then i2 + 1 = (len (Gauge (C,n))) + 1 by A43, XXREAL_0:1;
then cell ((Gauge (C,n)),(len (Gauge (C,n))),j1) meets C by A10, A14, A11, A15, A16, A17, A18, A32, GOBRD13:22;
hence contradiction by A2, A23, JORDAN8:16; :: thesis:

end;

hence [(i29 + 1),j29] in Indices (Gauge (C,n)) by A25, A27, A24, A41, A42, MATRIX_0:30; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 + 1),j29) by A12, A41, A42, FINSEQ_4:67; :: thesis:

end;

case ( i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

hence ( [i29,(j29 -' 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 -' 1)) ) by A32, A38, A41; :: thesis:

end;

case ( i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

hence ( [i29,(j29 + 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 + 1)) ) by A32, A38, A41; :: thesis:

end;

case ( i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

hence ( [(i29 -' 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 -' 1),j29) ) by A32, A39, A42; :: thesis:

end;

hence S₁[k,x,f1] by A7, A9, A10, A31; :: thesis:

end;

suppose A44: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

take f1 = f ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*>; :: thesis:

now :: thesis:

take i = i2; :: thesis:
take j = j2 -' 1; :: thesis:
thus f1 turns_right (len f) -' 1, Gauge (C,n) :: thesis:

proof

let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 6 :: thesis:
assume that
A45: [i19,j19] in Indices (Gauge (C,n)) and
A46: [i29,j29] in Indices (Gauge (C,n)) and
A47: f1 /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) and
A48: f1 /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A49: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A13, A48, FINSEQ_4:68;
then A50: i2 = i29 by A17, A18, A46, GOBOARD1:5;
A51: f /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) by A26, A47, FINSEQ_4:68;
then A52: i1 = i19 by A15, A16, A45, GOBOARD1:5;
A53: j2 = j29 by A17, A18, A46, A49, GOBOARD1:5;

per cases by A15, A16, A19, A45, A51, A50, A53, GOBOARD1:5;

case ( i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

hence ( [(i29 + 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 + 1),j29) ) by A44, A52, A50; :: thesis:

end;

case ( i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

now :: thesis:

assume j2 -' 1 < 1 ; :: thesis:
then j2 <= 1 by NAT_1:14, NAT_D:36;
then j2 = 1 by A25, XXREAL_0:1;
then cell ((Gauge (C,n)),i1,(1 -' 1)) meets C by A10, A14, A11, A15, A16, A17, A18, A44, GOBRD13:24;
then cell ((Gauge (C,n)),i1,0) meets C by XREAL_1:232;
hence contradiction by A20, JORDAN8:17; :: thesis:

end;

hence [i29,(j29 -' 1)] in Indices (Gauge (C,n)) by A22, A29, A28, A50, A53, MATRIX_0:30; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 -' 1)) by A12, A50, A53, FINSEQ_4:67; :: thesis:

end;

case ( i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

hence ( [i29,(j29 + 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 + 1)) ) by A44, A52, A50; :: thesis:

end;

case ( i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

hence ( [(i29 -' 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 -' 1),j29) ) by A44, A52, A50; :: thesis:

end;

hence S₁[k,x,f1] by A7, A9, A10, A31; :: thesis:

end;

suppose A54: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

take f1 = f ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*>; :: thesis:

now :: thesis:

take i = i2; :: thesis:
take j = j2 + 1; :: thesis:
thus f1 turns_right (len f) -' 1, Gauge (C,n) :: thesis:

proof

let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 6 :: thesis:
assume that
A55: [i19,j19] in Indices (Gauge (C,n)) and
A56: [i29,j29] in Indices (Gauge (C,n)) and
A57: f1 /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) and
A58: f1 /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A59: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A13, A58, FINSEQ_4:68;
then A60: i2 = i29 by A17, A18, A56, GOBOARD1:5;
A61: f /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) by A26, A57, FINSEQ_4:68;
then A62: i1 = i19 by A15, A16, A55, GOBOARD1:5;
A63: j2 = j29 by A17, A18, A56, A59, GOBOARD1:5;

per cases by A15, A16, A19, A55, A61, A60, A63, GOBOARD1:5;

case ( i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

hence ( [(i29 + 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 + 1),j29) ) by A54, A62, A60; :: thesis:

end;

case ( i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

hence ( [i29,(j29 -' 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 -' 1)) ) by A54, A62, A60; :: thesis:

end;

case ( i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

now :: thesis:

assume j2 + 1 > len (Gauge (C,n)) ; :: thesis:
then A64: (len (Gauge (C,n))) + 1 <= j2 + 1 by NAT_1:13;
j2 + 1 <= (len (Gauge (C,n))) + 1 by A2, A27, XREAL_1:6;
then j2 + 1 = (len (Gauge (C,n))) + 1 by A64, XXREAL_0:1;
then cell ((Gauge (C,n)),i2,(len (Gauge (C,n)))) meets C by A10, A14, A11, A15, A16, A17, A18, A54, GOBRD13:26;
hence contradiction by A29, JORDAN8:15; :: thesis:

end;

hence [i29,(j29 + 1)] in Indices (Gauge (C,n)) by A2, A22, A29, A21, A60, A63, MATRIX_0:30; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 + 1)) by A12, A60, A63, FINSEQ_4:67; :: thesis:

end;

case ( i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

hence ( [(i29 -' 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 -' 1),j29) ) by A54, A62, A60; :: thesis:

end;

hence S₁[k,x,f1] by A7, A9, A10, A31; :: thesis:

end;

suppose A65: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

take f1 = f ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*>; :: thesis:

now :: thesis:

reconsider i = i2 -' 1, j = j2 as Nat ;
take i = i; :: thesis:
take j = j; :: thesis:
thus f1 turns_right (len f) -' 1, Gauge (C,n) :: thesis:

proof

let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 6 :: thesis:
assume that
A66: [i19,j19] in Indices (Gauge (C,n)) and
A67: [i29,j29] in Indices (Gauge (C,n)) and
A68: f1 /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) and
A69: f1 /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A70: f /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) by A26, A68, FINSEQ_4:68;
then A71: i1 = i19 by A15, A16, A66, GOBOARD1:5;
A72: j1 = j19 by A15, A16, A66, A70, GOBOARD1:5;
A73: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A13, A69, FINSEQ_4:68;
then A74: i2 = i29 by A17, A18, A67, GOBOARD1:5;
A75: j2 = j29 by A17, A18, A67, A73, GOBOARD1:5;

per cases by A15, A16, A19, A66, A70, A74, A75, GOBOARD1:5;

case ( i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

hence ( [(i29 + 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 + 1),j29) ) by A65, A72, A75; :: thesis:

end;

case ( i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

hence ( [i29,(j29 -' 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 -' 1)) ) by A65, A71, A74; :: thesis:

end;

case ( i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

hence ( [i29,(j29 + 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 + 1)) ) by A65, A71, A74; :: thesis:

end;

case ( i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

now :: thesis:

assume i2 -' 1 < 1 ; :: thesis:
then i2 <= 1 by NAT_1:14, NAT_D:36;
then i2 = 1 by A22, XXREAL_0:1;
then cell ((Gauge (C,n)),(1 -' 1),j2) meets C by A10, A14, A11, A15, A16, A17, A18, A65, GOBRD13:28;
then cell ((Gauge (C,n)),0,j2) meets C by XREAL_1:232;
hence contradiction by A2, A27, JORDAN8:18; :: thesis:

end;

hence [(i29 -' 1),j29] in Indices (Gauge (C,n)) by A25, A27, A30, A74, A75, MATRIX_0:30; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 -' 1),j29) by A12, A74, A75, FINSEQ_4:67; :: thesis:

end;

hence S₁[k,x,f1] by A7, A9, A10, A31; :: thesis:

end;

suppose A76: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) misses C & front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C ) ; :: thesis:

per cases by A19;

suppose A77: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

take f1 = f ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*>; :: thesis:

now :: thesis:

take i = i2; :: thesis:
take j = j2 + 1; :: thesis:
thus f1 goes_straight (len f) -' 1, Gauge (C,n) :: thesis:

proof

let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 8 :: thesis:
assume that
A78: [i19,j19] in Indices (Gauge (C,n)) and
A79: [i29,j29] in Indices (Gauge (C,n)) and
A80: f1 /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) and
A81: f1 /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A82: f /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) by A26, A80, FINSEQ_4:68;
then A83: i1 = i19 by A15, A16, A78, GOBOARD1:5;
A84: j1 = j19 by A15, A16, A78, A82, GOBOARD1:5;
A85: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A13, A81, FINSEQ_4:68;
then A86: i2 = i29 by A17, A18, A79, GOBOARD1:5;
A87: j2 = j29 by A17, A18, A79, A85, GOBOARD1:5;

per cases by A15, A16, A19, A78, A82, A86, A87, GOBOARD1:5;

case ( i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

now :: thesis:

assume j2 + 1 > len (Gauge (C,n)) ; :: thesis:
then A88: (len (Gauge (C,n))) + 1 <= j2 + 1 by NAT_1:13;
j2 + 1 <= (len (Gauge (C,n))) + 1 by A2, A27, XREAL_1:6;
then j2 + 1 = (len (Gauge (C,n))) + 1 by A88, XXREAL_0:1;
then cell ((Gauge (C,n)),i1,(len (Gauge (C,n)))) meets C by A10, A14, A11, A15, A16, A17, A18, A76, A77, GOBRD13:35;
hence contradiction by A20, JORDAN8:15; :: thesis:

end;

hence [i29,(j29 + 1)] in Indices (Gauge (C,n)) by A2, A22, A29, A21, A86, A87, MATRIX_0:30; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 + 1)) by A12, A86, A87, FINSEQ_4:67; :: thesis:

end;

case ( i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

hence ( [(i29 + 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 + 1),j29) ) by A77, A83, A86; :: thesis:

end;

case ( i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

hence ( [(i29 -' 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 -' 1),j29) ) by A77, A83, A86; :: thesis:

end;

case ( i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

hence ( [i29,(j29 -' 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 -' 1)) ) by A77, A84, A87; :: thesis:

end;

hence S₁[k,x,f1] by A7, A9, A10, A76; :: thesis:

end;

suppose A89: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

take f1 = f ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*>; :: thesis:

now :: thesis:

take i = i2 + 1; :: thesis:
take j = j2; :: thesis:
thus f1 goes_straight (len f) -' 1, Gauge (C,n) :: thesis:

proof

let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 8 :: thesis:
assume that
A90: [i19,j19] in Indices (Gauge (C,n)) and
A91: [i29,j29] in Indices (Gauge (C,n)) and
A92: f1 /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) and
A93: f1 /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A94: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A13, A93, FINSEQ_4:68;
then A95: i2 = i29 by A17, A18, A91, GOBOARD1:5;
A96: f /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) by A26, A92, FINSEQ_4:68;
then A97: i1 = i19 by A15, A16, A90, GOBOARD1:5;
A98: j2 = j29 by A17, A18, A91, A94, GOBOARD1:5;

per cases by A15, A16, A19, A90, A96, A95, A98, GOBOARD1:5;

case ( i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

hence ( [i29,(j29 + 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 + 1)) ) by A89, A97, A95; :: thesis:

end;

case ( i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

now :: thesis:

assume i2 + 1 > len (Gauge (C,n)) ; :: thesis:
then A99: (len (Gauge (C,n))) + 1 <= i2 + 1 by NAT_1:13;
i2 + 1 <= (len (Gauge (C,n))) + 1 by A29, XREAL_1:6;
then i2 + 1 = (len (Gauge (C,n))) + 1 by A99, XXREAL_0:1;
then cell ((Gauge (C,n)),(len (Gauge (C,n))),(j1 -' 1)) meets C by A10, A14, A11, A15, A16, A17, A18, A76, A89, GOBRD13:37;
hence contradiction by A2, A23, JORDAN8:16, NAT_D:44; :: thesis:

end;

hence [(i29 + 1),j29] in Indices (Gauge (C,n)) by A25, A27, A24, A95, A98, MATRIX_0:30; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 + 1),j29) by A12, A95, A98, FINSEQ_4:67; :: thesis:

end;

case ( i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

hence ( [(i29 -' 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 -' 1),j29) ) by A89, A97, A95; :: thesis:

end;

case ( i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

hence ( [i29,(j29 -' 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 -' 1)) ) by A89, A97, A95; :: thesis:

end;

hence S₁[k,x,f1] by A7, A9, A10, A76; :: thesis:

end;

suppose A100: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

take f1 = f ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*>; :: thesis:

now :: thesis:

take i = i2 -' 1; :: thesis:
take j = j2; :: thesis:
thus f1 goes_straight (len f) -' 1, Gauge (C,n) :: thesis:

proof

let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 8 :: thesis:
assume that
A101: [i19,j19] in Indices (Gauge (C,n)) and
A102: [i29,j29] in Indices (Gauge (C,n)) and
A103: f1 /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) and
A104: f1 /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A105: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A13, A104, FINSEQ_4:68;
then A106: i2 = i29 by A17, A18, A102, GOBOARD1:5;
A107: f /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) by A26, A103, FINSEQ_4:68;
then A108: i1 = i19 by A15, A16, A101, GOBOARD1:5;
A109: j2 = j29 by A17, A18, A102, A105, GOBOARD1:5;

per cases by A15, A16, A19, A101, A107, A106, A109, GOBOARD1:5;

case ( i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

hence ( [i29,(j29 + 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 + 1)) ) by A100, A108, A106; :: thesis:

end;

case ( i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

hence ( [(i29 + 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 + 1),j29) ) by A100, A108, A106; :: thesis:

end;

case ( i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

now :: thesis:

assume i2 -' 1 < 1 ; :: thesis:
then i2 <= 1 by NAT_1:14, NAT_D:36;
then i2 = 1 by A22, XXREAL_0:1;
then cell ((Gauge (C,n)),(1 -' 1),j1) meets C by A10, A14, A11, A15, A16, A17, A18, A76, A100, GOBRD13:39;
then cell ((Gauge (C,n)),0,j1) meets C by XREAL_1:232;
hence contradiction by A2, A23, JORDAN8:18; :: thesis:

end;

hence [(i29 -' 1),j29] in Indices (Gauge (C,n)) by A25, A27, A30, A106, A109, MATRIX_0:30; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 -' 1),j29) by A12, A106, A109, FINSEQ_4:67; :: thesis:

end;

case ( i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

hence ( [i29,(j29 -' 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 -' 1)) ) by A100, A108, A106; :: thesis:

end;

hence S₁[k,x,f1] by A7, A9, A10, A76; :: thesis:

end;

suppose A110: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

take f1 = f ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*>; :: thesis:

now :: thesis:

take i = i2; :: thesis:
take j = j2 -' 1; :: thesis:
thus f1 goes_straight (len f) -' 1, Gauge (C,n) :: thesis:

proof

let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 8 :: thesis:
assume that
A111: [i19,j19] in Indices (Gauge (C,n)) and
A112: [i29,j29] in Indices (Gauge (C,n)) and
A113: f1 /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) and
A114: f1 /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A115: f /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) by A26, A113, FINSEQ_4:68;
then A116: i1 = i19 by A15, A16, A111, GOBOARD1:5;
A117: j1 = j19 by A15, A16, A111, A115, GOBOARD1:5;
A118: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A13, A114, FINSEQ_4:68;
then A119: i2 = i29 by A17, A18, A112, GOBOARD1:5;
A120: j2 = j29 by A17, A18, A112, A118, GOBOARD1:5;

per cases by A15, A16, A19, A111, A115, A119, A120, GOBOARD1:5;

case ( i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

hence ( [i29,(j29 + 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 + 1)) ) by A110, A117, A120; :: thesis:

end;

case ( i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

hence ( [(i29 + 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 + 1),j29) ) by A110, A116, A119; :: thesis:

end;

case ( i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

hence ( [(i29 -' 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 -' 1),j29) ) by A110, A116, A119; :: thesis:

end;

case ( i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

now :: thesis:

assume j2 -' 1 < 1 ; :: thesis:
then j2 <= 1 by NAT_1:14, NAT_D:36;
then j2 = 1 by A25, XXREAL_0:1;
then cell ((Gauge (C,n)),(i1 -' 1),(1 -' 1)) meets C by A10, A14, A11, A15, A16, A17, A18, A76, A110, GOBRD13:41;
then cell ((Gauge (C,n)),(i1 -' 1),0) meets C by XREAL_1:232;
hence contradiction by A20, JORDAN8:17, NAT_D:44; :: thesis:

end;

hence [i29,(j29 -' 1)] in Indices (Gauge (C,n)) by A22, A29, A28, A119, A120, MATRIX_0:30; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 -' 1)) by A12, A119, A120, FINSEQ_4:67; :: thesis:

end;

hence S₁[k,x,f1] by A7, A9, A10, A76; :: thesis:

end;

suppose A121: front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C ; :: thesis:

per cases by A19;

suppose A122: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

take f1 = f ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*>; :: thesis:

now :: thesis:

take i = i2 -' 1; :: thesis:
take j = j2; :: thesis:
thus f1 turns_left (len f) -' 1, Gauge (C,n) :: thesis:

proof

let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 7 :: thesis:
assume that
A123: [i19,j19] in Indices (Gauge (C,n)) and
A124: [i29,j29] in Indices (Gauge (C,n)) and
A125: f1 /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) and
A126: f1 /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A127: f /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) by A26, A125, FINSEQ_4:68;
then A128: i1 = i19 by A15, A16, A123, GOBOARD1:5;
A129: j1 = j19 by A15, A16, A123, A127, GOBOARD1:5;
A130: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A13, A126, FINSEQ_4:68;
then A131: i2 = i29 by A17, A18, A124, GOBOARD1:5;
A132: j2 = j29 by A17, A18, A124, A130, GOBOARD1:5;

per cases by A15, A16, A19, A123, A127, A131, A132, GOBOARD1:5;

case ( i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

now :: thesis:

assume i2 -' 1 < 1 ; :: thesis:
then i2 <= 1 by NAT_1:14, NAT_D:36;
then i2 = 1 by A22, XXREAL_0:1;
then cell ((Gauge (C,n)),(1 -' 1),j2) meets C by A10, A14, A11, A15, A16, A17, A18, A121, A122, GOBRD13:34;
then cell ((Gauge (C,n)),0,j2) meets C by XREAL_1:232;
hence contradiction by A2, A27, JORDAN8:18; :: thesis:

end;

hence [(i29 -' 1),j29] in Indices (Gauge (C,n)) by A25, A27, A30, A131, A132, MATRIX_0:30; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 -' 1),j29) by A12, A131, A132, FINSEQ_4:67; :: thesis:

end;

case ( i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

hence ( [i29,(j29 + 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 + 1)) ) by A122, A128, A131; :: thesis:

end;

case ( i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

hence ( [i29,(j29 -' 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 -' 1)) ) by A122, A128, A131; :: thesis:

end;

case ( i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

hence ( [(i29 + 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 + 1),j29) ) by A122, A129, A132; :: thesis:

end;

hence S₁[k,x,f1] by A7, A9, A10, A121; :: thesis:

end;

suppose A133: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

take f1 = f ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*>; :: thesis:

now :: thesis:

take i = i2; :: thesis:
take j = j2 + 1; :: thesis:
thus f1 turns_left (len f) -' 1, Gauge (C,n) :: thesis:

proof

let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 7 :: thesis:
assume that
A134: [i19,j19] in Indices (Gauge (C,n)) and
A135: [i29,j29] in Indices (Gauge (C,n)) and
A136: f1 /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) and
A137: f1 /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A138: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A13, A137, FINSEQ_4:68;
then A139: i2 = i29 by A17, A18, A135, GOBOARD1:5;
A140: f /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) by A26, A136, FINSEQ_4:68;
then A141: i1 = i19 by A15, A16, A134, GOBOARD1:5;
A142: j2 = j29 by A17, A18, A135, A138, GOBOARD1:5;

per cases by A15, A16, A19, A134, A140, A139, A142, GOBOARD1:5;

case ( i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

hence ( [(i29 -' 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 -' 1),j29) ) by A133, A141, A139; :: thesis:

end;

case ( i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

now :: thesis:

assume j2 + 1 > len (Gauge (C,n)) ; :: thesis:
then A143: (len (Gauge (C,n))) + 1 <= j2 + 1 by NAT_1:13;
j2 + 1 <= (len (Gauge (C,n))) + 1 by A2, A27, XREAL_1:6;
then j2 + 1 = (len (Gauge (C,n))) + 1 by A143, XXREAL_0:1;
then cell ((Gauge (C,n)),i2,(len (Gauge (C,n)))) meets C by A10, A14, A11, A15, A16, A17, A18, A121, A133, GOBRD13:36;
hence contradiction by A29, JORDAN8:15; :: thesis:

end;

hence [i29,(j29 + 1)] in Indices (Gauge (C,n)) by A2, A22, A29, A21, A139, A142, MATRIX_0:30; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 + 1)) by A12, A139, A142, FINSEQ_4:67; :: thesis:

end;

case ( i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

hence ( [i29,(j29 -' 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 -' 1)) ) by A133, A141, A139; :: thesis:

end;

case ( i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

hence ( [(i29 + 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 + 1),j29) ) by A133, A141, A139; :: thesis:

end;

hence S₁[k,x,f1] by A7, A9, A10, A121; :: thesis:

end;

suppose A144: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

take f1 = f ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*>; :: thesis:

now :: thesis:

take i = i2; :: thesis:
take j = j2 -' 1; :: thesis:
thus f1 turns_left (len f) -' 1, Gauge (C,n) :: thesis:

proof

let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 7 :: thesis:
assume that
A145: [i19,j19] in Indices (Gauge (C,n)) and
A146: [i29,j29] in Indices (Gauge (C,n)) and
A147: f1 /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) and
A148: f1 /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A149: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A13, A148, FINSEQ_4:68;
then A150: i2 = i29 by A17, A18, A146, GOBOARD1:5;
A151: f /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) by A26, A147, FINSEQ_4:68;
then A152: i1 = i19 by A15, A16, A145, GOBOARD1:5;
A153: j2 = j29 by A17, A18, A146, A149, GOBOARD1:5;

per cases by A15, A16, A19, A145, A151, A150, A153, GOBOARD1:5;

case ( i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

hence ( [(i29 -' 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 -' 1),j29) ) by A144, A152, A150; :: thesis:

end;

case ( i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

hence ( [i29,(j29 + 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 + 1)) ) by A144, A152, A150; :: thesis:

end;

case ( i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

now :: thesis:

assume j2 -' 1 < 1 ; :: thesis:
then j2 <= 1 by NAT_1:14, NAT_D:36;
then j2 = 1 by A25, XXREAL_0:1;
then cell ((Gauge (C,n)),(i2 -' 1),(1 -' 1)) meets C by A10, A14, A11, A15, A16, A17, A18, A121, A144, GOBRD13:38;
then cell ((Gauge (C,n)),(i2 -' 1),0) meets C by XREAL_1:232;
hence contradiction by A29, JORDAN8:17, NAT_D:44; :: thesis:

end;

hence [i29,(j29 -' 1)] in Indices (Gauge (C,n)) by A22, A29, A28, A150, A153, MATRIX_0:30; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 -' 1)) by A12, A150, A153, FINSEQ_4:67; :: thesis:

end;

case ( i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

hence ( [(i29 + 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 + 1),j29) ) by A144, A152, A150; :: thesis:

end;

hence S₁[k,x,f1] by A7, A9, A10, A121; :: thesis:

end;

suppose A154: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

take f1 = f ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*>; :: thesis:

now :: thesis:

take i = i2 + 1; :: thesis:
take j = j2; :: thesis:
thus f1 turns_left (len f) -' 1, Gauge (C,n) :: thesis:

proof

let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 7 :: thesis:
assume that
A155: [i19,j19] in Indices (Gauge (C,n)) and
A156: [i29,j29] in Indices (Gauge (C,n)) and
A157: f1 /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) and
A158: f1 /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A159: f /. ((len f) -' 1) = (Gauge (C,n)) * (i19,j19) by A26, A157, FINSEQ_4:68;
then A160: i1 = i19 by A15, A16, A155, GOBOARD1:5;
A161: j1 = j19 by A15, A16, A155, A159, GOBOARD1:5;
A162: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A13, A158, FINSEQ_4:68;
then A163: i2 = i29 by A17, A18, A156, GOBOARD1:5;
A164: j2 = j29 by A17, A18, A156, A162, GOBOARD1:5;

per cases by A15, A16, A19, A155, A159, A163, A164, GOBOARD1:5;

case ( i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

hence ( [(i29 -' 1),j29] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 -' 1),j29) ) by A154, A161, A164; :: thesis:

end;

case ( i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

hence ( [i29,(j29 + 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 + 1)) ) by A154, A160, A163; :: thesis:

end;

case ( i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

hence ( [i29,(j29 -' 1)] in Indices (Gauge (C,n)) & f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * (i29,(j29 -' 1)) ) by A154, A160, A163; :: thesis:

end;

case ( i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

now :: thesis:

assume i2 + 1 > len (Gauge (C,n)) ; :: thesis:
then A165: (len (Gauge (C,n))) + 1 <= i2 + 1 by NAT_1:13;
i2 + 1 <= (len (Gauge (C,n))) + 1 by A29, XREAL_1:6;
then i2 + 1 = (len (Gauge (C,n))) + 1 by A165, XXREAL_0:1;
then cell ((Gauge (C,n)),(len (Gauge (C,n))),(j2 -' 1)) meets C by A10, A14, A11, A15, A16, A17, A18, A121, A154, GOBRD13:40;
hence contradiction by A2, A27, JORDAN8:16, NAT_D:44; :: thesis:

end;

hence [(i29 + 1),j29] in Indices (Gauge (C,n)) by A25, A27, A24, A163, A164, MATRIX_0:30; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge (C,n)) * ((i29 + 1),j29) by A12, A163, A164, FINSEQ_4:67; :: thesis:

end;

hence S₁[k,x,f1] by A7, A9, A10, A121; :: thesis:

end;

suppose A166: ( not f is_sequence_on Gauge (C,n) or right_cell (f,((len f) -' 1),(Gauge (C,n))) misses C ) ; :: thesis:

take f ^ <*((Gauge (C,n)) * (1,1))*> ; :: thesis:
thus S₁[k,x,f ^ <*((Gauge (C,n)) * (1,1))*>] by A7, A9, A166; :: thesis:

end;

suppose A167: len f <> k ; :: thesis:

take {} ; :: thesis:
thus S₁[k,x, {} ] by A7, A167; :: thesis:

end;

suppose A168: ( k > 1 & x is not FinSequence of (TOP-REAL 2) ) ; :: thesis:

take {} ; :: thesis:
thus S₁[k,x, {} ] by A168; :: thesis:

end;

consider F being Function such that
A169: dom F = NAT and
A170: F . 0 = {} and
A171: for k being Nat holds S₁[k,F . k,F . (k + 1)] from RECDEF_1:sch 1(A3);
defpred S₂[ Nat] means F . $1 is FinSequence of (TOP-REAL 2);
A172: {} = <*> the carrier of (TOP-REAL 2) ;
A173: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis:
assume A174: F . k is FinSequence of (TOP-REAL 2) ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A175: S₁[k,F . k,F . (k + 1)] by A171;

per cases by NAT_1:25;

suppose k = 0 ; :: thesis:

hence S₂[k + 1] by A175; :: thesis:

end;

suppose k = 1 ; :: thesis:

hence S₂[k + 1] by A175; :: thesis:

end;

suppose A176: k > 1 ; :: thesis:

reconsider f = F . k as FinSequence of (TOP-REAL 2) by A174;

per cases ;

suppose A177: len f = k ; :: thesis:

per cases ;

suppose A178: ( f is_sequence_on Gauge (C,n) & right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C ) ; :: thesis:

then A179: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C implies ex i, j being Nat st
( f ^ <*((Gauge (C,n)) * (i,j))*> turns_left (len f) -' 1, Gauge (C,n) & F . (k + 1) = f ^ <*((Gauge (C,n)) * (i,j))*> ) ) by A171, A176, A177;
A180: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) misses C & front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C implies ex i, j being Nat st
( f ^ <*((Gauge (C,n)) * (i,j))*> goes_straight (len f) -' 1, Gauge (C,n) & F . (k + 1) = f ^ <*((Gauge (C,n)) * (i,j))*> ) ) by A171, A176, A177, A178;
( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) misses C & front_right_cell (f,((len f) -' 1),(Gauge (C,n))) misses C implies ex i, j being Nat st
( f ^ <*((Gauge (C,n)) * (i,j))*> turns_right (len f) -' 1, Gauge (C,n) & F . (k + 1) = f ^ <*((Gauge (C,n)) * (i,j))*> ) ) by A171, A176, A177, A178;
hence S₂[k + 1] by A180, A179; :: thesis:

end;

suppose A181: ( not f is_sequence_on Gauge (C,n) or right_cell (f,((len f) -' 1),(Gauge (C,n))) misses C ) ; :: thesis:

f ^ <*((Gauge (C,n)) * (1,1))*> is FinSequence of (TOP-REAL 2) ;
hence S₂[k + 1] by A171, A176, A177, A181; :: thesis:

end;

suppose len f <> k ; :: thesis:

hence S₂[k + 1] by A171, A172, A176; :: thesis:

end;

A182: S₂[ 0 ] by A170, A172;
A183: for k being Nat holds S₂[k] from NAT_1:sch 2(A182, A173);
rng F c= the carrier of (TOP-REAL 2) *

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng F ; :: thesis:
then ex x being object st
( x in dom F & F . x = y ) by FUNCT_1:def 3;
then y is FinSequence of (TOP-REAL 2) by A169, A183;
hence y in the carrier of (TOP-REAL 2) * by FINSEQ_1:def 11; :: thesis:

end;

then reconsider F = F as sequence of ( the carrier of (TOP-REAL 2) *) by A169, FUNCT_2:def 1, RELSET_1:4;
defpred S₃[ Nat] means len (F . $1) = $1;
A184: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis:
assume A185: len (F . k) = k ; :: thesis:
A186: S₁[k,F . k,F . (k + 1)] by A171;

per cases by NAT_1:25;

suppose k = 0 ; :: thesis:

hence S₃[k + 1] by A186, FINSEQ_1:39; :: thesis:

end;

suppose k = 1 ; :: thesis:

hence S₃[k + 1] by A186, FINSEQ_1:44; :: thesis:

end;

suppose A187: k > 1 ; :: thesis:

thus S₃[k + 1] :: thesis:

proof

per cases ;

suppose A188: ( F . k is_sequence_on Gauge (C,n) & right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ) ; :: thesis:

then A189: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C implies ex i, j being Nat st
( (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_left (len (F . k)) -' 1, Gauge (C,n) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ) by A171, A185, A187;
A190: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C implies ex i, j being Nat st
( (F . k) ^ <*((Gauge (C,n)) * (i,j))*> goes_straight (len (F . k)) -' 1, Gauge (C,n) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ) by A171, A185, A187, A188;
( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C implies ex i, j being Nat st
( (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_right (len (F . k)) -' 1, Gauge (C,n) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ) by A171, A185, A187, A188;
hence S₃[k + 1] by A185, A190, A189, FINSEQ_2:16; :: thesis:

end;

suppose ( not F . k is_sequence_on Gauge (C,n) or right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C ) ; :: thesis:

then F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (1,1))*> by A171, A185, A187;
hence S₃[k + 1] by A185, FINSEQ_2:16; :: thesis:

end;

A191: S₃[ 0 ] by A170, CARD_1:27;
A192: for k being Nat holds S₃[k] from NAT_1:sch 2(A191, A184);

A193: now :: thesis:

let k be Nat; :: thesis:
assume that
A194: F . k is_sequence_on Gauge (C,n) and
A195: for m being Nat st 1 <= m & m + 1 <= len (F . k) holds
( left_cell ((F . k),m,(Gauge (C,n))) misses C & right_cell ((F . k),m,(Gauge (C,n))) meets C ) and
A196: k > 1 ; :: thesis:
len (F . k) = k by A192;
then A197: ( 1 <= (len (F . k)) -' 1 & ((len (F . k)) -' 1) + 1 = len (F . k) ) by A196, NAT_D:49, XREAL_1:235;
then A198: right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C by A195;
let i1, j1, i2, j2 be Nat; :: thesis:
assume that
A199: [i1,j1] in Indices (Gauge (C,n)) and
A200: (F . k) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) and
A201: [i2,j2] in Indices (Gauge (C,n)) and
A202: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) ; :: thesis:
A203: i2 <= len (Gauge (C,n)) by A201, MATRIX_0:32;
A204: 1 <= i2 + 1 by NAT_1:12;
A205: 1 <= j2 by A201, MATRIX_0:32;
A206: j2 <= width (Gauge (C,n)) by A201, MATRIX_0:32;
A207: j1 <= width (Gauge (C,n)) by A199, MATRIX_0:32;

hereby :: thesis:

assume A208: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

now :: thesis:

assume i2 + 1 > len (Gauge (C,n)) ; :: thesis:
then A209: (len (Gauge (C,n))) + 1 <= i2 + 1 by NAT_1:13;
i2 + 1 <= (len (Gauge (C,n))) + 1 by A203, XREAL_1:6;
then i2 + 1 = (len (Gauge (C,n))) + 1 by A209, XXREAL_0:1;
then cell ((Gauge (C,n)),(len (Gauge (C,n))),j1) meets C by A194, A199, A200, A201, A202, A197, A198, A208, GOBRD13:22;
hence contradiction by A2, A207, JORDAN8:16; :: thesis:

end;

hence [(i2 + 1),j2] in Indices (Gauge (C,n)) by A205, A206, A204, MATRIX_0:30; :: thesis:

end;

A210: i1 <= len (Gauge (C,n)) by A199, MATRIX_0:32;
A211: 1 <= i2 by A201, MATRIX_0:32;
A212: j2 -' 1 <= width (Gauge (C,n)) by A206, NAT_D:44;

hereby :: thesis:

assume A213: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

now :: thesis:

assume j2 -' 1 < 1 ; :: thesis:
then j2 <= 1 by NAT_1:14, NAT_D:36;
then j2 = 1 by A205, XXREAL_0:1;
then cell ((Gauge (C,n)),i1,(1 -' 1)) meets C by A194, A199, A200, A201, A202, A197, A198, A213, GOBRD13:24;
then cell ((Gauge (C,n)),i1,0) meets C by XREAL_1:232;
hence contradiction by A210, JORDAN8:17; :: thesis:

end;

hence [i2,(j2 -' 1)] in Indices (Gauge (C,n)) by A211, A203, A212, MATRIX_0:30; :: thesis:

end;

A214: 1 <= j2 + 1 by NAT_1:12;

hereby :: thesis:

assume A215: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

now :: thesis:

assume j2 + 1 > len (Gauge (C,n)) ; :: thesis:
then A216: (len (Gauge (C,n))) + 1 <= j2 + 1 by NAT_1:13;
j2 + 1 <= (len (Gauge (C,n))) + 1 by A2, A206, XREAL_1:6;
then j2 + 1 = (len (Gauge (C,n))) + 1 by A216, XXREAL_0:1;
then cell ((Gauge (C,n)),i2,(len (Gauge (C,n)))) meets C by A194, A199, A200, A201, A202, A197, A198, A215, GOBRD13:26;
hence contradiction by A203, JORDAN8:15; :: thesis:

end;

hence [i2,(j2 + 1)] in Indices (Gauge (C,n)) by A2, A211, A203, A214, MATRIX_0:30; :: thesis:

end;

A217: i2 -' 1 <= len (Gauge (C,n)) by A203, NAT_D:44;

hereby :: thesis:

assume A218: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

now :: thesis:

assume i2 -' 1 < 1 ; :: thesis:
then i2 <= 1 by NAT_1:14, NAT_D:36;
then i2 = 1 by A211, XXREAL_0:1;
then cell ((Gauge (C,n)),(1 -' 1),j2) meets C by A194, A199, A200, A201, A202, A197, A198, A218, GOBRD13:28;
then cell ((Gauge (C,n)),0,j2) meets C by XREAL_1:232;
hence contradiction by A2, A206, JORDAN8:18; :: thesis:

end;

hence [(i2 -' 1),j2] in Indices (Gauge (C,n)) by A205, A206, A217, MATRIX_0:30; :: thesis:

end;

hereby :: thesis:

assume A219: ( front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

now :: thesis:

assume j2 + 1 > len (Gauge (C,n)) ; :: thesis:
then A220: (len (Gauge (C,n))) + 1 <= j2 + 1 by NAT_1:13;
j2 + 1 <= (len (Gauge (C,n))) + 1 by A2, A206, XREAL_1:6;
then j2 + 1 = (len (Gauge (C,n))) + 1 by A220, XXREAL_0:1;
then cell ((Gauge (C,n)),i1,(len (Gauge (C,n)))) meets C by A194, A199, A200, A201, A202, A197, A219, GOBRD13:35;
hence contradiction by A210, JORDAN8:15; :: thesis:

end;

hence [i2,(j2 + 1)] in Indices (Gauge (C,n)) by A2, A211, A203, A214, MATRIX_0:30; :: thesis:

end;

hereby :: thesis:

assume A221: ( front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

now :: thesis:

assume i2 + 1 > len (Gauge (C,n)) ; :: thesis:
then A222: (len (Gauge (C,n))) + 1 <= i2 + 1 by NAT_1:13;
i2 + 1 <= (len (Gauge (C,n))) + 1 by A203, XREAL_1:6;
then i2 + 1 = (len (Gauge (C,n))) + 1 by A222, XXREAL_0:1;
then cell ((Gauge (C,n)),(len (Gauge (C,n))),(j1 -' 1)) meets C by A194, A199, A200, A201, A202, A197, A221, GOBRD13:37;
hence contradiction by A2, A207, JORDAN8:16, NAT_D:44; :: thesis:

end;

hence [(i2 + 1),j2] in Indices (Gauge (C,n)) by A205, A206, A204, MATRIX_0:30; :: thesis:

end;

hereby :: thesis:

assume A223: ( front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

now :: thesis:

assume i2 -' 1 < 1 ; :: thesis:
then i2 <= 1 by NAT_1:14, NAT_D:36;
then i2 = 1 by A211, XXREAL_0:1;
then cell ((Gauge (C,n)),(1 -' 1),j1) meets C by A194, A199, A200, A201, A202, A197, A223, GOBRD13:39;
then cell ((Gauge (C,n)),0,j1) meets C by XREAL_1:232;
hence contradiction by A2, A207, JORDAN8:18; :: thesis:

end;

hence [(i2 -' 1),j2] in Indices (Gauge (C,n)) by A205, A206, A217, MATRIX_0:30; :: thesis:

end;

hereby :: thesis:

assume A224: ( front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

now :: thesis:

assume j2 -' 1 < 1 ; :: thesis:
then j2 <= 1 by NAT_1:14, NAT_D:36;
then j2 = 1 by A205, XXREAL_0:1;
then cell ((Gauge (C,n)),(i1 -' 1),(1 -' 1)) meets C by A194, A199, A200, A201, A202, A197, A224, GOBRD13:41;
then cell ((Gauge (C,n)),(i1 -' 1),0) meets C by XREAL_1:232;
hence contradiction by A210, JORDAN8:17, NAT_D:44; :: thesis:

end;

hence [i2,(j2 -' 1)] in Indices (Gauge (C,n)) by A211, A203, A212, MATRIX_0:30; :: thesis:

end;

hereby :: thesis:

assume A225: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

now :: thesis:

assume i2 -' 1 < 1 ; :: thesis:
then i2 <= 1 by NAT_1:14, NAT_D:36;
then i2 = 1 by A211, XXREAL_0:1;
then cell ((Gauge (C,n)),(1 -' 1),j2) meets C by A194, A199, A200, A201, A202, A197, A225, GOBRD13:34;
then cell ((Gauge (C,n)),0,j2) meets C by XREAL_1:232;
hence contradiction by A2, A206, JORDAN8:18; :: thesis:

end;

hence [(i2 -' 1),j2] in Indices (Gauge (C,n)) by A205, A206, A217, MATRIX_0:30; :: thesis:

end;

hereby :: thesis:

assume A226: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

now :: thesis:

assume j2 + 1 > len (Gauge (C,n)) ; :: thesis:
then A227: (len (Gauge (C,n))) + 1 <= j2 + 1 by NAT_1:13;
j2 + 1 <= (len (Gauge (C,n))) + 1 by A2, A206, XREAL_1:6;
then j2 + 1 = (len (Gauge (C,n))) + 1 by A227, XXREAL_0:1;
then cell ((Gauge (C,n)),i2,(len (Gauge (C,n)))) meets C by A194, A199, A200, A201, A202, A197, A226, GOBRD13:36;
hence contradiction by A203, JORDAN8:15; :: thesis:

end;

hence [i2,(j2 + 1)] in Indices (Gauge (C,n)) by A2, A211, A203, A214, MATRIX_0:30; :: thesis:

end;

hereby :: thesis:

assume A228: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

now :: thesis:

assume j2 -' 1 < 1 ; :: thesis:
then j2 <= 1 by NAT_1:14, NAT_D:36;
then j2 = 1 by A205, XXREAL_0:1;
then cell ((Gauge (C,n)),(i2 -' 1),(1 -' 1)) meets C by A194, A199, A200, A201, A202, A197, A228, GOBRD13:38;
then cell ((Gauge (C,n)),(i2 -' 1),0) meets C by XREAL_1:232;
hence contradiction by A203, JORDAN8:17, NAT_D:44; :: thesis:

end;

hence [i2,(j2 -' 1)] in Indices (Gauge (C,n)) by A211, A203, A212, MATRIX_0:30; :: thesis:

end;

hereby :: thesis:

assume A229: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

now :: thesis:

assume i2 + 1 > len (Gauge (C,n)) ; :: thesis:
then A230: (len (Gauge (C,n))) + 1 <= i2 + 1 by NAT_1:13;
i2 + 1 <= (len (Gauge (C,n))) + 1 by A203, XREAL_1:6;
then i2 + 1 = (len (Gauge (C,n))) + 1 by A230, XXREAL_0:1;
then cell ((Gauge (C,n)),(len (Gauge (C,n))),(j2 -' 1)) meets C by A194, A199, A200, A201, A202, A197, A229, GOBRD13:40;
hence contradiction by A2, A206, JORDAN8:16, NAT_D:44; :: thesis:

end;

hence [(i2 + 1),j2] in Indices (Gauge (C,n)) by A205, A206, A204, MATRIX_0:30; :: thesis:

end;

defpred S₄[ Nat] means ( F . $1 is_sequence_on Gauge (C,n) & ( for m being Nat st 1 <= m & m + 1 <= len (F . $1) holds
( left_cell ((F . $1),m,(Gauge (C,n))) misses C & right_cell ((F . $1),m,(Gauge (C,n))) meets C ) ) );
A231: len (Gauge (C,n)) = (2 |^ n) + 3 by JORDAN8:def 1;
A232: for k being Nat st S₄[k] holds
S₄[k + 1]

proof

A233: 2 |^ n > 0 by NEWTON:83;
A234: 1 <= len (Gauge (C,n)) by A231, NAT_1:12;
let k be Nat; :: thesis:
assume that
A235: F . k is_sequence_on Gauge (C,n) and
A236: for m being Nat st 1 <= m & m + 1 <= len (F . k) holds
( left_cell ((F . k),m,(Gauge (C,n))) misses C & right_cell ((F . k),m,(Gauge (C,n))) meets C ) ; :: thesis:
A237: len (F . k) = k by A192;
A238: len (F . (k + 1)) = k + 1 by A192;

per cases by NAT_1:25;

suppose A239: k = 0 ; :: thesis:

then consider i being Nat such that
A240: 1 <= i and
A241: i + 1 <= len (Gauge (C,n)) and
N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) and
N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) and
A242: F . (k + 1) = <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> by A171;
i < len (Gauge (C,n)) by A241, NAT_1:13;
then A243: [i,(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A2, A234, A240, MATRIX_0:30;

A244: now :: thesis:

let l be Nat; :: thesis:
assume l in dom (F . (k + 1)) ; :: thesis:
then ( 1 <= l & l <= 1 ) by A238, A239, FINSEQ_3:25;
then l = 1 by XXREAL_0:1;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & (F . (k + 1)) /. l = (Gauge (C,n)) * (i,j) ) by A2, A242, A243, FINSEQ_4:16; :: thesis:

end;

now :: thesis:

let l be Nat; :: thesis:
assume that
A245: l in dom (F . (k + 1)) and
A246: l + 1 in dom (F . (k + 1)) ; :: thesis:
( 1 <= l & l <= 1 ) by A238, A239, A245, FINSEQ_3:25;
then l = 1 by XXREAL_0:1;
hence for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (Gauge (C,n)) & [i2,j2] in Indices (Gauge (C,n)) & (F . (k + 1)) /. l = (Gauge (C,n)) * (i1,j1) & (F . (k + 1)) /. (l + 1) = (Gauge (C,n)) * (i2,j2) holds
|.(i1 - i2).| + |.(j1 - j2).| = 1 by A238, A239, A246, FINSEQ_3:25; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A244, GOBOARD1:def 9; :: thesis:
let m be Nat; :: thesis:
assume that
A247: 1 <= m and
A248: m + 1 <= len (F . (k + 1)) ; :: thesis:
1 <= m + 1 by NAT_1:12;
then m + 1 = 0 + 1 by A238, A239, A248, XXREAL_0:1;
hence ( left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) by A247; :: thesis:

end;

suppose A249: k = 1 ; :: thesis:

then consider i being Nat such that
A250: 1 <= i and
A251: i + 1 <= len (Gauge (C,n)) and
A252: N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) and
N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) and
A253: F . (k + 1) = <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))))*> by A171;
A254: i < len (Gauge (C,n)) by A251, NAT_1:13;
then A255: [i,(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A2, A234, A250, MATRIX_0:30;
1 <= i + 1 by A250, NAT_1:13;
then A256: [(i + 1),(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A2, A234, A251, MATRIX_0:30;
A257: ( (F . (k + 1)) /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) & (F . (k + 1)) /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) ) by A253, FINSEQ_4:17;

A258: now :: thesis:

let l be Nat; :: thesis:
assume that
A259: l in dom (F . (k + 1)) and
A260: l + 1 in dom (F . (k + 1)) ; :: thesis:
l <= 2 by A238, A249, A259, FINSEQ_3:25;
then A261: not not l = 0 & ... & not l = 2 ;
let i1, j1, i2, j2 be Nat; :: thesis:
assume A262: ( [i1,j1] in Indices (Gauge (C,n)) & [i2,j2] in Indices (Gauge (C,n)) & (F . (k + 1)) /. l = (Gauge (C,n)) * (i1,j1) & (F . (k + 1)) /. (l + 1) = (Gauge (C,n)) * (i2,j2) ) ; :: thesis:
( j1 = len (Gauge (C,n)) & j2 = len (Gauge (C,n)) ) by A2, A238, A249, A257, A255, A256, A259, A260, A261, A262, FINSEQ_3:25, GOBOARD1:5;
then A263: |.(j1 - j2).| = 0 by ABSVALUE:def 1;
( i1 = i & i2 = i + 1 ) by A2, A238, A249, A257, A255, A256, A259, A260, A261, A262, FINSEQ_3:25, GOBOARD1:5;
then |.(i2 - i1).| = 1 by ABSVALUE:def 1;
hence |.(i1 - i2).| + |.(j1 - j2).| = 1 by A263, UNIFORM1:11; :: thesis:

end;

now :: thesis:

let l be Nat; :: thesis:
assume A264: l in dom (F . (k + 1)) ; :: thesis:
then l <= 2 by A238, A249, FINSEQ_3:25;
then not not l = 0 & ... & not l = 2 ;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & (F . (k + 1)) /. l = (Gauge (C,n)) * (i,j) ) by A2, A257, A255, A256, A264, FINSEQ_3:25; :: thesis:

end;

hence A265: F . (k + 1) is_sequence_on Gauge (C,n) by A258, GOBOARD1:def 9; :: thesis:
A266: ( i < i + 1 & i + 1 < (i + 1) + 1 ) by NAT_1:13;
let m be Nat; :: thesis:
assume that
A267: 1 <= m and
A268: m + 1 <= len (F . (k + 1)) ; :: thesis:
1 + 1 <= m + 1 by A267, XREAL_1:6;
then A269: m + 1 = 1 + 1 by A238, A249, A268, XXREAL_0:1;
then A270: left_cell ((F . (k + 1)),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) by A2, A257, A255, A256, A265, A268, A266, GOBRD13:def 3;

now :: thesis:

N-bound C > S-bound C by JORDAN8:9;
then (N-bound C) - (S-bound C) > (S-bound C) - (S-bound C) by XREAL_1:9;
then ((N-bound C) - (S-bound C)) / (2 |^ n) > 0 by A233, XREAL_1:139;
then A271: (N-bound C) + 0 < (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) by XREAL_1:6;
[1,(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A2, A234, MATRIX_0:30;
then (Gauge (C,n)) * (1,(len (Gauge (C,n)))) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2)))]| by JORDAN8:def 1;
then A272: ((Gauge (C,n)) * (1,(len (Gauge (C,n))))) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2)) by EUCLID:52;
A273: cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) = { |[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))))) `2 <= s ) } by A2, A250, A254, GOBRD11:31;
assume left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ; :: thesis:
then consider p being object such that
A274: p in cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) and
A275: p in C by A270, XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A274;
reconsider p = p as Element of (TOP-REAL 2) ;
A276: p `2 <= N-bound C by A275, PSCOMP_1:24;
consider r, s being Real such that
A277: p = |[r,s]| and
((Gauge (C,n)) * (i,1)) `1 <= r and
r <= ((Gauge (C,n)) * ((i + 1),1)) `1 and
A278: ((Gauge (C,n)) * (1,(len (Gauge (C,n))))) `2 <= s by A274, A273;
(((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2) = ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (2 |^ n)) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * 1) by A231
.= ((N-bound C) - (S-bound C)) + (((N-bound C) - (S-bound C)) / (2 |^ n)) by A233, XCMPLX_1:87 ;
then N-bound C < s by A278, A272, A271, XXREAL_0:2;
hence contradiction by A277, A276, EUCLID:52; :: thesis:

end;

hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C ; :: thesis:
( N-min C in C & N-min C in right_cell ((F . (k + 1)),m,(Gauge (C,n))) ) by A2, A252, A257, A255, A256, A265, A268, A269, A266, GOBRD13:def 2, SPRECT_1:11;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by XBOOLE_0:3; :: thesis:

end;

suppose A279: k > 1 ; :: thesis:

then A280: len (F . k) in dom (F . k) by A237, FINSEQ_3:25;
A281: ((len (F . k)) -' 1) + 1 = len (F . k) by A237, A279, XREAL_1:235;
A282: 1 <= (len (F . k)) -' 1 by A237, A279, NAT_D:49;
then consider i1, j1, i2, j2 being Nat such that
A283: [i1,j1] in Indices (Gauge (C,n)) and
A284: (F . k) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) and
A285: [i2,j2] in Indices (Gauge (C,n)) and
A286: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) and
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A235, A281, JORDAN8:3;
A287: ( i1 = i2 & j1 + 1 = j2 implies [(i2 + 1),j2] in Indices (Gauge (C,n)) ) by A193, A235, A236, A279, A283, A284, A285, A286;
A288: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 = i2 + 1 & j1 = j2 implies [i2,(j2 -' 1)] in Indices (Gauge (C,n)) ) by A193, A235, A236, A279, A283, A284, A285, A286;
A289: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 + 1 = i2 & j1 = j2 implies [i2,(j2 + 1)] in Indices (Gauge (C,n)) ) by A193, A235, A236, A279, A283, A284, A285, A286;
A290: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 = i2 & j1 + 1 = j2 implies [(i2 -' 1),j2] in Indices (Gauge (C,n)) ) by A193, A235, A236, A279, A283, A284, A285, A286;
A291: ( front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 = i2 & j1 = j2 + 1 implies [i2,(j2 -' 1)] in Indices (Gauge (C,n)) ) by A193, A235, A236, A279, A283, A284, A285, A286;
A292: ( i1 = i2 + 1 & j1 = j2 implies [i2,(j2 + 1)] in Indices (Gauge (C,n)) ) by A193, A235, A236, A279, A283, A284, A285, A286;
A293: ( i1 + 1 = i2 & j1 = j2 implies [i2,(j2 -' 1)] in Indices (Gauge (C,n)) ) by A193, A235, A236, A279, A283, A284, A285, A286;
A294: 1 <= j2 by A285, MATRIX_0:32;
A295: right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C by A236, A282, A281;
A296: ( front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 = i2 + 1 & j1 = j2 implies [(i2 -' 1),j2] in Indices (Gauge (C,n)) ) by A193, A235, A236, A279, A283, A284, A285, A286;
A297: ( front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 + 1 = i2 & j1 = j2 implies [(i2 + 1),j2] in Indices (Gauge (C,n)) ) by A193, A235, A236, A279, A283, A284, A285, A286;
A298: ( front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 = i2 & j1 + 1 = j2 implies [i2,(j2 + 1)] in Indices (Gauge (C,n)) ) by A193, A235, A236, A279, A283, A284, A285, A286;
A299: ( i1 = i2 & j1 = j2 + 1 implies [(i2 -' 1),j2] in Indices (Gauge (C,n)) ) by A193, A235, A236, A279, A283, A284, A285, A286;
A300: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C & i1 = i2 & j1 = j2 + 1 implies [(i2 + 1),j2] in Indices (Gauge (C,n)) ) by A193, A235, A236, A279, A283, A284, A285, A286;
(len (F . k)) -' 1 <= len (F . k) by NAT_D:35;
then A301: (len (F . k)) -' 1 in dom (F . k) by A282, FINSEQ_3:25;
A302: 1 <= i2 by A285, MATRIX_0:32;
thus A303: F . (k + 1) is_sequence_on Gauge (C,n) :: thesis:

proof

per cases ;

suppose ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C ) ; :: thesis:

then consider i, j being Nat such that
A304: (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_right (len (F . k)) -' 1, Gauge (C,n) and
A305: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A171, A235, A237, A279, A295;
thus F . (k + 1) is_sequence_on Gauge (C,n) :: thesis:

proof

set f = (F . k) ^ <*((Gauge (C,n)) * (i,j))*>;
A306: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i,j) by FINSEQ_4:67;
A307: ( ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) & ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) ) by A284, A286, A301, A280, FINSEQ_4:68;

per cases by A281, A283, A285, A304, A307;

suppose that A308: ( i1 = i2 & j1 + 1 = j2 ) and
A309: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * ((i2 + 1),j2) ; :: thesis:

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume A310: ( [i19,j19] in Indices (Gauge (C,n)) & [i29,j29] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) & (Gauge (C,n)) * ((i2 + 1),j2) = (Gauge (C,n)) * (i29,j29) ) ; :: thesis:
then ( j2 = j19 & j2 = j29 ) by A285, A286, A287, A308, GOBOARD1:5;
then A311: |.(j29 - j19).| = 0 by ABSVALUE:def 1;
( i2 = i19 & i2 + 1 = i29 ) by A285, A286, A287, A308, A310, GOBOARD1:5;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A311, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A235, A237, A279, A287, A305, A306, A308, A309, CARD_1:27, JORDAN8:6; :: thesis:

end;

suppose that A312: ( i1 + 1 = i2 & j1 = j2 ) and
A313: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i2,(j2 -' 1)) ; :: thesis:

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume A314: ( [i19,j19] in Indices (Gauge (C,n)) & [i29,j29] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) & (Gauge (C,n)) * (i2,(j2 -' 1)) = (Gauge (C,n)) * (i29,j29) ) ; :: thesis:
then ( j2 = j19 & j2 -' 1 = j29 ) by A285, A286, A293, A312, GOBOARD1:5;
then j19 - j29 = j2 - (j2 - 1) by A294, XREAL_1:233;
then A315: |.(j19 - j29).| = 1 by ABSVALUE:def 1;
( i2 = i19 & i2 = i29 ) by A285, A286, A293, A312, A314, GOBOARD1:5;
then |.(i29 - i19).| = 0 by ABSVALUE:def 1;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A315, UNIFORM1:11; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A235, A237, A279, A293, A305, A306, A312, A313, CARD_1:27, JORDAN8:6; :: thesis:

end;

suppose that A316: ( i1 = i2 + 1 & j1 = j2 ) and
A317: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i2,(j2 + 1)) ; :: thesis:

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume A318: ( [i19,j19] in Indices (Gauge (C,n)) & [i29,j29] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) & (Gauge (C,n)) * (i2,(j2 + 1)) = (Gauge (C,n)) * (i29,j29) ) ; :: thesis:
then ( i2 = i19 & i2 = i29 ) by A285, A286, A292, A316, GOBOARD1:5;
then A319: |.(i29 - i19).| = 0 by ABSVALUE:def 1;
( j2 = j19 & j2 + 1 = j29 ) by A285, A286, A292, A316, A318, GOBOARD1:5;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A319, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A235, A237, A279, A292, A305, A306, A316, A317, CARD_1:27, JORDAN8:6; :: thesis:

end;

suppose that A320: ( i1 = i2 & j1 = j2 + 1 ) and
A321: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * ((i2 -' 1),j2) ; :: thesis:

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume A322: ( [i19,j19] in Indices (Gauge (C,n)) & [i29,j29] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) & (Gauge (C,n)) * ((i2 -' 1),j2) = (Gauge (C,n)) * (i29,j29) ) ; :: thesis:
then ( i2 = i19 & i2 -' 1 = i29 ) by A285, A286, A299, A320, GOBOARD1:5;
then i19 - i29 = i2 - (i2 - 1) by A302, XREAL_1:233;
then A323: |.(i19 - i29).| = 1 by ABSVALUE:def 1;
( j2 = j19 & j2 = j29 ) by A285, A286, A299, A320, A322, GOBOARD1:5;
then |.(j29 - j19).| = 0 by ABSVALUE:def 1;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A323, UNIFORM1:11; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A235, A237, A279, A299, A305, A306, A320, A321, CARD_1:27, JORDAN8:6; :: thesis:

end;

suppose A324: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ) ; :: thesis:

then consider i, j being Nat such that
A325: (F . k) ^ <*((Gauge (C,n)) * (i,j))*> goes_straight (len (F . k)) -' 1, Gauge (C,n) and
A326: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A171, A235, A237, A279, A295;
thus F . (k + 1) is_sequence_on Gauge (C,n) :: thesis:

proof

set f = (F . k) ^ <*((Gauge (C,n)) * (i,j))*>;
A327: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i,j) by FINSEQ_4:67;
A328: ( ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) & ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) ) by A284, A286, A301, A280, FINSEQ_4:68;

per cases by A281, A283, A285, A325, A328;

suppose that A329: ( i1 = i2 & j1 + 1 = j2 ) and
A330: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i2,(j2 + 1)) ; :: thesis:

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume A331: ( [i19,j19] in Indices (Gauge (C,n)) & [i29,j29] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) & (Gauge (C,n)) * (i2,(j2 + 1)) = (Gauge (C,n)) * (i29,j29) ) ; :: thesis:
then ( i2 = i19 & i2 = i29 ) by A285, A286, A298, A324, A329, GOBOARD1:5;
then A332: |.(i29 - i19).| = 0 by ABSVALUE:def 1;
( j2 = j19 & j2 + 1 = j29 ) by A285, A286, A298, A324, A329, A331, GOBOARD1:5;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A332, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A235, A237, A279, A298, A324, A326, A327, A329, A330, CARD_1:27, JORDAN8:6; :: thesis:

end;

suppose that A333: ( i1 + 1 = i2 & j1 = j2 ) and
A334: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * ((i2 + 1),j2) ; :: thesis:

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume A335: ( [i19,j19] in Indices (Gauge (C,n)) & [i29,j29] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) & (Gauge (C,n)) * ((i2 + 1),j2) = (Gauge (C,n)) * (i29,j29) ) ; :: thesis:
then ( j2 = j19 & j2 = j29 ) by A285, A286, A297, A324, A333, GOBOARD1:5;
then A336: |.(j29 - j19).| = 0 by ABSVALUE:def 1;
( i2 = i19 & i2 + 1 = i29 ) by A285, A286, A297, A324, A333, A335, GOBOARD1:5;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A336, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A235, A237, A279, A297, A324, A326, A327, A333, A334, CARD_1:27, JORDAN8:6; :: thesis:

end;

suppose that A337: ( i1 = i2 + 1 & j1 = j2 ) and
A338: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * ((i2 -' 1),j2) ; :: thesis:

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume A339: ( [i19,j19] in Indices (Gauge (C,n)) & [i29,j29] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) & (Gauge (C,n)) * ((i2 -' 1),j2) = (Gauge (C,n)) * (i29,j29) ) ; :: thesis:
then ( i2 = i19 & i2 -' 1 = i29 ) by A285, A286, A296, A324, A337, GOBOARD1:5;
then i19 - i29 = i2 - (i2 - 1) by A302, XREAL_1:233;
then A340: |.(i19 - i29).| = 1 by ABSVALUE:def 1;
( j2 = j19 & j2 = j29 ) by A285, A286, A296, A324, A337, A339, GOBOARD1:5;
then |.(j29 - j19).| = 0 by ABSVALUE:def 1;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A340, UNIFORM1:11; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A235, A237, A279, A296, A324, A326, A327, A337, A338, CARD_1:27, JORDAN8:6; :: thesis:

end;

suppose that A341: ( i1 = i2 & j1 = j2 + 1 ) and
A342: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i2,(j2 -' 1)) ; :: thesis:

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume A343: ( [i19,j19] in Indices (Gauge (C,n)) & [i29,j29] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) & (Gauge (C,n)) * (i2,(j2 -' 1)) = (Gauge (C,n)) * (i29,j29) ) ; :: thesis:
then ( j2 = j19 & j2 -' 1 = j29 ) by A285, A286, A291, A324, A341, GOBOARD1:5;
then j19 - j29 = j2 - (j2 - 1) by A294, XREAL_1:233;
then A344: |.(j19 - j29).| = 1 by ABSVALUE:def 1;
( i2 = i19 & i2 = i29 ) by A285, A286, A291, A324, A341, A343, GOBOARD1:5;
then |.(i29 - i19).| = 0 by ABSVALUE:def 1;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A344, UNIFORM1:11; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A235, A237, A279, A291, A324, A326, A327, A341, A342, CARD_1:27, JORDAN8:6; :: thesis:

end;

suppose A345: front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ; :: thesis:

then consider i, j being Nat such that
A346: (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_left (len (F . k)) -' 1, Gauge (C,n) and
A347: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A171, A235, A237, A279, A295;
thus F . (k + 1) is_sequence_on Gauge (C,n) :: thesis:

proof

set f = (F . k) ^ <*((Gauge (C,n)) * (i,j))*>;
A348: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i,j) by FINSEQ_4:67;
A349: ( ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) & ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) ) by A284, A286, A301, A280, FINSEQ_4:68;

per cases by A281, A283, A285, A346, A349;

suppose that A350: ( i1 = i2 & j1 + 1 = j2 ) and
A351: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * ((i2 -' 1),j2) ; :: thesis:

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume A352: ( [i19,j19] in Indices (Gauge (C,n)) & [i29,j29] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) & (Gauge (C,n)) * ((i2 -' 1),j2) = (Gauge (C,n)) * (i29,j29) ) ; :: thesis:
then ( i2 = i19 & i2 -' 1 = i29 ) by A285, A286, A290, A345, A350, GOBOARD1:5;
then i19 - i29 = i2 - (i2 - 1) by A302, XREAL_1:233;
then A353: |.(i19 - i29).| = 1 by ABSVALUE:def 1;
( j2 = j19 & j2 = j29 ) by A285, A286, A290, A345, A350, A352, GOBOARD1:5;
then |.(j29 - j19).| = 0 by ABSVALUE:def 1;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A353, UNIFORM1:11; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A235, A237, A279, A290, A345, A347, A348, A350, A351, CARD_1:27, JORDAN8:6; :: thesis:

end;

suppose that A354: ( i1 + 1 = i2 & j1 = j2 ) and
A355: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i2,(j2 + 1)) ; :: thesis:

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume A356: ( [i19,j19] in Indices (Gauge (C,n)) & [i29,j29] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) & (Gauge (C,n)) * (i2,(j2 + 1)) = (Gauge (C,n)) * (i29,j29) ) ; :: thesis:
then ( i2 = i19 & i2 = i29 ) by A285, A286, A289, A345, A354, GOBOARD1:5;
then A357: |.(i29 - i19).| = 0 by ABSVALUE:def 1;
( j2 = j19 & j2 + 1 = j29 ) by A285, A286, A289, A345, A354, A356, GOBOARD1:5;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A357, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A235, A237, A279, A289, A345, A347, A348, A354, A355, CARD_1:27, JORDAN8:6; :: thesis:

end;

suppose that A358: ( i1 = i2 + 1 & j1 = j2 ) and
A359: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i2,(j2 -' 1)) ; :: thesis:

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume A360: ( [i19,j19] in Indices (Gauge (C,n)) & [i29,j29] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) & (Gauge (C,n)) * (i2,(j2 -' 1)) = (Gauge (C,n)) * (i29,j29) ) ; :: thesis:
then ( j2 = j19 & j2 -' 1 = j29 ) by A285, A286, A288, A345, A358, GOBOARD1:5;
then j19 - j29 = j2 - (j2 - 1) by A294, XREAL_1:233;
then A361: |.(j19 - j29).| = 1 by ABSVALUE:def 1;
( i2 = i19 & i2 = i29 ) by A285, A286, A288, A345, A358, A360, GOBOARD1:5;
then |.(i29 - i19).| = 0 by ABSVALUE:def 1;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A361, UNIFORM1:11; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A235, A237, A279, A288, A345, A347, A348, A358, A359, CARD_1:27, JORDAN8:6; :: thesis:

end;

suppose that A362: ( i1 = i2 & j1 = j2 + 1 ) and
A363: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * ((i2 + 1),j2) ; :: thesis:

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume A364: ( [i19,j19] in Indices (Gauge (C,n)) & [i29,j29] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) & (Gauge (C,n)) * ((i2 + 1),j2) = (Gauge (C,n)) * (i29,j29) ) ; :: thesis:
then ( j2 = j19 & j2 = j29 ) by A285, A286, A300, A345, A362, GOBOARD1:5;
then A365: |.(j29 - j19).| = 0 by ABSVALUE:def 1;
( i2 = i19 & i2 + 1 = i29 ) by A285, A286, A300, A345, A362, A364, GOBOARD1:5;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A365, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A235, A237, A279, A300, A345, A347, A348, A362, A363, CARD_1:27, JORDAN8:6; :: thesis:

end;

let m be Nat; :: thesis:
assume that
A366: 1 <= m and
A367: m + 1 <= len (F . (k + 1)) ; :: thesis:
A368: left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C by A236, A282, A281;

now :: thesis:

per cases ;

suppose A369: m + 1 = len (F . (k + 1)) ; :: thesis:

A370: (j2 -' 1) + 1 = j2 by A294, XREAL_1:235;
A371: (i2 -' 1) + 1 = i2 by A302, XREAL_1:235;
thus ( left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) :: thesis:

proof

per cases ;

suppose A372: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C ) ; :: thesis:

then A373: ex i, j being Nat st
( (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_right (len (F . k)) -' 1, Gauge (C,n) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A171, A235, A237, A279, A295;
then A374: (F . (k + 1)) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) by A286, A280, FINSEQ_4:68;
A375: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) by A284, A301, A373, FINSEQ_4:68;

now :: thesis:

per cases by A281, A283, A285, A373, A375, A374;

suppose that A376: ( i1 = i2 & j1 + 1 = j2 ) and
A377: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * ((i2 + 1),j2) ; :: thesis:

front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j2) by A235, A282, A281, A283, A284, A285, A286, A376, GOBRD13:35;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A237, A238, A285, A287, A303, A366, A369, A372, A374, A376, A377, GOBRD13:23; :: thesis:
( j2 -' 1 = j1 & cell ((Gauge (C,n)),i1,j1) meets C ) by A235, A282, A281, A283, A284, A285, A286, A295, A376, GOBRD13:22, NAT_D:34;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A237, A238, A285, A287, A303, A366, A369, A374, A376, A377, GOBRD13:24; :: thesis:

end;

suppose that A378: ( i1 + 1 = i2 & j1 = j2 ) and
A379: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i2,(j2 -' 1)) ; :: thesis:

front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A235, A282, A281, A283, A284, A285, A286, A378, GOBRD13:37;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A237, A238, A285, A293, A303, A366, A369, A370, A372, A374, A378, A379, GOBRD13:27; :: thesis:
( i2 -' 1 = i1 & cell ((Gauge (C,n)),i1,(j1 -' 1)) meets C ) by A235, A282, A281, A283, A284, A285, A286, A295, A378, GOBRD13:24, NAT_D:34;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A237, A238, A285, A293, A303, A366, A369, A370, A374, A378, A379, GOBRD13:28; :: thesis:

end;

suppose that A380: ( i1 = i2 + 1 & j1 = j2 ) and
A381: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i2,(j2 + 1)) ; :: thesis:

front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),j2) by A235, A282, A281, A283, A284, A285, A286, A380, GOBRD13:39;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A237, A238, A285, A292, A303, A366, A369, A372, A374, A380, A381, GOBRD13:21; :: thesis:
cell ((Gauge (C,n)),i2,j2) meets C by A235, A282, A281, A283, A284, A285, A286, A295, A380, GOBRD13:26;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A237, A238, A285, A292, A303, A366, A369, A374, A380, A381, GOBRD13:22; :: thesis:

end;

suppose that A382: ( i1 = i2 & j1 = j2 + 1 ) and
A383: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * ((i2 -' 1),j2) ; :: thesis:

front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) by A235, A282, A281, A283, A284, A285, A286, A382, GOBRD13:41;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A237, A238, A285, A299, A303, A366, A369, A371, A372, A374, A382, A383, GOBRD13:25; :: thesis:
cell ((Gauge (C,n)),(i2 -' 1),j2) meets C by A235, A282, A281, A283, A284, A285, A286, A295, A382, GOBRD13:28;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A237, A238, A285, A299, A303, A366, A369, A371, A374, A382, A383, GOBRD13:26; :: thesis:

end;

hence ( left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) ; :: thesis:

end;

suppose A384: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ) ; :: thesis:

then A385: ex i, j being Nat st
( (F . k) ^ <*((Gauge (C,n)) * (i,j))*> goes_straight (len (F . k)) -' 1, Gauge (C,n) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A171, A235, A237, A279, A295;
then A386: (F . (k + 1)) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) by A286, A280, FINSEQ_4:68;
A387: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) by A284, A301, A385, FINSEQ_4:68;

now :: thesis:

per cases by A281, A283, A285, A385, A387, A386;

suppose that A388: ( i1 = i2 & j1 + 1 = j2 ) and
A389: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i2,(j2 + 1)) ; :: thesis:

front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j2) by A235, A282, A281, A283, A284, A285, A286, A388, GOBRD13:34;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A237, A238, A285, A298, A303, A366, A369, A384, A386, A388, A389, GOBRD13:21; :: thesis:
front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j2) by A235, A282, A281, A283, A284, A285, A286, A388, GOBRD13:35;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A237, A238, A285, A298, A303, A366, A369, A384, A386, A388, A389, GOBRD13:22; :: thesis:

end;

suppose that A390: ( i1 + 1 = i2 & j1 = j2 ) and
A391: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * ((i2 + 1),j2) ; :: thesis:

front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) by A235, A282, A281, A283, A284, A285, A286, A390, GOBRD13:36;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A237, A238, A285, A297, A303, A366, A369, A384, A386, A390, A391, GOBRD13:23; :: thesis:
front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A235, A282, A281, A283, A284, A285, A286, A390, GOBRD13:37;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A237, A238, A285, A297, A303, A366, A369, A384, A386, A390, A391, GOBRD13:24; :: thesis:

end;

suppose that A392: ( i1 = i2 + 1 & j1 = j2 ) and
A393: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * ((i2 -' 1),j2) ; :: thesis:

front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) by A235, A282, A281, A283, A284, A285, A286, A392, GOBRD13:38;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A237, A238, A285, A296, A303, A366, A369, A371, A384, A386, A392, A393, GOBRD13:25; :: thesis:
front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),j2) by A235, A282, A281, A283, A284, A285, A286, A392, GOBRD13:39;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A237, A238, A285, A296, A303, A366, A369, A371, A384, A386, A392, A393, GOBRD13:26; :: thesis:

end;

suppose that A394: ( i1 = i2 & j1 = j2 + 1 ) and
A395: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i2,(j2 -' 1)) ; :: thesis:

front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A235, A282, A281, A283, A284, A285, A286, A394, GOBRD13:40;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A237, A238, A285, A291, A303, A366, A369, A370, A384, A386, A394, A395, GOBRD13:27; :: thesis:
front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) by A235, A282, A281, A283, A284, A285, A286, A394, GOBRD13:41;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A237, A238, A285, A291, A303, A366, A369, A370, A384, A386, A394, A395, GOBRD13:28; :: thesis:

end;

hence ( left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) ; :: thesis:

end;

suppose A396: front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ; :: thesis:

then A397: ex i, j being Nat st
( (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_left (len (F . k)) -' 1, Gauge (C,n) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A171, A235, A237, A279, A295;
then A398: (F . (k + 1)) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) by A286, A280, FINSEQ_4:68;
A399: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) by A284, A301, A397, FINSEQ_4:68;

now :: thesis:

per cases by A281, A283, A285, A397, A399, A398;

suppose that A400: ( i1 = i2 & j1 + 1 = j2 ) and
A401: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * ((i2 -' 1),j2) ; :: thesis:

( j2 -' 1 = j1 & cell ((Gauge (C,n)),(i1 -' 1),j1) misses C ) by A235, A282, A281, A283, A284, A285, A286, A368, A400, GOBRD13:21, NAT_D:34;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A237, A238, A285, A290, A303, A366, A369, A371, A396, A398, A400, A401, GOBRD13:25; :: thesis:
front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j2) by A235, A282, A281, A283, A284, A285, A286, A400, GOBRD13:34;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A237, A238, A285, A290, A303, A366, A369, A371, A396, A398, A400, A401, GOBRD13:26; :: thesis:

end;

suppose that A402: ( i1 + 1 = i2 & j1 = j2 ) and
A403: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i2,(j2 + 1)) ; :: thesis:

( i2 -' 1 = i1 & cell ((Gauge (C,n)),i1,j1) misses C ) by A235, A282, A281, A283, A284, A285, A286, A368, A402, GOBRD13:23, NAT_D:34;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A237, A238, A285, A289, A303, A366, A369, A396, A398, A402, A403, GOBRD13:21; :: thesis:
front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) by A235, A282, A281, A283, A284, A285, A286, A402, GOBRD13:36;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A237, A238, A285, A289, A303, A366, A369, A396, A398, A402, A403, GOBRD13:22; :: thesis:

end;

suppose that A404: ( i1 = i2 + 1 & j1 = j2 ) and
A405: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i2,(j2 -' 1)) ; :: thesis:

cell ((Gauge (C,n)),i2,(j2 -' 1)) misses C by A235, A282, A281, A283, A284, A285, A286, A368, A404, GOBRD13:25;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A237, A238, A285, A288, A303, A366, A369, A370, A396, A398, A404, A405, GOBRD13:27; :: thesis:
front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) by A235, A282, A281, A283, A284, A285, A286, A404, GOBRD13:38;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A237, A238, A285, A288, A303, A366, A369, A370, A396, A398, A404, A405, GOBRD13:28; :: thesis:

end;

suppose that A406: ( i1 = i2 & j1 = j2 + 1 ) and
A407: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * ((i2 + 1),j2) ; :: thesis:

cell ((Gauge (C,n)),i2,j2) misses C by A235, A282, A281, A283, A284, A285, A286, A368, A406, GOBRD13:27;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A237, A238, A285, A300, A303, A366, A369, A396, A398, A406, A407, GOBRD13:23; :: thesis:
front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A235, A282, A281, A283, A284, A285, A286, A406, GOBRD13:40;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A237, A238, A285, A300, A303, A366, A369, A396, A398, A406, A407, GOBRD13:24; :: thesis:

end;

hence ( left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) ; :: thesis:

end;

suppose m + 1 <> len (F . (k + 1)) ; :: thesis:

then m + 1 < len (F . (k + 1)) by A367, XXREAL_0:1;
then A408: m + 1 <= len (F . k) by A237, A238, NAT_1:13;
then consider i1, j1, i2, j2 being Nat such that
A409: [i1,j1] in Indices (Gauge (C,n)) and
A410: (F . k) /. m = (Gauge (C,n)) * (i1,j1) and
A411: [i2,j2] in Indices (Gauge (C,n)) and
A412: (F . k) /. (m + 1) = (Gauge (C,n)) * (i2,j2) and
A413: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A235, A366, JORDAN8:3;
A414: ( left_cell ((F . k),m,(Gauge (C,n))) misses C & right_cell ((F . k),m,(Gauge (C,n))) meets C ) by A236, A366, A408;

A415: now :: thesis:

per cases ;

suppose ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C ) ; :: thesis:

then consider i, j being Nat such that
(F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_right (len (F . k)) -' 1, Gauge (C,n) and
A416: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A171, A235, A237, A279, A295;
take i = i; :: thesis:
take j = j; :: thesis:
thus F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A416; :: thesis:

end;

suppose ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ) ; :: thesis:

then consider i, j being Nat such that
(F . k) ^ <*((Gauge (C,n)) * (i,j))*> goes_straight (len (F . k)) -' 1, Gauge (C,n) and
A417: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A171, A235, A237, A279, A295;
take i = i; :: thesis:
take j = j; :: thesis:
thus F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A417; :: thesis:

end;

suppose front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ; :: thesis:

then consider i, j being Nat such that
(F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_left (len (F . k)) -' 1, Gauge (C,n) and
A418: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A171, A235, A237, A279, A295;
take i = i; :: thesis:
take j = j; :: thesis:
thus F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A418; :: thesis:

end;

1 <= m + 1 by NAT_1:12;
then m + 1 in dom (F . k) by A408, FINSEQ_3:25;
then A419: (F . (k + 1)) /. (m + 1) = (Gauge (C,n)) * (i2,j2) by A412, A415, FINSEQ_4:68;
m <= len (F . k) by A408, NAT_1:13;
then m in dom (F . k) by A366, FINSEQ_3:25;
then A420: (F . (k + 1)) /. m = (Gauge (C,n)) * (i1,j1) by A410, A415, FINSEQ_4:68;

now :: thesis:

per cases by A413;

suppose A421: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

then ( left_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j1) & right_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) ) by A235, A366, A408, A409, A410, A411, A412, GOBRD13:21, GOBRD13:22;
hence ( left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) by A303, A366, A367, A409, A411, A414, A420, A419, A421, GOBRD13:21, GOBRD13:22; :: thesis:

end;

suppose A422: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

then ( left_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) & right_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,(j1 -' 1)) ) by A235, A366, A408, A409, A410, A411, A412, GOBRD13:23, GOBRD13:24;
hence ( left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) by A303, A366, A367, A409, A411, A414, A420, A419, A422, GOBRD13:23, GOBRD13:24; :: thesis:

end;

suppose A423: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

then ( left_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) & right_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) ) by A235, A366, A408, A409, A410, A411, A412, GOBRD13:25, GOBRD13:26;
hence ( left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) by A303, A366, A367, A409, A411, A414, A420, A419, A423, GOBRD13:25, GOBRD13:26; :: thesis:

end;

suppose A424: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

then ( left_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) & right_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j2) ) by A235, A366, A408, A409, A410, A411, A412, GOBRD13:27, GOBRD13:28;
hence ( left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) by A303, A366, A367, A409, A411, A414, A420, A419, A424, GOBRD13:27, GOBRD13:28; :: thesis:

end;

hence ( left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) ; :: thesis:

end;

hence ( left_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & right_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) ; :: thesis:

end;

defpred S₅[ Nat] means ex w being Nat st
( w = $1 & $1 >= 1 & ex m being Nat st
( m in dom (F . w) & m <> len (F . w) & (F . w) /. m = (F . w) /. (len (F . w)) ) );
A425: S₄[ 0 ]

proof

( ( for n being Nat st n in dom (F . 0) holds
ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & (F . 0) /. n = (Gauge (C,n)) * (i,j) ) ) & ( for n being Nat st n in dom (F . 0) & n + 1 in dom (F . 0) holds
for m, k, i, j being Nat st [m,k] in Indices (Gauge (C,n)) & [i,j] in Indices (Gauge (C,n)) & (F . 0) /. n = (Gauge (C,n)) * (m,k) & (F . 0) /. (n + 1) = (Gauge (C,n)) * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) ) by A170;
hence F . 0 is_sequence_on Gauge (C,n) by GOBOARD1:def 9; :: thesis:
let m be Nat; :: thesis:
assume that
1 <= m and
A426: m + 1 <= len (F . 0) ; :: thesis:
thus ( left_cell ((F . 0),m,(Gauge (C,n))) misses C & right_cell ((F . 0),m,(Gauge (C,n))) meets C ) by A170, A426, CARD_1:27; :: thesis:

end;

A427: for k being Nat holds S₄[k] from NAT_1:sch 2(A425, A232);
A428: for k, i1, i2, j1, j2 being Nat st k > 1 & [i1,j1] in Indices (Gauge (C,n)) & (F . k) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) & [i2,j2] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) holds
( ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C implies ( F . (k + 1) turns_right (len (F . k)) -' 1, Gauge (C,n) & ( i1 = i2 & j1 + 1 = j2 implies ( [(i2 + 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> ) ) & ( i1 + 1 = i2 & j1 = j2 implies ( [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> ) ) & ( i1 = i2 + 1 & j1 = j2 implies ( [i2,(j2 + 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> ) ) & ( i1 = i2 & j1 = j2 + 1 implies ( [(i2 -' 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> ) ) ) ) & ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C implies ( F . (k + 1) goes_straight (len (F . k)) -' 1, Gauge (C,n) & ( i1 = i2 & j1 + 1 = j2 implies ( [i2,(j2 + 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> ) ) & ( i1 + 1 = i2 & j1 = j2 implies ( [(i2 + 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> ) ) & ( i1 = i2 + 1 & j1 = j2 implies ( [(i2 -' 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> ) ) & ( i1 = i2 & j1 = j2 + 1 implies ( [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> ) ) ) ) & ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C implies ( F . (k + 1) turns_left (len (F . k)) -' 1, Gauge (C,n) & ( i1 = i2 & j1 + 1 = j2 implies ( [(i2 -' 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> ) ) & ( i1 + 1 = i2 & j1 = j2 implies ( [i2,(j2 + 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> ) ) & ( i1 = i2 + 1 & j1 = j2 implies ( [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> ) ) & ( i1 = i2 & j1 = j2 + 1 implies ( [(i2 + 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> ) ) ) ) )

proof

let k, i1, i2, j1, j2 be Nat; :: thesis:
assume that
A429: k > 1 and
A430: [i1,j1] in Indices (Gauge (C,n)) and
A431: (F . k) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) and
A432: [i2,j2] in Indices (Gauge (C,n)) and
A433: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) ; :: thesis:
A434: len (F . k) = k by A192;
then A435: ((len (F . k)) -' 1) + 1 = len (F . k) by A429, XREAL_1:235;
A436: 1 <= (len (F . k)) -' 1 by A429, A434, NAT_D:49;
then A437: right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C by A427, A435;
(len (F . k)) -' 1 <= len (F . k) by NAT_D:35;
then A438: (len (F . k)) -' 1 in dom (F . k) by A436, FINSEQ_3:25;
A439: ( j1 + 1 > j1 & j2 + 1 > j2 ) by NAT_1:13;
A440: F . k is_sequence_on Gauge (C,n) by A427;
A441: ( i1 + 1 > i1 & i2 + 1 > i2 ) by NAT_1:13;
A442: len (F . k) in dom (F . k) by A429, A434, FINSEQ_3:25;

hereby :: thesis:

assume ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C ) ; :: thesis:
then consider i, j being Nat such that
A443: (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_right (len (F . k)) -' 1, Gauge (C,n) and
A444: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A171, A429, A440, A434, A437;
thus F . (k + 1) turns_right (len (F . k)) -' 1, Gauge (C,n) by A443, A444; :: thesis:
A445: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i,j) by A444, FINSEQ_4:67;
A446: ( (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) & (F . (k + 1)) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) ) by A431, A433, A438, A442, A444, FINSEQ_4:68;
hence ( i1 = i2 & j1 + 1 = j2 implies ( [(i2 + 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> ) ) by A430, A432, A435, A439, A443, A444, A445; :: thesis:
thus ( i1 + 1 = i2 & j1 = j2 implies ( [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> ) ) by A430, A432, A435, A441, A443, A444, A446, A445; :: thesis:
thus ( i1 = i2 + 1 & j1 = j2 implies ( [i2,(j2 + 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> ) ) by A430, A432, A435, A441, A443, A444, A446, A445; :: thesis:
thus ( i1 = i2 & j1 = j2 + 1 implies ( [(i2 -' 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> ) ) by A430, A432, A435, A439, A443, A444, A446, A445; :: thesis:

end;

hereby :: thesis:

assume ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ) ; :: thesis:
then consider i, j being Nat such that
A447: (F . k) ^ <*((Gauge (C,n)) * (i,j))*> goes_straight (len (F . k)) -' 1, Gauge (C,n) and
A448: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A171, A429, A440, A434, A437;
thus F . (k + 1) goes_straight (len (F . k)) -' 1, Gauge (C,n) by A447, A448; :: thesis:
A449: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i,j) by A448, FINSEQ_4:67;
A450: ( (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) & (F . (k + 1)) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) ) by A431, A433, A438, A442, A448, FINSEQ_4:68;
hence ( i1 = i2 & j1 + 1 = j2 implies ( [i2,(j2 + 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> ) ) by A430, A432, A435, A439, A447, A448, A449; :: thesis:
thus ( i1 + 1 = i2 & j1 = j2 implies ( [(i2 + 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> ) ) by A430, A432, A435, A441, A447, A448, A450, A449; :: thesis:
thus ( i1 = i2 + 1 & j1 = j2 implies ( [(i2 -' 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> ) ) by A430, A432, A435, A441, A447, A448, A450, A449; :: thesis:
thus ( i1 = i2 & j1 = j2 + 1 implies ( [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> ) ) by A430, A432, A435, A439, A447, A448, A450, A449; :: thesis:

end;

assume front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ; :: thesis:
then consider i, j being Nat such that
A451: (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_left (len (F . k)) -' 1, Gauge (C,n) and
A452: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A171, A429, A440, A434, A437;
A453: (F . (k + 1)) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) by A433, A442, A452, FINSEQ_4:68;
thus F . (k + 1) turns_left (len (F . k)) -' 1, Gauge (C,n) by A451, A452; :: thesis:
A454: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i,j) by A452, FINSEQ_4:67;
A455: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) by A431, A438, A452, FINSEQ_4:68;
hence ( i1 = i2 & j1 + 1 = j2 implies ( [(i2 -' 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> ) ) by A430, A432, A435, A439, A451, A452, A453, A454; :: thesis:
thus ( i1 + 1 = i2 & j1 = j2 implies ( [i2,(j2 + 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> ) ) by A430, A432, A435, A441, A451, A452, A455, A453, A454; :: thesis:
thus ( i1 = i2 + 1 & j1 = j2 implies ( [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> ) ) by A430, A432, A435, A441, A451, A452, A455, A453, A454; :: thesis:
thus ( i1 = i2 & j1 = j2 + 1 implies ( [(i2 + 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> ) ) by A430, A432, A435, A439, A451, A452, A455, A453, A454; :: thesis:

end;

A456: for k being Nat st k > 1 holds
( ( front_left_cell ((F . k),(k -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),(k -' 1),(Gauge (C,n))) misses C implies F . (k + 1) turns_right k -' 1, Gauge (C,n) ) & ( front_left_cell ((F . k),(k -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),(k -' 1),(Gauge (C,n))) meets C implies F . (k + 1) goes_straight k -' 1, Gauge (C,n) ) & ( front_left_cell ((F . k),(k -' 1),(Gauge (C,n))) meets C implies F . (k + 1) turns_left k -' 1, Gauge (C,n) ) )

proof

let k be Nat; :: thesis:
assume A457: k > 1 ; :: thesis:
A458: F . k is_sequence_on Gauge (C,n) by A427;
A459: len (F . k) = k by A192;
then ( 1 <= (len (F . k)) -' 1 & ((len (F . k)) -' 1) + 1 = len (F . k) ) by A457, NAT_D:49, XREAL_1:235;
then ex i1, j1, i2, j2 being Nat st
( [i1,j1] in Indices (Gauge (C,n)) & (F . k) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) & [i2,j2] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) ) by A458, JORDAN8:3;
hence ( ( front_left_cell ((F . k),(k -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),(k -' 1),(Gauge (C,n))) misses C implies F . (k + 1) turns_right k -' 1, Gauge (C,n) ) & ( front_left_cell ((F . k),(k -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),(k -' 1),(Gauge (C,n))) meets C implies F . (k + 1) goes_straight k -' 1, Gauge (C,n) ) & ( front_left_cell ((F . k),(k -' 1),(Gauge (C,n))) meets C implies F . (k + 1) turns_left k -' 1, Gauge (C,n) ) ) by A428, A457, A459; :: thesis:

end;

defpred S₆[ Nat] means for m being Nat st m <= $1 holds
(F . $1) | m = F . m;
A460: S₆[ 0 ]

proof

let m be Nat; :: thesis:
assume A461: m <= 0 ; :: thesis:
then (F . 0) | 0 = (F . 0) | m ;
hence (F . 0) | m = F . m by A170, A461; :: thesis:

end;

A462: for k being Nat ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> )

proof

let k be Nat; :: thesis:
A463: F . k is_sequence_on Gauge (C,n) by A427;
A464: len (F . k) = k by A192;
len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A465: ( len (Gauge (C,n)) = width (Gauge (C,n)) & 1 < len (Gauge (C,n)) ) by JORDAN8:def 1, XXREAL_0:2;

per cases by XXREAL_0:1;

suppose A466: k < 1 ; :: thesis:

consider i being Nat such that
A467: 1 <= i and
A468: i + 1 <= len (Gauge (C,n)) and
N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) and
N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) and
A469: F . (0 + 1) = <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> by A171;
take i ; :: thesis:
take j = width (Gauge (C,n)); :: thesis:
i < len (Gauge (C,n)) by A468, NAT_1:13;
hence [i,j] in Indices (Gauge (C,n)) by A465, A467, MATRIX_0:30; :: thesis:
k = 0 by A466, NAT_1:14;
hence F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A170, A469, FINSEQ_1:34; :: thesis:

end;

suppose A470: k = 1 ; :: thesis:

consider i being Nat such that
A471: 1 <= i and
A472: i + 1 <= len (Gauge (C,n)) and
A473: ( N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) ) and
A474: F . (0 + 1) = <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> by A171;
take i + 1 ; :: thesis:
take j = width (Gauge (C,n)); :: thesis:
1 <= i + 1 by A471, NAT_1:13;
hence [(i + 1),j] in Indices (Gauge (C,n)) by A465, A472, MATRIX_0:30; :: thesis:
consider i9 being Nat such that
A475: ( 1 <= i9 & i9 + 1 <= len (Gauge (C,n)) & N-min C in cell ((Gauge (C,n)),i9,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i9,((width (Gauge (C,n))) -' 1)) ) and
A476: F . (1 + 1) = <*((Gauge (C,n)) * (i9,(width (Gauge (C,n))))),((Gauge (C,n)) * ((i9 + 1),(width (Gauge (C,n)))))*> by A171;
i = i9 by A471, A472, A473, A475, Th29;
hence F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i + 1),j))*> by A470, A474, A476, FINSEQ_1:def 9; :: thesis:

end;

suppose A477: k > 1 ; :: thesis:

then ( 1 <= (len (F . k)) -' 1 & ((len (F . k)) -' 1) + 1 = len (F . k) ) by A464, NAT_D:49, XREAL_1:235;
then consider i1, j1, i2, j2 being Nat such that
A478: ( [i1,j1] in Indices (Gauge (C,n)) & (F . k) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) & [i2,j2] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) ) and
A479: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A463, JORDAN8:3;

now :: thesis:

per cases ;

suppose A480: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C ) ; :: thesis:

now :: thesis:

per cases by A479;

suppose ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

then ( [(i2 + 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> ) by A428, A477, A478, A480;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

suppose ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

then ( [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> ) by A428, A477, A478, A480;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

suppose ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

then ( [i2,(j2 + 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> ) by A428, A477, A478, A480;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

suppose ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

then ( [(i2 -' 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> ) by A428, A477, A478, A480;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

suppose A481: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ) ; :: thesis:

now :: thesis:

per cases by A479;

suppose ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

then ( [i2,(j2 + 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> ) by A428, A477, A478, A481;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

suppose ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

then ( [(i2 + 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> ) by A428, A477, A478, A481;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

suppose ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

then ( [(i2 -' 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> ) by A428, A477, A478, A481;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

suppose ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

then ( [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> ) by A428, A477, A478, A481;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

suppose A482: front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ; :: thesis:

now :: thesis:

per cases by A479;

suppose ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

then ( [(i2 -' 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> ) by A428, A477, A478, A482;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

suppose ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

then ( [i2,(j2 + 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> ) by A428, A477, A478, A482;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

suppose ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

then ( [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> ) by A428, A477, A478, A482;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

suppose ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

then ( [(i2 + 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> ) by A428, A477, A478, A482;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ; :: thesis:

end;

A483: for k being Nat st S₆[k] holds
S₆[k + 1]

proof

let k be Nat; :: thesis:
assume A484: for m being Nat st m <= k holds
(F . k) | m = F . m ; :: thesis:
let m be Nat; :: thesis:
assume A485: m <= k + 1 ; :: thesis:

per cases by A485, XXREAL_0:1;

suppose m < k + 1 ; :: thesis:

then A486: m <= k by NAT_1:13;
( len (F . k) = k & ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ) by A192, A462;
then (F . (k + 1)) | m = (F . k) | m by A486, FINSEQ_5:22;
hence (F . (k + 1)) | m = F . m by A484, A486; :: thesis:

end;

suppose A487: m = k + 1 ; :: thesis:

len (F . (k + 1)) = k + 1 by A192;
hence (F . (k + 1)) | m = F . m by A487, FINSEQ_1:58; :: thesis:

end;

A488: for k being Nat holds S₆[k] from NAT_1:sch 2(A460, A483);
defpred S₇[ Nat] means F . $1 is unfolded ;
A489: for k being Nat st S₇[k] holds
S₇[k + 1]

proof

let k be Nat; :: thesis:
assume A490: F . k is unfolded ; :: thesis:
A491: F . k is_sequence_on Gauge (C,n) by A427;

per cases ;

suppose k <= 1 ; :: thesis:

then k + 1 <= 1 + 1 by XREAL_1:6;
then len (F . (k + 1)) <= 2 by A192;
hence S₇[k + 1] by SPPOL_2:26; :: thesis:

end;

suppose A492: k > 1 ; :: thesis:

set m = k -' 1;
A493: (k -' 1) + 1 = k by A492, XREAL_1:235;
A494: len (F . k) = k by A192;
A495: 1 <= k -' 1 by A492, NAT_D:49;
then consider i1, j1, i2, j2 being Nat such that
A496: [i1,j1] in Indices (Gauge (C,n)) and
A497: (F . k) /. (k -' 1) = (Gauge (C,n)) * (i1,j1) and
A498: [i2,j2] in Indices (Gauge (C,n)) and
A499: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) and
A500: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A491, A493, A494, JORDAN8:3;
A501: LSeg ((F . k),(k -' 1)) = LSeg (((Gauge (C,n)) * (i1,j1)),((Gauge (C,n)) * (i2,j2))) by A495, A493, A494, A497, A499, TOPREAL1:def 3;
A502: 1 <= j2 by A498, MATRIX_0:32;
then A503: (j2 -' 1) + 1 = j2 by XREAL_1:235;
A504: 1 <= j1 by A496, MATRIX_0:32;
A505: 1 <= i2 by A498, MATRIX_0:32;
then A506: (i2 -' 1) + 1 = i2 by XREAL_1:235;
A507: i1 <= len (Gauge (C,n)) by A496, MATRIX_0:32;
A508: j2 <= width (Gauge (C,n)) by A498, MATRIX_0:32;
A509: 1 <= i1 by A496, MATRIX_0:32;
A510: j1 <= width (Gauge (C,n)) by A496, MATRIX_0:32;
A511: i2 <= len (Gauge (C,n)) by A498, MATRIX_0:32;

now :: thesis:

per cases ;

suppose A512: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C ) ; :: thesis:

now :: thesis:

per cases by A500;

suppose A513: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

then [(i2 + 1),j2] in Indices (Gauge (C,n)) by A428, A492, A494, A496, A497, A498, A499, A512;
then i2 + 1 <= len (Gauge (C,n)) by MATRIX_0:32;
then A514: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * ((i2 + 1),j2)))) = {((F . k) /. (len (F . k)))} by A499, A509, A504, A508, A501, A513, GOBOARD7:15;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> by A428, A492, A494, A496, A497, A498, A499, A512, A513;
hence S₇[k + 1] by A490, A493, A494, A514, SPPOL_2:30; :: thesis:

end;

suppose A515: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

then [i2,(j2 -' 1)] in Indices (Gauge (C,n)) by A428, A492, A494, A496, A497, A498, A499, A512;
then 1 <= j2 -' 1 by MATRIX_0:32;
then A516: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * (i2,(j2 -' 1))))) = {((F . k) /. (len (F . k)))} by A499, A509, A510, A511, A503, A501, A515, GOBOARD7:16;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> by A428, A492, A494, A496, A497, A498, A499, A512, A515;
hence S₇[k + 1] by A490, A493, A494, A516, SPPOL_2:30; :: thesis:

end;

suppose A517: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

then [i2,(j2 + 1)] in Indices (Gauge (C,n)) by A428, A492, A494, A496, A497, A498, A499, A512;
then j2 + 1 <= width (Gauge (C,n)) by MATRIX_0:32;
then A518: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * (i2,(j2 + 1))))) = {((F . k) /. (len (F . k)))} by A499, A507, A504, A505, A501, A517, GOBOARD7:17;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> by A428, A492, A494, A496, A497, A498, A499, A512, A517;
hence S₇[k + 1] by A490, A493, A494, A518, SPPOL_2:30; :: thesis:

end;

suppose A519: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

then [(i2 -' 1),j2] in Indices (Gauge (C,n)) by A428, A492, A494, A496, A497, A498, A499, A512;
then 1 <= i2 -' 1 by MATRIX_0:32;
then A520: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * ((i2 -' 1),j2)))) = {((F . k) /. (len (F . k)))} by A499, A507, A510, A502, A506, A501, A519, GOBOARD7:18;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> by A428, A492, A494, A496, A497, A498, A499, A512, A519;
hence S₇[k + 1] by A490, A493, A494, A520, SPPOL_2:30; :: thesis:

end;

hence S₇[k + 1] ; :: thesis:

end;

suppose A521: ( front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ) ; :: thesis:

now :: thesis:

per cases by A500;

suppose A522: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

then [i2,(j2 + 1)] in Indices (Gauge (C,n)) by A428, A492, A494, A496, A497, A498, A499, A521;
then A523: j2 + 1 <= width (Gauge (C,n)) by MATRIX_0:32;
j2 + 1 = j1 + (1 + 1) by A522;
then A524: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * (i2,(j2 + 1))))) = {((F . k) /. (len (F . k)))} by A499, A509, A507, A504, A501, A522, A523, GOBOARD7:13;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> by A428, A492, A494, A496, A497, A498, A499, A521, A522;
hence S₇[k + 1] by A490, A493, A494, A524, SPPOL_2:30; :: thesis:

end;

suppose A525: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

then [(i2 + 1),j2] in Indices (Gauge (C,n)) by A428, A492, A494, A496, A497, A498, A499, A521;
then A526: i2 + 1 <= len (Gauge (C,n)) by MATRIX_0:32;
i2 + 1 = i1 + (1 + 1) by A525;
then A527: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * ((i2 + 1),j2)))) = {((F . k) /. (len (F . k)))} by A499, A509, A504, A510, A501, A525, A526, GOBOARD7:14;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> by A428, A492, A494, A496, A497, A498, A499, A521, A525;
hence S₇[k + 1] by A490, A493, A494, A527, SPPOL_2:30; :: thesis:

end;

suppose A528: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

then [(i2 -' 1),j2] in Indices (Gauge (C,n)) by A428, A492, A494, A496, A497, A498, A499, A521;
then A529: 1 <= i2 -' 1 by MATRIX_0:32;
((i2 -' 1) + 1) + 1 = (i2 -' 1) + (1 + 1) ;
then A530: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * ((i2 -' 1),j2)))) = {((F . k) /. (len (F . k)))} by A499, A507, A504, A510, A506, A501, A528, A529, GOBOARD7:14;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> by A428, A492, A494, A496, A497, A498, A499, A521, A528;
hence S₇[k + 1] by A490, A493, A494, A530, SPPOL_2:30; :: thesis:

end;

suppose A531: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

then [i2,(j2 -' 1)] in Indices (Gauge (C,n)) by A428, A492, A494, A496, A497, A498, A499, A521;
then A532: 1 <= j2 -' 1 by MATRIX_0:32;
((j2 -' 1) + 1) + 1 = (j2 -' 1) + (1 + 1) ;
then A533: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * (i2,(j2 -' 1))))) = {((F . k) /. (len (F . k)))} by A499, A509, A507, A510, A503, A501, A531, A532, GOBOARD7:13;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> by A428, A492, A494, A496, A497, A498, A499, A521, A531;
hence S₇[k + 1] by A490, A493, A494, A533, SPPOL_2:30; :: thesis:

end;

hence S₇[k + 1] ; :: thesis:

end;

suppose A534: front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ; :: thesis:

now :: thesis:

per cases by A500;

suppose A535: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

then [(i2 -' 1),j2] in Indices (Gauge (C,n)) by A428, A492, A494, A496, A497, A498, A499, A534;
then 1 <= i2 -' 1 by MATRIX_0:32;
then A536: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * ((i2 -' 1),j2)))) = {((F . k) /. (len (F . k)))} by A499, A507, A504, A508, A506, A501, A535, GOBOARD7:16;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> by A428, A492, A494, A496, A497, A498, A499, A534, A535;
hence S₇[k + 1] by A490, A493, A494, A536, SPPOL_2:30; :: thesis:

end;

suppose A537: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

then [i2,(j2 + 1)] in Indices (Gauge (C,n)) by A428, A492, A494, A496, A497, A498, A499, A534;
then j2 + 1 <= width (Gauge (C,n)) by MATRIX_0:32;
then A538: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * (i2,(j2 + 1))))) = {((F . k) /. (len (F . k)))} by A499, A509, A504, A511, A501, A537, GOBOARD7:18;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> by A428, A492, A494, A496, A497, A498, A499, A534, A537;
hence S₇[k + 1] by A490, A493, A494, A538, SPPOL_2:30; :: thesis:

end;

suppose A539: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

then [i2,(j2 -' 1)] in Indices (Gauge (C,n)) by A428, A492, A494, A496, A497, A498, A499, A534;
then 1 <= j2 -' 1 by MATRIX_0:32;
then A540: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * (i2,(j2 -' 1))))) = {((F . k) /. (len (F . k)))} by A499, A507, A510, A505, A503, A501, A539, GOBOARD7:15;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> by A428, A492, A494, A496, A497, A498, A499, A534, A539;
hence S₇[k + 1] by A490, A493, A494, A540, SPPOL_2:30; :: thesis:

end;

suppose A541: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

then [(i2 + 1),j2] in Indices (Gauge (C,n)) by A428, A492, A494, A496, A497, A498, A499, A534;
then i2 + 1 <= len (Gauge (C,n)) by MATRIX_0:32;
then A542: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * ((i2 + 1),j2)))) = {((F . k) /. (len (F . k)))} by A499, A509, A510, A502, A501, A541, GOBOARD7:17;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> by A428, A492, A494, A496, A497, A498, A499, A534, A541;
hence S₇[k + 1] by A490, A493, A494, A542, SPPOL_2:30; :: thesis:

end;

hence S₇[k + 1] ; :: thesis:

end;

hence S₇[k + 1] ; :: thesis:

end;

now :: thesis:

defpred S₈[ Nat] means F . $1 is one-to-one ;
assume A543: for k being Nat st k >= 1 holds
for m being Nat st m in dom (F . k) & m <> len (F . k) holds
(F . k) /. m <> (F . k) /. (len (F . k)) ; :: thesis:
A544: for k being Nat st S₈[k] holds
S₈[k + 1]

proof

let k be Nat; :: thesis:
assume A545: F . k is one-to-one ; :: thesis:

now :: thesis:

let n, m be Element of NAT ; :: thesis:
assume that
A546: n in dom (F . (k + 1)) and
A547: m in dom (F . (k + 1)) and
A548: (F . (k + 1)) /. n = (F . (k + 1)) /. m ; :: thesis:
A549: ( n <= len (F . (k + 1)) & m <= len (F . (k + 1)) ) by A546, A547, FINSEQ_3:25;
A550: 1 <= m by A547, FINSEQ_3:25;
A551: 1 <= n by A546, FINSEQ_3:25;
A552: ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A462;
A553: len (F . k) = k by A192;
A554: len (F . (k + 1)) = k + 1 by A192;

per cases by A549, A554, NAT_1:8;

suppose A555: ( n <= k & m <= k ) ; :: thesis:

then A556: m in dom (F . k) by A550, A553, FINSEQ_3:25;
then A557: (F . (k + 1)) /. m = (F . k) /. m by A552, FINSEQ_4:68;
A558: n in dom (F . k) by A551, A553, A555, FINSEQ_3:25;
then (F . (k + 1)) /. n = (F . k) /. n by A552, FINSEQ_4:68;
hence n = m by A545, A548, A558, A556, A557, PARTFUN2:10; :: thesis:

end;

suppose ( n = k + 1 & m <= k ) ; :: thesis:

hence n = m by A543, A547, A548, A554, NAT_1:12; :: thesis:

end;

suppose ( n <= k & m = k + 1 ) ; :: thesis:

hence n = m by A543, A546, A548, A554, NAT_1:12; :: thesis:

end;

suppose ( n = k + 1 & m = k + 1 ) ; :: thesis:

hence n = m ; :: thesis:

end;

hence S₈[k + 1] by PARTFUN2:9; :: thesis:

end;

A559: S₈[ 0 ] by A170;
A560: for k being Nat holds S₈[k] from NAT_1:sch 2(A559, A544);
A561: for k being Nat holds card (rng (F . k)) = k

proof

let k be Nat; :: thesis:
F . k is one-to-one by A560;
hence card (rng (F . k)) = len (F . k) by FINSEQ_4:62
.= k by A192 ;
:: thesis:

end;

set k = ((len (Gauge (C,n))) * (width (Gauge (C,n)))) + 1;
F . (((len (Gauge (C,n))) * (width (Gauge (C,n)))) + 1) is_sequence_on Gauge (C,n) by A427;
then ( card (Values (Gauge (C,n))) <= (len (Gauge (C,n))) * (width (Gauge (C,n))) & card (rng (F . (((len (Gauge (C,n))) * (width (Gauge (C,n)))) + 1))) <= card (Values (Gauge (C,n))) ) by GOBRD13:8, MATRIX_0:40, NAT_1:43;
then ( ((len (Gauge (C,n))) * (width (Gauge (C,n)))) + 1 > (len (Gauge (C,n))) * (width (Gauge (C,n))) & card (rng (F . (((len (Gauge (C,n))) * (width (Gauge (C,n)))) + 1))) <= (len (Gauge (C,n))) * (width (Gauge (C,n))) ) by NAT_1:13, XXREAL_0:2;
hence contradiction by A561; :: thesis:

end;

then A562: ex k being Nat st S₅[k] ;
consider k being Nat such that
A563: S₅[k] and
A564: for l being Nat st S₅[l] holds
k <= l from NAT_1:sch 5(A562);
reconsider k = k as Nat ;
consider m being Nat such that
A565: m in dom (F . k) and
A566: m <> len (F . k) and
A567: (F . k) /. m = (F . k) /. (len (F . k)) by A563;
A568: 1 <= m by A565, FINSEQ_3:25;
reconsider f = F . k as non empty FinSequence of (TOP-REAL 2) by A563;
A569: f is_sequence_on Gauge (C,n) by A427;
A570: m <= len f by A565, FINSEQ_3:25;
then A571: m < len f by A566, XXREAL_0:1;
then 1 < len f by A568, XXREAL_0:2;
then A572: len f >= 1 + 1 by NAT_1:13;
A573: S₇[ 0 ] by A170, CARD_1:27, SPPOL_2:26;
for k being Nat holds S₇[k] from NAT_1:sch 2(A573, A489);
then reconsider f = f as non empty non constant special unfolded FinSequence of (TOP-REAL 2) by A569, A572, JORDAN8:4, JORDAN8:5;
A574: m + 1 <= len f by A571, NAT_1:13;
set g = f /^ (m -' 1);
m -' 1 <= m by NAT_D:44;
then m -' 1 < m + 1 by NAT_1:13;
then A575: m -' 1 < len f by A574, XXREAL_0:2;
then A576: len (f /^ (m -' 1)) = (len f) - (m -' 1) by RFINSEQ:def 1;
then (m -' 1) - (m -' 1) < len (f /^ (m -' 1)) by A575, XREAL_1:9;
then reconsider g = f /^ (m -' 1) as non empty FinSequence of (TOP-REAL 2) by CARD_1:27;
len g in dom g by FINSEQ_5:6;
then A577: g /. (len g) = f /. ((m -' 1) + (len g)) by FINSEQ_5:27
.= f /. (len f) by A576 ;
A578: len (F . k) = k by A192;
A579: for j, i being Nat st 1 <= i & i < len g & 1 <= j & j < len g & g /. i = g /. j holds
i = j

proof

let j, i be Nat; :: thesis:
assume that
A580: 1 <= i and
A581: i < len g and
A582: 1 <= j and
A583: j < len g and
A584: g /. i = g /. j and
A585: i <> j ; :: thesis:
A586: i in dom g by A580, A581, FINSEQ_3:25;
then A587: g /. i = f /. ((m -' 1) + i) by FINSEQ_5:27;
A588: j in dom g by A582, A583, FINSEQ_3:25;
then A589: g /. j = f /. ((m -' 1) + j) by FINSEQ_5:27;

per cases by A585, XXREAL_0:1;

suppose A590: i < j ; :: thesis:

set l = (m -' 1) + j;
set m9 = (m -' 1) + i;
A591: (m -' 1) + i < (m -' 1) + j by A590, XREAL_1:6;
A592: len (F . ((m -' 1) + j)) = (m -' 1) + j by A192;
A593: (m -' 1) + j < k by A578, A576, A583, XREAL_1:20;
then A594: f | ((m -' 1) + j) = F . ((m -' 1) + j) by A488;
0 + j <= (m -' 1) + j by XREAL_1:6;
then A595: 1 <= (m -' 1) + j by A582, XXREAL_0:2;
then (m -' 1) + j in dom (F . ((m -' 1) + j)) by A592, FINSEQ_3:25;
then A596: (F . ((m -' 1) + j)) /. ((m -' 1) + j) = f /. ((m -' 1) + j) by A594, FINSEQ_4:70;
0 + i <= (m -' 1) + i by XREAL_1:6;
then 1 <= (m -' 1) + i by A580, XXREAL_0:2;
then A597: (m -' 1) + i in dom (F . ((m -' 1) + j)) by A591, A592, FINSEQ_3:25;
then (F . ((m -' 1) + j)) /. ((m -' 1) + i) = f /. ((m -' 1) + i) by A594, FINSEQ_4:70;
hence contradiction by A564, A584, A587, A588, A591, A593, A595, A592, A597, A596, FINSEQ_5:27; :: thesis:

end;

suppose A598: j < i ; :: thesis:

set l = (m -' 1) + i;
set m9 = (m -' 1) + j;
A599: (m -' 1) + j < (m -' 1) + i by A598, XREAL_1:6;
A600: len (F . ((m -' 1) + i)) = (m -' 1) + i by A192;
A601: (m -' 1) + i < k by A578, A576, A581, XREAL_1:20;
then A602: f | ((m -' 1) + i) = F . ((m -' 1) + i) by A488;
0 + i <= (m -' 1) + i by XREAL_1:6;
then A603: 1 <= (m -' 1) + i by A580, XXREAL_0:2;
then (m -' 1) + i in dom (F . ((m -' 1) + i)) by A600, FINSEQ_3:25;
then A604: (F . ((m -' 1) + i)) /. ((m -' 1) + i) = f /. ((m -' 1) + i) by A602, FINSEQ_4:70;
0 + j <= (m -' 1) + j by XREAL_1:6;
then 1 <= (m -' 1) + j by A582, XXREAL_0:2;
then A605: (m -' 1) + j in dom (F . ((m -' 1) + i)) by A599, A600, FINSEQ_3:25;
then (F . ((m -' 1) + i)) /. ((m -' 1) + j) = f /. ((m -' 1) + j) by A602, FINSEQ_4:70;
hence contradiction by A564, A584, A586, A589, A599, A601, A603, A600, A605, A604, FINSEQ_5:27; :: thesis:

end;

A606: now :: thesis:

consider i being Nat such that
A607: ( 1 <= i & i + 1 <= len (Gauge (C,n)) ) and
A608: ( N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) ) and
A609: F . (1 + 1) = <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))))*> by A171;
take i = i; :: thesis:
thus ( 1 <= i & i + 1 <= len (Gauge (C,n)) ) by A607; :: thesis:
A610: f | 2 = F . 2 by A488, A578, A572;
A611: len (f | 2) = 2 by A572, FINSEQ_1:59;
then 1 in dom (f | 2) by FINSEQ_3:25;
hence f /. 1 = (f | 2) /. 1 by FINSEQ_4:70
.= (Gauge (C,n)) * (i,(width (Gauge (C,n)))) by A609, A610, FINSEQ_4:17 ;
:: thesis:
2 in dom (f | 2) by A611, FINSEQ_3:25;
hence f /. 2 = (f | 2) /. 2 by FINSEQ_4:70
.= (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) by A609, A610, FINSEQ_4:17 ;
:: thesis:
thus ( N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) ) by A608; :: thesis:

end;

1 in dom g by FINSEQ_5:6;
then A612: g /. 1 = f /. ((m -' 1) + 1) by FINSEQ_5:27
.= f /. m by A568, XREAL_1:235 ;
A613: for j, i being Nat st 1 < i & i < j & j <= len g holds
g /. i <> g /. j

proof

let j, i be Nat; :: thesis:
assume that
A614: 1 < i and
A615: i < j and
A616: j <= len g and
A617: g /. i = g /. j ; :: thesis:
A618: 1 < j by A614, A615, XXREAL_0:2;
A619: i < len g by A615, A616, XXREAL_0:2;
then A620: 1 < len g by A614, XXREAL_0:2;

per cases ;

suppose j <> len g ; :: thesis:

then j < len g by A616, XXREAL_0:1;
hence contradiction by A579, A614, A615, A617, A618, A619; :: thesis:

end;

suppose j = len g ; :: thesis:

hence contradiction by A567, A612, A577, A579, A614, A615, A617, A620; :: thesis:

end;

(m + 1) - (m -' 1) <= len g by A574, A576, XREAL_1:9;
then A621: (m + 1) - (m - 1) <= len g by A568, XREAL_1:233;
then A622: ((1 + m) - m) + 1 <= len g ;
A623: g is_sequence_on Gauge (C,n) by A427, JORDAN8:2;
then A624: g is standard by JORDAN8:4;
A625: not g is constant

proof

take 1 ; :: according to SEQM_3:def 10 :: thesis:
take 2 ; :: thesis:
thus A626: 1 in dom g by FINSEQ_5:6; :: thesis:
thus A627: 2 in dom g by A621, FINSEQ_3:25; :: thesis:
then g /. 1 <> g /. (1 + 1) by A624, FINSEQ_5:6, GOBOARD7:29;
then g . 1 <> g /. (1 + 1) by A626, PARTFUN1:def 6;
hence not g . 1 = g . 2 by A627, PARTFUN1:def 6; :: thesis:

end;

A628: for j, i being Nat st 1 <= i & i < j & j < len g holds
g /. i <> g /. j

proof

let j, i be Nat; :: thesis:
assume that
A629: ( 1 <= i & i < j & j < len g ) and
A630: g /. i = g /. j ; :: thesis:
( 1 < j & i < len g ) by A629, XXREAL_0:2;
hence contradiction by A579, A629, A630; :: thesis:

end;

g is s.c.c.

proof

let i be Nat; :: according to GOBOARD5:def 4 :: thesis:
let j be Nat; :: thesis:
assume that
A631: i + 1 < j and
A632: ( ( i > 1 & j < len g ) or j + 1 < len g ) ; :: thesis:
A633: 1 < j by A631, NAT_1:12;
A634: 1 <= i + 1 by NAT_1:12;
A635: j <= j + 1 by NAT_1:12;
then A636: i + 1 < j + 1 by A631, XXREAL_0:2;
i < j by A631, NAT_1:13;
then A637: i < j + 1 by A635, XXREAL_0:2;

per cases by A632, NAT_1:14;

suppose A638: ( i > 1 & j < len g ) ; :: thesis:

then A639: j + 1 <= len g by NAT_1:13;
then A640: LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by A633, TOPREAL1:def 3;
consider i19, j19, i29, j29 being Nat such that
A641: [i19,j19] in Indices (Gauge (C,n)) and
A642: g /. j = (Gauge (C,n)) * (i19,j19) and
A643: [i29,j29] in Indices (Gauge (C,n)) and
A644: g /. (j + 1) = (Gauge (C,n)) * (i29,j29) and
A645: ( ( i19 = i29 & j19 + 1 = j29 ) or ( i19 + 1 = i29 & j19 = j29 ) or ( i19 = i29 + 1 & j19 = j29 ) or ( i19 = i29 & j19 = j29 + 1 ) ) by A623, A633, A639, JORDAN8:3;
A646: 1 <= i19 by A641, MATRIX_0:32;
A647: j29 <= width (Gauge (C,n)) by A643, MATRIX_0:32;
A648: 1 <= i29 by A643, MATRIX_0:32;
A649: i19 <= len (Gauge (C,n)) by A641, MATRIX_0:32;
A650: 1 <= j29 by A643, MATRIX_0:32;
A651: j19 <= width (Gauge (C,n)) by A641, MATRIX_0:32;
A652: i29 <= len (Gauge (C,n)) by A643, MATRIX_0:32;
A653: 1 <= j19 by A641, MATRIX_0:32;
A654: i + 1 < len g by A631, A638, XXREAL_0:2;
then A655: LSeg (g,i) = LSeg ((g /. i),(g /. (i + 1))) by A638, TOPREAL1:def 3;
A656: i < len g by A654, NAT_1:13;
consider i1, j1, i2, j2 being Nat such that
A657: [i1,j1] in Indices (Gauge (C,n)) and
A658: g /. i = (Gauge (C,n)) * (i1,j1) and
A659: [i2,j2] in Indices (Gauge (C,n)) and
A660: g /. (i + 1) = (Gauge (C,n)) * (i2,j2) and
A661: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A623, A638, A654, JORDAN8:3;
A662: 1 <= i1 by A657, MATRIX_0:32;
A663: j2 <= width (Gauge (C,n)) by A659, MATRIX_0:32;
A664: j1 <= width (Gauge (C,n)) by A657, MATRIX_0:32;
A665: 1 <= j2 by A659, MATRIX_0:32;
A666: 1 <= j1 by A657, MATRIX_0:32;
A667: i2 <= len (Gauge (C,n)) by A659, MATRIX_0:32;
A668: i1 <= len (Gauge (C,n)) by A657, MATRIX_0:32;
A669: 1 < i + 1 by A638, NAT_1:13;
assume A670: LSeg (g,i) meets LSeg (g,j) ; :: thesis:
A671: 1 <= i2 by A659, MATRIX_0:32;

now :: thesis:

per cases by A661, A645;

suppose A672: ( i1 = i2 & j1 + 1 = j2 & i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

then A673: ( j1 = j19 or j1 = j19 + 1 or j1 + 1 = j19 ) by A655, A658, A660, A662, A668, A666, A663, A640, A642, A644, A646, A649, A653, A647, A670, GOBOARD7:22;
i1 = i19 by A655, A658, A660, A662, A668, A666, A663, A640, A642, A644, A646, A649, A653, A647, A670, A672, GOBOARD7:19;
hence contradiction by A579, A613, A631, A635, A634, A633, A637, A638, A654, A656, A658, A660, A639, A642, A644, A672, A673; :: thesis:

end;

suppose A674: ( i1 = i2 & j1 + 1 = j2 & i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

then ( ( i1 = i19 & j1 = j19 ) or ( i1 = i19 & j1 + 1 = j19 ) or ( i1 = i19 + 1 & j1 = j19 ) or ( i1 = i19 + 1 & j1 + 1 = j19 ) ) by A655, A658, A660, A662, A668, A666, A663, A640, A642, A644, A646, A653, A651, A652, A670, GOBOARD7:21;
hence contradiction by A579, A613, A631, A636, A633, A637, A638, A669, A656, A658, A660, A639, A642, A644, A674; :: thesis:

end;

suppose A675: ( i1 = i2 & j1 + 1 = j2 & i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

then ( ( i1 = i29 & j19 = j1 ) or ( i1 = i29 & j1 + 1 = j19 ) or ( i1 = i29 + 1 & j19 = j1 ) or ( i1 = i29 + 1 & j1 + 1 = j19 ) ) by A655, A658, A660, A662, A668, A666, A663, A640, A642, A644, A649, A653, A651, A648, A670, GOBOARD7:21;
hence contradiction by A579, A613, A631, A636, A633, A637, A638, A669, A656, A658, A660, A639, A642, A644, A675; :: thesis:

end;

suppose A676: ( i1 = i2 & j1 + 1 = j2 & i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

then A677: ( j1 = j29 or j1 = j29 + 1 or j1 + 1 = j29 ) by A655, A658, A660, A662, A668, A666, A663, A640, A642, A644, A646, A649, A651, A650, A670, GOBOARD7:22;
i1 = i19 by A655, A658, A660, A662, A668, A666, A663, A640, A642, A644, A646, A649, A651, A650, A670, A676, GOBOARD7:19;
hence contradiction by A579, A613, A631, A636, A633, A638, A669, A656, A658, A660, A639, A642, A644, A676, A677; :: thesis:

end;

suppose A678: ( i1 + 1 = i2 & j1 = j2 & i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

then ( ( i19 = i1 & j1 = j19 ) or ( i19 = i1 & j19 + 1 = j1 ) or ( i19 = i1 + 1 & j1 = j19 ) or ( i19 = i1 + 1 & j19 + 1 = j1 ) ) by A655, A658, A660, A662, A666, A664, A667, A640, A642, A644, A646, A649, A653, A647, A670, GOBOARD7:21;
hence contradiction by A579, A613, A631, A636, A633, A637, A638, A669, A656, A658, A660, A639, A642, A644, A678; :: thesis:

end;

suppose A679: ( i1 + 1 = i2 & j1 = j2 & i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

then A680: ( i1 = i19 or i1 = i19 + 1 or i1 + 1 = i19 ) by A655, A658, A660, A662, A666, A664, A667, A640, A642, A644, A646, A653, A651, A652, A670, GOBOARD7:23;
j1 = j19 by A655, A658, A660, A662, A666, A664, A667, A640, A642, A644, A646, A653, A651, A652, A670, A679, GOBOARD7:20;
hence contradiction by A579, A613, A631, A635, A634, A633, A637, A638, A654, A656, A658, A660, A639, A642, A644, A679, A680; :: thesis:

end;

suppose A681: ( i1 + 1 = i2 & j1 = j2 & i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

then A682: ( i1 = i29 or i1 = i29 + 1 or i1 + 1 = i29 ) by A655, A658, A660, A662, A666, A664, A667, A640, A642, A644, A649, A653, A651, A648, A670, GOBOARD7:23;
j1 = j19 by A655, A658, A660, A662, A666, A664, A667, A640, A642, A644, A649, A653, A651, A648, A670, A681, GOBOARD7:20;
hence contradiction by A579, A613, A636, A633, A637, A638, A669, A656, A658, A660, A639, A642, A644, A681, A682; :: thesis:

end;

suppose A683: ( i1 + 1 = i2 & j1 = j2 & i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

then ( ( i19 = i1 & j1 = j29 ) or ( i19 = i1 & j29 + 1 = j1 ) or ( i19 = i1 + 1 & j1 = j29 ) or ( i19 = i1 + 1 & j29 + 1 = j1 ) ) by A655, A658, A660, A662, A666, A664, A667, A640, A642, A644, A646, A649, A651, A650, A670, GOBOARD7:21;
hence contradiction by A579, A613, A631, A636, A633, A637, A638, A669, A656, A658, A660, A639, A642, A644, A683; :: thesis:

end;

suppose A684: ( i1 = i2 + 1 & j1 = j2 & i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

then ( ( i19 = i2 & j19 = j1 ) or ( i19 = i2 & j19 + 1 = j1 ) or ( i19 = i2 + 1 & j19 = j1 ) or ( i19 = i2 + 1 & j19 + 1 = j1 ) ) by A655, A658, A660, A668, A666, A664, A671, A640, A642, A644, A646, A649, A653, A647, A670, GOBOARD7:21;
hence contradiction by A579, A613, A631, A636, A633, A637, A638, A669, A656, A658, A660, A639, A642, A644, A684; :: thesis:

end;

suppose A685: ( i1 = i2 + 1 & j1 = j2 & i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

then A686: ( i2 = i19 or i2 = i19 + 1 or i2 + 1 = i19 ) by A655, A658, A660, A668, A666, A664, A671, A640, A642, A644, A646, A653, A651, A652, A670, GOBOARD7:23;
j1 = j19 by A655, A658, A660, A668, A666, A664, A671, A640, A642, A644, A646, A653, A651, A652, A670, A685, GOBOARD7:20;
hence contradiction by A579, A613, A631, A636, A633, A638, A669, A656, A658, A660, A639, A642, A644, A685, A686; :: thesis:

end;

suppose A687: ( i1 = i2 + 1 & j1 = j2 & i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

then A688: ( i2 = i29 or i2 = i29 + 1 or i2 + 1 = i29 ) by A655, A658, A660, A668, A666, A664, A671, A640, A642, A644, A649, A653, A651, A648, A670, GOBOARD7:23;
j1 = j19 by A655, A658, A660, A668, A666, A664, A671, A640, A642, A644, A649, A653, A651, A648, A670, A687, GOBOARD7:20;
hence contradiction by A613, A631, A636, A637, A638, A669, A658, A660, A639, A642, A644, A687, A688; :: thesis:

end;

suppose A689: ( i1 = i2 + 1 & j1 = j2 & i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

then ( ( i19 = i2 & j29 = j1 ) or ( i19 = i2 & j29 + 1 = j1 ) or ( i19 = i2 + 1 & j29 = j1 ) or ( i19 = i2 + 1 & j29 + 1 = j1 ) ) by A655, A658, A660, A668, A666, A664, A671, A640, A642, A644, A646, A649, A651, A650, A670, GOBOARD7:21;
hence contradiction by A579, A613, A631, A636, A633, A637, A638, A669, A656, A658, A660, A639, A642, A644, A689; :: thesis:

end;

suppose A690: ( i1 = i2 & j1 = j2 + 1 & i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

then A691: ( j2 = j19 or j2 = j19 + 1 or j2 + 1 = j19 ) by A655, A658, A660, A662, A668, A664, A665, A640, A642, A644, A646, A649, A653, A647, A670, GOBOARD7:22;
i1 = i19 by A655, A658, A660, A662, A668, A664, A665, A640, A642, A644, A646, A649, A653, A647, A670, A690, GOBOARD7:19;
hence contradiction by A579, A613, A631, A636, A633, A638, A669, A656, A658, A660, A639, A642, A644, A690, A691; :: thesis:

end;

suppose A692: ( i1 = i2 & j1 = j2 + 1 & i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

then ( ( i1 = i19 & j2 = j19 ) or ( i1 = i19 & j2 + 1 = j19 ) or ( i1 = i19 + 1 & j2 = j19 ) or ( i1 = i19 + 1 & j2 + 1 = j19 ) ) by A655, A658, A660, A662, A668, A664, A665, A640, A642, A644, A646, A653, A651, A652, A670, GOBOARD7:21;
hence contradiction by A579, A613, A631, A636, A633, A637, A638, A669, A656, A658, A660, A639, A642, A644, A692; :: thesis:

end;

suppose A693: ( i1 = i2 & j1 = j2 + 1 & i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

then ( ( i1 = i29 & j2 = j19 ) or ( i1 = i29 & j2 + 1 = j19 ) or ( i1 = i29 + 1 & j2 = j19 ) or ( i1 = i29 + 1 & j2 + 1 = j19 ) ) by A655, A658, A660, A662, A668, A664, A665, A640, A642, A644, A649, A653, A651, A648, A670, GOBOARD7:21;
hence contradiction by A579, A613, A631, A636, A633, A637, A638, A669, A656, A658, A660, A639, A642, A644, A693; :: thesis:

end;

suppose A694: ( i1 = i2 & j1 = j2 + 1 & i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

then A695: ( j2 = j29 or j2 = j29 + 1 or j2 + 1 = j29 ) by A655, A658, A660, A662, A668, A664, A665, A640, A642, A644, A646, A649, A651, A650, A670, GOBOARD7:22;
i1 = i19 by A655, A658, A660, A662, A668, A664, A665, A640, A642, A644, A646, A649, A651, A650, A670, A694, GOBOARD7:19;
hence contradiction by A613, A631, A636, A637, A638, A669, A658, A660, A639, A642, A644, A694, A695; :: thesis:

end;

hence contradiction ; :: thesis:

end;

suppose ( i = 0 & j + 1 < len g ) ; :: thesis:

then LSeg (g,i) = {} by TOPREAL1:def 3;
hence LSeg (g,i) misses LSeg (g,j) by XBOOLE_1:65; :: thesis:

end;

suppose A696: ( 1 <= i & j + 1 < len g ) ; :: thesis:

then A697: i + 1 < len g by A636, XXREAL_0:2;
then A698: LSeg (g,i) = LSeg ((g /. i),(g /. (i + 1))) by A696, TOPREAL1:def 3;
A699: i < len g by A697, NAT_1:13;
consider i1, j1, i2, j2 being Nat such that
A700: [i1,j1] in Indices (Gauge (C,n)) and
A701: g /. i = (Gauge (C,n)) * (i1,j1) and
A702: [i2,j2] in Indices (Gauge (C,n)) and
A703: g /. (i + 1) = (Gauge (C,n)) * (i2,j2) and
A704: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A623, A696, A697, JORDAN8:3;
A705: 1 <= i1 by A700, MATRIX_0:32;
A706: j2 <= width (Gauge (C,n)) by A702, MATRIX_0:32;
A707: j1 <= width (Gauge (C,n)) by A700, MATRIX_0:32;
A708: 1 <= j2 by A702, MATRIX_0:32;
A709: 1 <= j1 by A700, MATRIX_0:32;
A710: i2 <= len (Gauge (C,n)) by A702, MATRIX_0:32;
A711: i1 <= len (Gauge (C,n)) by A700, MATRIX_0:32;
A712: 1 < i + 1 by A696, NAT_1:13;
assume A713: LSeg (g,i) meets LSeg (g,j) ; :: thesis:
consider i19, j19, i29, j29 being Nat such that
A714: [i19,j19] in Indices (Gauge (C,n)) and
A715: g /. j = (Gauge (C,n)) * (i19,j19) and
A716: [i29,j29] in Indices (Gauge (C,n)) and
A717: g /. (j + 1) = (Gauge (C,n)) * (i29,j29) and
A718: ( ( i19 = i29 & j19 + 1 = j29 ) or ( i19 + 1 = i29 & j19 = j29 ) or ( i19 = i29 + 1 & j19 = j29 ) or ( i19 = i29 & j19 = j29 + 1 ) ) by A623, A633, A696, JORDAN8:3;
A719: 1 <= i19 by A714, MATRIX_0:32;
A720: j29 <= width (Gauge (C,n)) by A716, MATRIX_0:32;
A721: 1 <= i29 by A716, MATRIX_0:32;
A722: i19 <= len (Gauge (C,n)) by A714, MATRIX_0:32;
A723: 1 <= j29 by A716, MATRIX_0:32;
A724: j19 <= width (Gauge (C,n)) by A714, MATRIX_0:32;
A725: i29 <= len (Gauge (C,n)) by A716, MATRIX_0:32;
A726: 1 <= j19 by A714, MATRIX_0:32;
A727: j < len g by A696, NAT_1:12;
A728: LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by A633, A696, TOPREAL1:def 3;
A729: 1 <= i2 by A702, MATRIX_0:32;

now :: thesis:

per cases by A704, A718;

suppose A730: ( i1 = i2 & j1 + 1 = j2 & i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

then A731: ( j1 = j19 or j1 = j19 + 1 or j1 + 1 = j19 ) by A698, A701, A703, A705, A711, A709, A706, A728, A715, A717, A719, A722, A726, A720, A713, GOBOARD7:22;
i1 = i19 by A698, A701, A703, A705, A711, A709, A706, A728, A715, A717, A719, A722, A726, A720, A713, A730, GOBOARD7:19;
hence contradiction by A628, A631, A636, A634, A637, A696, A727, A701, A703, A715, A717, A730, A731; :: thesis:

end;

suppose A732: ( i1 = i2 & j1 + 1 = j2 & i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

then ( ( i1 = i19 & j1 = j19 ) or ( i1 = i19 & j1 + 1 = j19 ) or ( i1 = i19 + 1 & j1 = j19 ) or ( i1 = i19 + 1 & j1 + 1 = j19 ) ) by A698, A701, A703, A705, A711, A709, A706, A728, A715, A717, A719, A726, A724, A725, A713, GOBOARD7:21;
hence contradiction by A579, A628, A631, A636, A633, A637, A696, A712, A699, A727, A701, A703, A715, A717, A732; :: thesis:

end;

suppose A733: ( i1 = i2 & j1 + 1 = j2 & i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

then ( ( i1 = i29 & j19 = j1 ) or ( i1 = i29 & j1 + 1 = j19 ) or ( i1 = i29 + 1 & j19 = j1 ) or ( i1 = i29 + 1 & j1 + 1 = j19 ) ) by A698, A701, A703, A705, A711, A709, A706, A728, A715, A717, A722, A726, A724, A721, A713, GOBOARD7:21;
hence contradiction by A579, A628, A631, A636, A633, A637, A696, A712, A699, A727, A701, A703, A715, A717, A733; :: thesis:

end;

suppose A734: ( i1 = i2 & j1 + 1 = j2 & i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

then A735: ( j1 = j29 or j1 = j29 + 1 or j1 + 1 = j29 ) by A698, A701, A703, A705, A711, A709, A706, A728, A715, A717, A719, A722, A724, A723, A713, GOBOARD7:22;
i1 = i19 by A698, A701, A703, A705, A711, A709, A706, A728, A715, A717, A719, A722, A724, A723, A713, A734, GOBOARD7:19;
hence contradiction by A579, A613, A631, A636, A633, A696, A712, A699, A727, A701, A703, A715, A717, A734, A735; :: thesis:

end;

suppose A736: ( i1 + 1 = i2 & j1 = j2 & i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

then ( ( i19 = i1 & j1 = j19 ) or ( i19 = i1 & j19 + 1 = j1 ) or ( i19 = i1 + 1 & j1 = j19 ) or ( i19 = i1 + 1 & j19 + 1 = j1 ) ) by A698, A701, A703, A705, A709, A707, A710, A728, A715, A717, A719, A722, A726, A720, A713, GOBOARD7:21;
hence contradiction by A579, A628, A631, A636, A634, A633, A637, A696, A699, A727, A701, A703, A715, A717, A736; :: thesis:

end;

suppose A737: ( i1 + 1 = i2 & j1 = j2 & i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

then A738: ( i1 = i19 or i1 = i19 + 1 or i1 + 1 = i19 ) by A698, A701, A703, A705, A709, A707, A710, A728, A715, A717, A719, A726, A724, A725, A713, GOBOARD7:23;
j1 = j19 by A698, A701, A703, A705, A709, A707, A710, A728, A715, A717, A719, A726, A724, A725, A713, A737, GOBOARD7:20;
hence contradiction by A628, A631, A636, A634, A637, A696, A727, A701, A703, A715, A717, A737, A738; :: thesis:

end;

suppose A739: ( i1 + 1 = i2 & j1 = j2 & i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

then A740: ( i1 = i29 or i1 = i29 + 1 or i1 + 1 = i29 ) by A698, A701, A703, A705, A709, A707, A710, A728, A715, A717, A722, A726, A724, A721, A713, GOBOARD7:23;
j1 = j19 by A698, A701, A703, A705, A709, A707, A710, A728, A715, A717, A722, A726, A724, A721, A713, A739, GOBOARD7:20;
hence contradiction by A579, A628, A636, A633, A637, A696, A712, A699, A727, A701, A703, A715, A717, A739, A740; :: thesis:

end;

suppose A741: ( i1 + 1 = i2 & j1 = j2 & i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

then ( ( i19 = i1 & j1 = j29 ) or ( i19 = i1 & j29 + 1 = j1 ) or ( i19 = i1 + 1 & j1 = j29 ) or ( i19 = i1 + 1 & j29 + 1 = j1 ) ) by A698, A701, A703, A705, A709, A707, A710, A728, A715, A717, A719, A722, A724, A723, A713, GOBOARD7:21;
hence contradiction by A579, A628, A631, A636, A633, A637, A696, A712, A699, A727, A701, A703, A715, A717, A741; :: thesis:

end;

suppose A742: ( i1 = i2 + 1 & j1 = j2 & i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

then ( ( i19 = i2 & j19 = j1 ) or ( i19 = i2 & j19 + 1 = j1 ) or ( i19 = i2 + 1 & j19 = j1 ) or ( i19 = i2 + 1 & j19 + 1 = j1 ) ) by A698, A701, A703, A711, A709, A707, A729, A728, A715, A717, A719, A722, A726, A720, A713, GOBOARD7:21;
hence contradiction by A579, A628, A631, A636, A633, A637, A696, A712, A699, A727, A701, A703, A715, A717, A742; :: thesis:

end;

suppose A743: ( i1 = i2 + 1 & j1 = j2 & i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

then A744: ( i2 = i19 or i2 = i19 + 1 or i2 + 1 = i19 ) by A698, A701, A703, A711, A709, A707, A729, A728, A715, A717, A719, A726, A724, A725, A713, GOBOARD7:23;
j1 = j19 by A698, A701, A703, A711, A709, A707, A729, A728, A715, A717, A719, A726, A724, A725, A713, A743, GOBOARD7:20;
hence contradiction by A579, A613, A631, A636, A633, A696, A712, A699, A727, A701, A703, A715, A717, A743, A744; :: thesis:

end;

suppose A745: ( i1 = i2 + 1 & j1 = j2 & i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

then A746: ( i2 = i29 or i2 = i29 + 1 or i2 + 1 = i29 ) by A698, A701, A703, A711, A709, A707, A729, A728, A715, A717, A722, A726, A724, A721, A713, GOBOARD7:23;
j1 = j19 by A698, A701, A703, A711, A709, A707, A729, A728, A715, A717, A722, A726, A724, A721, A713, A745, GOBOARD7:20;
hence contradiction by A628, A631, A636, A637, A696, A712, A727, A701, A703, A715, A717, A745, A746; :: thesis:

end;

suppose A747: ( i1 = i2 + 1 & j1 = j2 & i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

then ( ( i19 = i2 & j29 = j1 ) or ( i19 = i2 & j29 + 1 = j1 ) or ( i19 = i2 + 1 & j29 = j1 ) or ( i19 = i2 + 1 & j29 + 1 = j1 ) ) by A698, A701, A703, A711, A709, A707, A729, A728, A715, A717, A719, A722, A724, A723, A713, GOBOARD7:21;
hence contradiction by A579, A628, A631, A636, A633, A637, A696, A712, A699, A727, A701, A703, A715, A717, A747; :: thesis:

end;

suppose A748: ( i1 = i2 & j1 = j2 + 1 & i19 = i29 & j19 + 1 = j29 ) ; :: thesis:

then A749: ( j2 = j19 or j2 = j19 + 1 or j2 + 1 = j19 ) by A698, A701, A703, A705, A711, A707, A708, A728, A715, A717, A719, A722, A726, A720, A713, GOBOARD7:22;
i1 = i19 by A698, A701, A703, A705, A711, A707, A708, A728, A715, A717, A719, A722, A726, A720, A713, A748, GOBOARD7:19;
hence contradiction by A579, A613, A631, A636, A633, A696, A712, A699, A727, A701, A703, A715, A717, A748, A749; :: thesis:

end;

suppose A750: ( i1 = i2 & j1 = j2 + 1 & i19 + 1 = i29 & j19 = j29 ) ; :: thesis:

then ( ( i1 = i19 & j2 = j19 ) or ( i1 = i19 & j2 + 1 = j19 ) or ( i1 = i19 + 1 & j2 = j19 ) or ( i1 = i19 + 1 & j2 + 1 = j19 ) ) by A698, A701, A703, A705, A711, A707, A708, A728, A715, A717, A719, A726, A724, A725, A713, GOBOARD7:21;
hence contradiction by A579, A628, A631, A636, A633, A637, A696, A712, A699, A727, A701, A703, A715, A717, A750; :: thesis:

end;

suppose A751: ( i1 = i2 & j1 = j2 + 1 & i19 = i29 + 1 & j19 = j29 ) ; :: thesis:

then ( ( i1 = i29 & j2 = j19 ) or ( i1 = i29 & j2 + 1 = j19 ) or ( i1 = i29 + 1 & j2 = j19 ) or ( i1 = i29 + 1 & j2 + 1 = j19 ) ) by A698, A701, A703, A705, A711, A707, A708, A728, A715, A717, A722, A726, A724, A721, A713, GOBOARD7:21;
hence contradiction by A579, A628, A631, A636, A633, A637, A696, A712, A699, A727, A701, A703, A715, A717, A751; :: thesis:

end;

suppose A752: ( i1 = i2 & j1 = j2 + 1 & i19 = i29 & j19 = j29 + 1 ) ; :: thesis:

then A753: ( j2 = j29 or j2 = j29 + 1 or j2 + 1 = j29 ) by A698, A701, A703, A705, A711, A707, A708, A728, A715, A717, A719, A722, A724, A723, A713, GOBOARD7:22;
i1 = i19 by A698, A701, A703, A705, A711, A707, A708, A728, A715, A717, A719, A722, A724, A723, A713, A752, GOBOARD7:19;
hence contradiction by A628, A631, A636, A637, A696, A712, A727, A701, A703, A715, A717, A752, A753; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then reconsider g = g as non constant standard special_circular_sequence by A567, A612, A577, A623, A625, FINSEQ_6:def 1, JORDAN8:4;
A754: for i being Nat st 1 <= i & i + 1 <= len f holds
right_cell (f,i,(Gauge (C,n))) = Cl (Int (right_cell (f,i,(Gauge (C,n)))))

proof

let i be Nat; :: thesis:
assume A755: ( 1 <= i & i + 1 <= len f ) ; :: thesis:
consider i1, j1, i2, j2 being Nat such that
A756: [i1,j1] in Indices (Gauge (C,n)) and
A757: f /. i = (Gauge (C,n)) * (i1,j1) and
A758: [i2,j2] in Indices (Gauge (C,n)) and
A759: f /. (i + 1) = (Gauge (C,n)) * (i2,j2) and
A760: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A569, A755, JORDAN8:3;
A761: i1 <= len (Gauge (C,n)) by A756, MATRIX_0:32;
A762: j2 <= width (Gauge (C,n)) by A758, MATRIX_0:32;
A763: j1 <= width (Gauge (C,n)) by A756, MATRIX_0:32;
A764: ( j1 + 1 > j1 & j2 + 1 > j2 ) by NAT_1:13;
A765: i2 <= len (Gauge (C,n)) by A758, MATRIX_0:32;
A766: ( i1 + 1 > i1 & i2 + 1 > i2 ) by NAT_1:13;

per cases by A760;

suppose ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

then right_cell (f,i,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) by A569, A755, A756, A757, A758, A759, A764, GOBRD13:def 2;
hence right_cell (f,i,(Gauge (C,n))) = Cl (Int (right_cell (f,i,(Gauge (C,n))))) by A761, A763, GOBRD11:35; :: thesis:

end;

suppose A767: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

A768: j1 -' 1 <= width (Gauge (C,n)) by A763, NAT_D:44;
right_cell (f,i,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,(j1 -' 1)) by A569, A755, A756, A757, A758, A759, A766, A767, GOBRD13:def 2;
hence right_cell (f,i,(Gauge (C,n))) = Cl (Int (right_cell (f,i,(Gauge (C,n))))) by A761, A768, GOBRD11:35; :: thesis:

end;

suppose ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

then right_cell (f,i,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) by A569, A755, A756, A757, A758, A759, A766, GOBRD13:def 2;
hence right_cell (f,i,(Gauge (C,n))) = Cl (Int (right_cell (f,i,(Gauge (C,n))))) by A765, A762, GOBRD11:35; :: thesis:

end;

suppose A769: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

A770: i1 -' 1 <= len (Gauge (C,n)) by A761, NAT_D:44;
right_cell (f,i,(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j2) by A569, A755, A756, A757, A758, A759, A764, A769, GOBRD13:def 2;
hence right_cell (f,i,(Gauge (C,n))) = Cl (Int (right_cell (f,i,(Gauge (C,n))))) by A762, A770, GOBRD11:35; :: thesis:

end;

now :: thesis:

A771: for h being non constant standard special_circular_sequence st L~ h c= L~ f holds
for Comp being Subset of (TOP-REAL 2) st Comp is_a_component_of (L~ h) ` holds
for n being Nat st 1 <= n & n + 1 <= len f & f /. n in Comp & not f /. n in L~ h holds
C meets Comp

proof

let h be non constant standard special_circular_sequence; :: thesis:
assume A772: L~ h c= L~ f ; :: thesis:
let Comp be Subset of (TOP-REAL 2); :: thesis:
assume A773: Comp is_a_component_of (L~ h) ` ; :: thesis:
let n be Nat; :: thesis:
assume that
A774: ( 1 <= n & n + 1 <= len f ) and
A775: f /. n in Comp and
A776: not f /. n in L~ h ; :: thesis:
reconsider rc = (right_cell (f,n,(Gauge (C,n)))) \ (L~ h) as Subset of (TOP-REAL 2) ;
f /. n in right_cell (f,n,(Gauge (C,n))) by A569, A774, Th8;
then f /. n in rc by A776, XBOOLE_0:def 5;
then A777: rc meets Comp by A775, XBOOLE_0:3;
A778: rc meets C

proof

right_cell (f,n,(Gauge (C,n))) meets C by A427, A774;
then consider p being object such that
A779: p in right_cell (f,n,(Gauge (C,n))) and
A780: p in C by XBOOLE_0:3;
reconsider p = p as Element of (TOP-REAL 2) by A779;

now :: thesis:

take a = p; :: thesis:

now :: thesis:

assume p in L~ h ; :: thesis:
then consider j being Nat such that
A781: ( 1 <= j & j + 1 <= len f ) and
A782: p in LSeg (f,j) by A772, SPPOL_2:13;
p in (left_cell (f,j,(Gauge (C,n)))) /\ (right_cell (f,j,(Gauge (C,n)))) by A427, A781, A782, GOBRD13:29;
then A783: p in left_cell (f,j,(Gauge (C,n))) by XBOOLE_0:def 4;
left_cell (f,j,(Gauge (C,n))) misses C by A427, A781;
hence contradiction by A780, A783, XBOOLE_0:3; :: thesis:

end;

hence a in rc by A779, XBOOLE_0:def 5; :: thesis:
thus a in C by A780; :: thesis:

end;

hence rc meets C by XBOOLE_0:3; :: thesis:

end;

end;

(L~ g) ` is open by TOPS_1:3;
then A788: (L~ g) ` = Int ((L~ g) `) by TOPS_1:23;
A789: L~ g c= L~ f by JORDAN3:40;
A790: for j, k being Nat st 1 <= j & j <= k holds
(F . k) /. j = (F . j) /. j

proof

let j, k be Nat; :: thesis:
assume that
A791: 1 <= j and
A792: j <= k ; :: thesis:
j <= len (F . k) by A192, A792;
then len ((F . k) | j) = j by FINSEQ_1:59;
then A793: j in dom ((F . k) | j) by A791, FINSEQ_3:25;
(F . k) | j = F . j by A488, A792;
hence (F . k) /. j = (F . j) /. j by A793, FINSEQ_4:70; :: thesis:

end;

assume m <> 1 ; :: thesis:
then A794: 1 < m by A568, XXREAL_0:1;
A795: for n being Nat st 1 <= n & n <= m -' 1 holds
not f /. n in L~ g

proof

A796: 2 <= len (Gauge (C,n)) by A231, NAT_1:12;
let n be Nat; :: thesis:
assume that
A797: 1 <= n and
A798: n <= m -' 1 ; :: thesis:
set p = f /. n;
A799: n <= len f by A575, A798, XXREAL_0:2;
then A800: f /. n in Values (Gauge (C,n)) by A427, A797, Th6;
assume f /. n in L~ g ; :: thesis:
then consider j being Nat such that
A801: (m -' 1) + 1 <= j and
A802: j + 1 <= len f and
A803: f /. n in LSeg (f,j) by A575, Th7;
A804: j < k by A578, A802, NAT_1:13;
A805: n < (m -' 1) + 1 by A798, NAT_1:13;
then A806: n < j by A801, XXREAL_0:2;
A807: (m -' 1) + 1 = m by A568, XREAL_1:235;
then A808: 1 < j by A794, A801, XXREAL_0:2;

per cases by A2, A427, A802, A803, A808, A796, A800, Th23;

suppose A809: f /. n = f /. j ; :: thesis:

A810: n <> len (F . j) by A192, A801, A805;
n <= len (F . j) by A192, A806;
then A811: n in dom (F . j) by A797, FINSEQ_3:25;
(F . j) /. n = (F . n) /. n by A790, A797, A806
.= f /. n by A578, A790, A797, A799
.= (F . j) /. j by A790, A808, A804, A809
.= (F . j) /. (len (F . j)) by A192 ;
hence contradiction by A564, A808, A804, A811, A810; :: thesis:

end;

suppose A812: f /. n = f /. (j + 1) ; :: thesis:

now :: thesis:

per cases by A578, A802, XXREAL_0:1;

suppose A813: j + 1 = k ; :: thesis:

A814: n <> len (F . m) by A192, A805, A807;
n <= len (F . m) by A192, A805, A807;
then A815: n in dom (F . m) by A797, FINSEQ_3:25;
(F . m) /. n = (F . n) /. n by A790, A797, A805, A807
.= (F . k) /. k by A578, A790, A797, A799, A812, A813
.= (F . m) /. m by A567, A578, A568, A570, A790
.= (F . m) /. (len (F . m)) by A192 ;
hence contradiction by A564, A578, A568, A571, A815, A814; :: thesis:

end;

suppose A816: j + 1 < k ; :: thesis:

set l = j + 1;
A817: 1 <= j + 1 by NAT_1:11;
A818: ( n < n + 1 & n + 1 < j + 1 ) by A806, XREAL_1:6, XREAL_1:29;
then A819: n <> len (F . (j + 1)) by A192;
A820: n < j + 1 by A818, XXREAL_0:2;
then n <= len (F . (j + 1)) by A192;
then A821: n in dom (F . (j + 1)) by A797, FINSEQ_3:25;
(F . (j + 1)) /. n = (F . n) /. n by A790, A797, A820
.= f /. n by A578, A790, A797, A799
.= (F . (j + 1)) /. (j + 1) by A790, A812, A816, A817
.= (F . (j + 1)) /. (len (F . (j + 1))) by A192 ;
hence contradiction by A564, A816, A821, A819, NAT_1:11; :: thesis:

end;

hence contradiction ; :: thesis:

end;

C meets RightComp (Rev g)

proof

1 <= len g by A622, XREAL_1:145;
then A822: ((len g) -' 1) + 2 = (len g) + 1 by Lm1;
A823: 1 - 1 < m - 1 by A794, XREAL_1:9;
A824: (m -' 1) + 2 = m + 1 by A568, Lm1;
set l = (m -' 1) + ((len g) -' 1);
set a = f /. (m -' 1);
set rg = Rev g;
set p = (Rev g) /. 1;
set q = (Rev g) /. 2;
A825: (1 + 1) - 1 <= (len g) - 1 by A621, XREAL_1:9;
(1 + 1) -' 1 <= (len g) -' 1 by A621, NAT_D:42;
then A826: 1 <= (len g) -' 1 by NAT_D:34;
then (m -' 1) + 1 <= (m -' 1) + ((len g) -' 1) by XREAL_1:6;
then m -' 1 < (m -' 1) + ((len g) -' 1) by NAT_1:13;
then A827: m -' 1 <> len (F . ((m -' 1) + ((len g) -' 1))) by A192;
A828: 1 + 1 <= len (Rev g) by A621, FINSEQ_5:def 3;
then (1 + 1) -' 1 <= (len (Rev g)) -' 1 by NAT_D:42;
then A829: 1 <= (len (Rev g)) -' 1 by NAT_D:34;
1 < len (Rev g) by A828, NAT_1:13;
then A830: ((len (Rev g)) -' 1) + 1 = len (Rev g) by XREAL_1:235;
A831: Rev g is_sequence_on Gauge (C,n) by A623, Th5;
then consider p1, p2, q1, q2 being Nat such that
A832: [p1,p2] in Indices (Gauge (C,n)) and
A833: (Rev g) /. 1 = (Gauge (C,n)) * (p1,p2) and
A834: [q1,q2] in Indices (Gauge (C,n)) and
A835: (Rev g) /. 2 = (Gauge (C,n)) * (q1,q2) and
A836: ( ( p1 = q1 & p2 + 1 = q2 ) or ( p1 + 1 = q1 & p2 = q2 ) or ( p1 = q1 + 1 & p2 = q2 ) or ( p1 = q1 & p2 = q2 + 1 ) ) by A828, JORDAN8:3;
A837: 1 <= p1 by A832, MATRIX_0:32;
A838: p2 <= width (Gauge (C,n)) by A832, MATRIX_0:32;
A839: p1 <= len (Gauge (C,n)) by A832, MATRIX_0:32;
A840: 1 <= p2 by A832, MATRIX_0:32;
A841: (Rev g) /. 1 = f /. m by A567, A577, FINSEQ_5:65;
(len g) -' 1 <= len g by NAT_D:44;
then A842: (len g) -' 1 in dom g by A826, FINSEQ_3:25;
then A843: (Rev g) /. 2 = g /. ((len g) -' 1) by A822, FINSEQ_5:66
.= f /. ((m -' 1) + ((len g) -' 1)) by A842, FINSEQ_5:27 ;
(m -' 1) + ((len g) -' 1) = (m + ((len g) -' 1)) -' 1 by A568, NAT_D:38
.= (((len g) -' 1) + m) - 1 by A826, NAT_D:37
.= (((len g) - 1) + m) - 1 by A825, XREAL_0:def 2
.= (((k - (m - 1)) - 1) + m) - 1 by A578, A576, A823, XREAL_0:def 2
.= k - 1 ;
then A844: k = ((m -' 1) + ((len g) -' 1)) + 1 ;
then A845: (m -' 1) + ((len g) -' 1) < k by XREAL_1:29;
(len g) -' 1 <= (m -' 1) + ((len g) -' 1) by NAT_1:11;
then A846: 1 <= (m -' 1) + ((len g) -' 1) by A826, XXREAL_0:2;
then A847: right_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) meets C by A427, A578, A844;
A848: (m -' 1) + 1 = m by A568, XREAL_1:235;
then A849: 1 <= m -' 1 by A794, NAT_1:13;
then A850: right_cell (f,(m -' 1),(Gauge (C,n))) meets C by A427, A570, A848;
m -' 1 <= (m -' 1) + ((len g) -' 1) by NAT_1:11;
then m -' 1 <= len (F . ((m -' 1) + ((len g) -' 1))) by A192;
then A851: m -' 1 in dom (F . ((m -' 1) + ((len g) -' 1))) by A849, FINSEQ_3:25;
not f /. (m -' 1) in L~ g by A795, A849;
then A852: not f /. (m -' 1) in L~ (Rev g) by SPPOL_2:22;

per cases by A836;

suppose A853: ( p1 = q1 & p2 + 1 = q2 ) ; :: thesis:

consider a1, a2, p91, p92 being Nat such that
A854: [a1,a2] in Indices (Gauge (C,n)) and
A855: f /. (m -' 1) = (Gauge (C,n)) * (a1,a2) and
A856: ( [p91,p92] in Indices (Gauge (C,n)) & (Rev g) /. 1 = (Gauge (C,n)) * (p91,p92) ) and
A857: ( ( a1 = p91 & a2 + 1 = p92 ) or ( a1 + 1 = p91 & a2 = p92 ) or ( a1 = p91 + 1 & a2 = p92 ) or ( a1 = p91 & a2 = p92 + 1 ) ) by A569, A570, A841, A848, A849, JORDAN8:3;
A858: 1 <= a2 by A854, MATRIX_0:32;
thus C meets RightComp (Rev g) :: thesis:

proof

per cases by A857;

suppose A859: ( a1 = p91 & a2 + 1 = p92 ) ; :: thesis:

A860: ( (m -' 1) + 1 <= len (F . m) & f /. ((m -' 1) + 1) = (F . m) /. m ) by A192, A578, A568, A570, A790, A848;
A861: (F . k) | (m + 1) = F . (m + 1) by A488, A578, A574;
A862: a1 = p1 by A832, A833, A856, A859, GOBOARD1:5;
A863: m -' 1 <= m by A848, NAT_1:11;
A864: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A578, A575, A790, A849
.= (F . m) /. (m -' 1) by A790, A849, A863 ;
A865: 2 in dom g by A621, FINSEQ_3:25;
A866: a2 + 1 = p2 by A832, A833, A856, A859, GOBOARD1:5;
then A867: p2 -' 1 = a2 by NAT_D:34;
right_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) = cell ((Gauge (C,n)),(p1 -' 1),p2) by A427, A567, A578, A841, A844, A846, A843, A832, A833, A834, A835, A853, GOBRD13:28
.= front_left_cell ((F . m),(m -' 1),(Gauge (C,n))) by A427, A841, A848, A849, A832, A833, A854, A855, A862, A866, A864, A860, GOBRD13:34 ;
then F . (m + 1) turns_left m -' 1, Gauge (C,n) by A456, A794, A847;
then A868: ( a2 + 1 > a2 & f turns_left m -' 1, Gauge (C,n) ) by A849, A824, A861, GOBRD13:44, NAT_1:13;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A822, FINSEQ_5:def 3;
then A869: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A865, FINSEQ_5:66
.= f /. (m + 1) by A824, A865, FINSEQ_5:27 ;
A870: (Rev g) /. 1 = g /. 1 by A567, A612, A577, FINSEQ_5:65
.= (Rev g) /. (len g) by FINSEQ_5:65
.= (Rev g) /. (len (Rev g)) by FINSEQ_5:def 3 ;
set rc = (right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g));
A871: RightComp (Rev g) is_a_component_of (L~ (Rev g)) ` by GOBOARD9:def 2;
A872: (p1 -' 1) + 1 = p1 by A837, XREAL_1:235;
A873: p2 + 1 > a2 + 1 by A866, NAT_1:13;
then A874: [(p1 -' 1),p2] in Indices (Gauge (C,n)) by A841, A848, A832, A833, A854, A855, A868;
then A875: 1 <= p1 -' 1 by MATRIX_0:32;
f /. (m + 1) = (Gauge (C,n)) * ((p1 -' 1),p2) by A841, A848, A832, A833, A854, A855, A873, A868;
then right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(p1 -' 1),a2) by A831, A829, A830, A832, A833, A874, A867, A872, A869, A870, GOBRD13:24;
then f /. (m -' 1) in right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) by A839, A838, A855, A858, A862, A866, A875, A872, Th20;
then A876: f /. (m -' 1) in (right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g)) by A852, XBOOLE_0:def 5;
( (right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g)) c= RightComp (Rev g) & L~ (Rev g) c= L~ f ) by A789, A831, A829, A830, Th27, SPPOL_2:22;
hence C meets RightComp (Rev g) by A570, A771, A848, A849, A852, A876, A871; :: thesis:

end;

suppose A877: ( a1 + 1 = p91 & a2 = p92 ) ; :: thesis:

then a1 + 1 = p1 by A832, A833, A856, GOBOARD1:5;
then A878: q1 -' 1 = a1 by A853, NAT_D:34;
a2 = p2 by A832, A833, A856, A877, GOBOARD1:5;
then right_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) = cell ((Gauge (C,n)),a1,a2) by A427, A567, A578, A841, A844, A846, A843, A832, A833, A834, A835, A853, A878, GOBRD13:28
.= left_cell (f,(m -' 1),(Gauge (C,n))) by A427, A570, A841, A848, A849, A854, A855, A856, A877, GOBRD13:23 ;
hence C meets RightComp (Rev g) by A427, A570, A848, A849, A847; :: thesis:

end;

suppose ( a1 = p91 + 1 & a2 = p92 ) ; :: thesis:

then ( a1 = p1 + 1 & a2 = p2 ) by A832, A833, A856, GOBOARD1:5;
then right_cell (f,(m -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),p1,p2) by A427, A570, A841, A848, A849, A832, A833, A854, A855, GOBRD13:26
.= left_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) by A427, A567, A578, A841, A844, A846, A843, A832, A833, A834, A835, A853, GOBRD13:27 ;
hence C meets RightComp (Rev g) by A427, A578, A844, A846, A850; :: thesis:

end;

suppose ( a1 = p91 & a2 = p92 + 1 ) ; :: thesis:

then A879: ( a1 = q1 & a2 = q2 ) by A832, A833, A853, A856, GOBOARD1:5;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A790, A849, NAT_1:11
.= (Rev g) /. 2 by A578, A575, A790, A849, A835, A855, A879
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A790, A845, A846, A843
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A192 ;
hence C meets RightComp (Rev g) by A564, A845, A846, A851, A827; :: thesis:

end;

suppose A880: ( p1 + 1 = q1 & p2 = q2 ) ; :: thesis:

consider a1, a2, p91, p92 being Nat such that
A881: [a1,a2] in Indices (Gauge (C,n)) and
A882: f /. (m -' 1) = (Gauge (C,n)) * (a1,a2) and
A883: ( [p91,p92] in Indices (Gauge (C,n)) & (Rev g) /. 1 = (Gauge (C,n)) * (p91,p92) ) and
A884: ( ( a1 = p91 & a2 + 1 = p92 ) or ( a1 + 1 = p91 & a2 = p92 ) or ( a1 = p91 + 1 & a2 = p92 ) or ( a1 = p91 & a2 = p92 + 1 ) ) by A569, A570, A841, A848, A849, JORDAN8:3;
A885: 1 <= a1 by A881, MATRIX_0:32;
thus C meets RightComp (Rev g) :: thesis:

proof

per cases by A884;

suppose A886: ( a1 = p91 & a2 + 1 = p92 ) ; :: thesis:

then a2 + 1 = p2 by A832, A833, A883, GOBOARD1:5;
then A887: q2 -' 1 = a2 by A880, NAT_D:34;
A888: a1 = p1 by A832, A833, A883, A886, GOBOARD1:5;
right_cell (f,(m -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),a1,a2) by A427, A570, A841, A848, A849, A881, A882, A883, A886, GOBRD13:22
.= left_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) by A427, A567, A578, A841, A844, A846, A843, A832, A833, A834, A835, A880, A888, A887, GOBRD13:25 ;
hence C meets RightComp (Rev g) by A427, A578, A844, A846, A850; :: thesis:

end;

suppose A889: ( a1 + 1 = p91 & a2 = p92 ) ; :: thesis:

A890: m -' 1 <= m by A848, NAT_1:11;
A891: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A578, A575, A790, A849
.= (F . m) /. (m -' 1) by A790, A849, A890 ;
A892: 2 in dom g by A621, FINSEQ_3:25;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A822, FINSEQ_5:def 3;
then A893: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A892, FINSEQ_5:66
.= f /. (m + 1) by A824, A892, FINSEQ_5:27 ;
A894: (Rev g) /. 1 = g /. 1 by A567, A612, A577, FINSEQ_5:65
.= (Rev g) /. (len g) by FINSEQ_5:65
.= (Rev g) /. (len (Rev g)) by FINSEQ_5:def 3 ;
A895: a2 = p2 by A832, A833, A883, A889, GOBOARD1:5;
A896: ( (m -' 1) + 1 <= len (F . m) & f /. ((m -' 1) + 1) = (F . m) /. m ) by A192, A578, A568, A570, A790, A848;
A897: (F . k) | (m + 1) = F . (m + 1) by A488, A578, A574;
set rc = (right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g));
A898: ( a1 < a1 + 1 & p1 < p1 + 1 ) by XREAL_1:29;
A899: a1 + 1 = p1 by A832, A833, A883, A889, GOBOARD1:5;
then A900: a1 = p1 -' 1 by NAT_D:34;
right_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) = cell ((Gauge (C,n)),p1,p2) by A427, A567, A578, A841, A844, A846, A843, A832, A833, A834, A835, A880, GOBRD13:26
.= front_left_cell ((F . m),(m -' 1),(Gauge (C,n))) by A427, A841, A848, A849, A832, A833, A881, A882, A899, A895, A891, A896, GOBRD13:36 ;
then F . (m + 1) turns_left m -' 1, Gauge (C,n) by A456, A794, A847;
then A901: f turns_left m -' 1, Gauge (C,n) by A849, A824, A897, GOBRD13:44;
then A902: [p1,(p2 + 1)] in Indices (Gauge (C,n)) by A841, A848, A832, A833, A881, A882, A899, A898;
then A903: p2 + 1 <= width (Gauge (C,n)) by MATRIX_0:32;
f /. (m + 1) = (Gauge (C,n)) * (p1,(p2 + 1)) by A841, A848, A832, A833, A881, A882, A899, A898, A901;
then right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(p1 -' 1),a2) by A831, A829, A830, A832, A833, A895, A902, A893, A894, GOBRD13:28;
then f /. (m -' 1) in right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) by A839, A840, A882, A885, A899, A895, A903, A900, Th20;
then A904: f /. (m -' 1) in (right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g)) by A852, XBOOLE_0:def 5;
A905: RightComp (Rev g) is_a_component_of (L~ (Rev g)) ` by GOBOARD9:def 2;
( (right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g)) c= RightComp (Rev g) & L~ (Rev g) c= L~ f ) by A789, A831, A829, A830, Th27, SPPOL_2:22;
hence C meets RightComp (Rev g) by A570, A771, A848, A849, A852, A904, A905; :: thesis:

end;

suppose ( a1 = p91 + 1 & a2 = p92 ) ; :: thesis:

then A906: ( a1 = q1 & a2 = q2 ) by A832, A833, A880, A883, GOBOARD1:5;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A790, A849, NAT_1:11
.= (Rev g) /. 2 by A578, A575, A790, A849, A835, A882, A906
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A790, A845, A846, A843
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A192 ;
hence C meets RightComp (Rev g) by A564, A845, A846, A851, A827; :: thesis:

end;

suppose ( a1 = p91 & a2 = p92 + 1 ) ; :: thesis:

then A907: ( a1 = p1 & a2 = p2 + 1 ) by A832, A833, A883, GOBOARD1:5;
right_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) = cell ((Gauge (C,n)),p1,p2) by A427, A567, A578, A841, A844, A846, A843, A832, A833, A834, A835, A880, GOBRD13:26
.= left_cell (f,(m -' 1),(Gauge (C,n))) by A427, A570, A841, A848, A849, A832, A833, A881, A882, A907, GOBRD13:27 ;
hence C meets RightComp (Rev g) by A427, A570, A848, A849, A847; :: thesis:

end;

suppose A908: ( p1 = q1 + 1 & p2 = q2 ) ; :: thesis:

consider a1, a2, p91, p92 being Nat such that
A909: [a1,a2] in Indices (Gauge (C,n)) and
A910: f /. (m -' 1) = (Gauge (C,n)) * (a1,a2) and
A911: ( [p91,p92] in Indices (Gauge (C,n)) & (Rev g) /. 1 = (Gauge (C,n)) * (p91,p92) ) and
A912: ( ( a1 = p91 & a2 + 1 = p92 ) or ( a1 + 1 = p91 & a2 = p92 ) or ( a1 = p91 + 1 & a2 = p92 ) or ( a1 = p91 & a2 = p92 + 1 ) ) by A569, A570, A841, A848, A849, JORDAN8:3;
A913: a1 <= len (Gauge (C,n)) by A909, MATRIX_0:32;
thus C meets RightComp (Rev g) :: thesis:

proof

per cases by A912;

suppose A914: ( a1 = p91 & a2 + 1 = p92 ) ; :: thesis:

then a2 + 1 = p2 by A832, A833, A911, GOBOARD1:5;
then A915: q2 -' 1 = a2 by A908, NAT_D:34;
a1 = p1 by A832, A833, A911, A914, GOBOARD1:5;
then A916: q1 = a1 -' 1 by A908, NAT_D:34;
right_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) = cell ((Gauge (C,n)),q1,(q2 -' 1)) by A427, A567, A578, A841, A844, A846, A843, A832, A833, A834, A835, A908, GOBRD13:24
.= left_cell (f,(m -' 1),(Gauge (C,n))) by A427, A570, A841, A848, A849, A909, A910, A911, A914, A916, A915, GOBRD13:21 ;
hence C meets RightComp (Rev g) by A427, A570, A848, A849, A847; :: thesis:

end;

suppose ( a1 + 1 = p91 & a2 = p92 ) ; :: thesis:

then A917: ( a1 + 1 = p1 & a2 = p2 ) by A832, A833, A911, GOBOARD1:5;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A790, A849, NAT_1:11
.= (Rev g) /. 2 by A578, A575, A790, A849, A835, A908, A910, A917
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A790, A845, A846, A843
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A192 ;
hence C meets RightComp (Rev g) by A564, A845, A846, A851, A827; :: thesis:

end;

suppose A918: ( a1 = p91 + 1 & a2 = p92 ) ; :: thesis:

A919: (Rev g) /. 1 = g /. 1 by A567, A612, A577, FINSEQ_5:65
.= (Rev g) /. (len g) by FINSEQ_5:65
.= (Rev g) /. (len (Rev g)) by FINSEQ_5:def 3 ;
A920: a1 = p1 + 1 by A832, A833, A911, A918, GOBOARD1:5;
p1 + 1 > p1 by XREAL_1:29;
then A921: a1 + 1 > p1 by A920, NAT_1:13;
A922: m -' 1 <= m by A848, NAT_1:11;
A923: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A578, A575, A790, A849
.= (F . m) /. (m -' 1) by A790, A849, A922 ;
A924: 2 in dom g by A621, FINSEQ_3:25;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A822, FINSEQ_5:def 3;
then A925: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A924, FINSEQ_5:66
.= f /. (m + 1) by A824, A924, FINSEQ_5:27 ;
A926: (F . k) | (m + 1) = F . (m + 1) by A488, A578, A574;
set rc = (right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g));
A927: RightComp (Rev g) is_a_component_of (L~ (Rev g)) ` by GOBOARD9:def 2;
A928: (p2 -' 1) + 1 = p2 by A840, XREAL_1:235;
A929: f /. ((m -' 1) + 1) = (F . m) /. m by A578, A568, A570, A790, A848;
A930: ( p1 -' 1 = q1 & (m -' 1) + 1 <= len (F . m) ) by A192, A848, A908, NAT_D:34;
A931: a2 = p2 by A832, A833, A911, A918, GOBOARD1:5;
right_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) = cell ((Gauge (C,n)),q1,(q2 -' 1)) by A427, A567, A578, A841, A844, A846, A843, A832, A833, A834, A835, A908, GOBRD13:24
.= front_left_cell ((F . m),(m -' 1),(Gauge (C,n))) by A427, A841, A848, A849, A832, A833, A908, A909, A910, A920, A931, A930, A923, A929, GOBRD13:38 ;
then F . (m + 1) turns_left m -' 1, Gauge (C,n) by A456, A794, A847;
then A932: f turns_left m -' 1, Gauge (C,n) by A849, A824, A926, GOBRD13:44;
A933: a2 + 1 > p2 by A931, NAT_1:13;
then A934: [p1,(p2 -' 1)] in Indices (Gauge (C,n)) by A841, A848, A832, A833, A909, A910, A931, A921, A932;
then A935: 1 <= p2 -' 1 by MATRIX_0:32;
f /. (m + 1) = (Gauge (C,n)) * (p1,(p2 -' 1)) by A841, A848, A832, A833, A909, A910, A931, A933, A921, A932;
then right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),p1,(p2 -' 1)) by A831, A829, A830, A832, A833, A934, A928, A925, A919, GOBRD13:22;
then f /. (m -' 1) in right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) by A837, A838, A910, A913, A920, A931, A935, A928, Th20;
then A936: f /. (m -' 1) in (right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g)) by A852, XBOOLE_0:def 5;
( (right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g)) c= RightComp (Rev g) & L~ (Rev g) c= L~ f ) by A789, A831, A829, A830, Th27, SPPOL_2:22;
hence C meets RightComp (Rev g) by A570, A771, A848, A849, A852, A936, A927; :: thesis:

end;

suppose A937: ( a1 = p91 & a2 = p92 + 1 ) ; :: thesis:

then a1 = p1 by A832, A833, A911, GOBOARD1:5;
then A938: q1 = a1 -' 1 by A908, NAT_D:34;
a2 = p2 + 1 by A832, A833, A911, A937, GOBOARD1:5;
then right_cell (f,(m -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),q1,q2) by A427, A570, A841, A848, A849, A908, A909, A910, A911, A937, A938, GOBRD13:28
.= left_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) by A427, A567, A578, A841, A844, A846, A843, A832, A833, A834, A835, A908, GOBRD13:23 ;
hence C meets RightComp (Rev g) by A427, A578, A844, A846, A850; :: thesis:

end;

suppose A939: ( p1 = q1 & p2 = q2 + 1 ) ; :: thesis:

consider a1, a2, p91, p92 being Nat such that
A940: [a1,a2] in Indices (Gauge (C,n)) and
A941: f /. (m -' 1) = (Gauge (C,n)) * (a1,a2) and
A942: ( [p91,p92] in Indices (Gauge (C,n)) & (Rev g) /. 1 = (Gauge (C,n)) * (p91,p92) ) and
A943: ( ( a1 = p91 & a2 + 1 = p92 ) or ( a1 + 1 = p91 & a2 = p92 ) or ( a1 = p91 + 1 & a2 = p92 ) or ( a1 = p91 & a2 = p92 + 1 ) ) by A569, A570, A841, A848, A849, JORDAN8:3;
A944: a2 <= width (Gauge (C,n)) by A940, MATRIX_0:32;
thus C meets RightComp (Rev g) :: thesis:

proof

per cases by A943;

suppose ( a1 = p91 & a2 + 1 = p92 ) ; :: thesis:

then A945: ( a1 = p1 & a2 + 1 = p2 ) by A832, A833, A942, GOBOARD1:5;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A790, A849, NAT_1:11
.= (Rev g) /. 2 by A578, A575, A790, A849, A835, A939, A941, A945
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A790, A845, A846, A843
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A192 ;
hence C meets RightComp (Rev g) by A564, A845, A846, A851, A827; :: thesis:

end;

suppose A946: ( a1 + 1 = p91 & a2 = p92 ) ; :: thesis:

then a2 = p2 by A832, A833, A942, GOBOARD1:5;
then A947: a2 -' 1 = q2 by A939, NAT_D:34;
a1 + 1 = p1 by A832, A833, A942, A946, GOBOARD1:5;
then A948: a1 = q1 -' 1 by A939, NAT_D:34;
right_cell (f,(m -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),a1,(a2 -' 1)) by A427, A570, A841, A848, A849, A940, A941, A942, A946, GOBRD13:24
.= left_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) by A427, A567, A578, A841, A844, A846, A843, A832, A833, A834, A835, A939, A948, A947, GOBRD13:21 ;
hence C meets RightComp (Rev g) by A427, A578, A844, A846, A850; :: thesis:

end;

suppose A949: ( a1 = p91 + 1 & a2 = p92 ) ; :: thesis:

then a2 = p2 by A832, A833, A942, GOBOARD1:5;
then A950: a2 -' 1 = q2 by A939, NAT_D:34;
A951: a1 = p1 + 1 by A832, A833, A942, A949, GOBOARD1:5;
right_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) = cell ((Gauge (C,n)),q1,q2) by A427, A567, A578, A841, A844, A846, A843, A832, A833, A834, A835, A939, GOBRD13:22
.= left_cell (f,(m -' 1),(Gauge (C,n))) by A427, A570, A841, A848, A849, A939, A940, A941, A942, A949, A951, A950, GOBRD13:25 ;
hence C meets RightComp (Rev g) by A427, A570, A848, A849, A847; :: thesis:

end;

suppose A952: ( a1 = p91 & a2 = p92 + 1 ) ; :: thesis:

set rc = (right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g));
A953: RightComp (Rev g) is_a_component_of (L~ (Rev g)) ` by GOBOARD9:def 2;
A954: 2 in dom g by A621, FINSEQ_3:25;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A822, FINSEQ_5:def 3;
then A955: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A954, FINSEQ_5:66
.= f /. (m + 1) by A824, A954, FINSEQ_5:27 ;
A956: (Rev g) /. 1 = g /. 1 by A567, A612, A577, FINSEQ_5:65
.= (Rev g) /. (len g) by FINSEQ_5:65
.= (Rev g) /. (len (Rev g)) by FINSEQ_5:def 3 ;
A957: a1 = p1 by A832, A833, A942, A952, GOBOARD1:5;
A958: m -' 1 <= m by A848, NAT_1:11;
A959: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A578, A575, A790, A849
.= (F . m) /. (m -' 1) by A790, A849, A958 ;
A960: ( p2 -' 1 = q2 & (m -' 1) + 1 <= len (F . m) ) by A192, A848, A939, NAT_D:34;
A961: f /. ((m -' 1) + 1) = (F . m) /. m by A578, A568, A570, A790, A848;
A962: (F . k) | (m + 1) = F . (m + 1) by A488, A578, A574;
A963: a2 = p2 + 1 by A832, A833, A942, A952, GOBOARD1:5;
right_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) = cell ((Gauge (C,n)),q1,q2) by A427, A567, A578, A841, A844, A846, A843, A832, A833, A834, A835, A939, GOBRD13:22
.= front_left_cell ((F . m),(m -' 1),(Gauge (C,n))) by A427, A841, A848, A849, A832, A833, A939, A940, A941, A957, A963, A960, A959, A961, GOBRD13:40 ;
then F . (m + 1) turns_left m -' 1, Gauge (C,n) by A456, A794, A847;
then A964: ( p2 + 1 > p2 & f turns_left m -' 1, Gauge (C,n) ) by A849, A824, A962, GOBRD13:44, NAT_1:13;
A965: a2 + 1 > p2 + 1 by A963, NAT_1:13;
then A966: [(p1 + 1),p2] in Indices (Gauge (C,n)) by A841, A848, A832, A833, A940, A941, A964;
then A967: p1 + 1 <= len (Gauge (C,n)) by MATRIX_0:32;
f /. (m + 1) = (Gauge (C,n)) * ((p1 + 1),p2) by A841, A848, A832, A833, A940, A941, A965, A964;
then right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),p1,p2) by A831, A829, A830, A832, A833, A966, A955, A956, GOBRD13:26;
then f /. (m -' 1) in right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) by A837, A840, A941, A944, A957, A963, A967, Th20;
then A968: f /. (m -' 1) in (right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g)) by A852, XBOOLE_0:def 5;
( (right_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g)) c= RightComp (Rev g) & L~ (Rev g) c= L~ f ) by A789, A831, A829, A830, Th27, SPPOL_2:22;
hence C meets RightComp (Rev g) by A570, A771, A848, A849, A852, A968, A953; :: thesis:

end;

then A969: ( LeftComp g is_a_component_of (L~ g) ` & C meets LeftComp g ) by GOBOARD9:24, GOBOARD9:def 1;
reconsider Lg9 = (L~ g) ` as Subset of (TOP-REAL 2) ;
A970: RightComp g is_a_component_of (L~ g) ` by GOBOARD9:def 2;
A971: C c= Lg9

proof

let c be object ; :: according to TARSKI:def 3 :: thesis:
assume that
A972: c in C and
A973: not c in Lg9 ; :: thesis:
reconsider c = c as Point of (TOP-REAL 2) by A972;
consider i being Nat such that
A974: 1 <= i and
A975: i + 1 <= len g and
A976: c in LSeg ((g /. i),(g /. (i + 1))) by A973, SPPOL_2:14, SUBSET_1:29;
A977: 1 <= i + (m -' 1) by A974, NAT_1:12;
i + 1 in dom g by A974, A975, SEQ_4:134;
then A978: g /. (i + 1) = f /. ((i + 1) + (m -' 1)) by FINSEQ_5:27;
(i + 1) + (m -' 1) = (i + (m -' 1)) + 1 ;
then A979: (i + (m -' 1)) + 1 <= (len g) + (m -' 1) by A975, XREAL_1:6;
i in dom g by A974, A975, SEQ_4:134;
then g /. i = f /. (i + (m -' 1)) by FINSEQ_5:27;
then c in LSeg (f,(i + (m -' 1))) by A576, A976, A978, A977, A979, TOPREAL1:def 3;
then c in (left_cell (f,(i + (m -' 1)),(Gauge (C,n)))) /\ (right_cell (f,(i + (m -' 1)),(Gauge (C,n)))) by A427, A576, A977, A979, GOBRD13:29;
then c in left_cell (f,(i + (m -' 1)),(Gauge (C,n))) by XBOOLE_0:def 4;
then left_cell (f,(i + (m -' 1)),(Gauge (C,n))) meets C by A972, XBOOLE_0:3;
hence contradiction by A427, A576, A977, A979; :: thesis:

end;

A980: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;
C meets RightComp g

proof

right_cell (f,m,(Gauge (C,n))) meets C by A427, A568, A574;
then consider p being object such that
A981: p in right_cell (f,m,(Gauge (C,n))) and
A982: p in C by XBOOLE_0:3;
reconsider p = p as Element of (TOP-REAL 2) by A981;

now :: thesis:

reconsider u = p as Element of (Euclid 2) by TOPREAL3:8;
take a = p; :: thesis:
thus a in C by A982; :: thesis:
consider r being Real such that
A983: r > 0 and
A984: Ball (u,r) c= (L~ g) ` by A971, A788, A982, GOBOARD6:5;
reconsider r = r as Real ;
A985: p in Ball (u,r) by A983, GOBOARD6:1;
reconsider B = Ball (u,r) as non empty Subset of (TOP-REAL 2) by A980, A983, GOBOARD6:1, TOPMETR:12;
A986: p in B by A983, GOBOARD6:1;
( right_cell (f,m,(Gauge (C,n))) = Cl (Int (right_cell (f,m,(Gauge (C,n))))) & B is open ) by A568, A574, A754, GOBOARD6:3;
then A987: Int (right_cell (f,m,(Gauge (C,n)))) meets B by A981, A985, TOPS_1:12;
( Int (right_cell (g,1,(Gauge (C,n)))) c= Int (right_cell (g,1)) & Int (right_cell (g,1)) c= RightComp g ) by A623, A622, GOBOARD9:25, GOBRD13:33, TOPS_1:19;
then Int (right_cell (g,1,(Gauge (C,n)))) c= RightComp g ;
then Int (right_cell (f,((m -' 1) + 1),(Gauge (C,n)))) c= RightComp g by A569, A575, A622, GOBRD13:32;
then ( B is connected & Int (right_cell (f,m,(Gauge (C,n)))) c= RightComp g ) by A568, SPRECT_3:7, XREAL_1:235;
then B c= RightComp g by A970, A984, A987, GOBOARD9:4;
hence a in RightComp g by A986; :: thesis:

end;

hence C meets RightComp g by XBOOLE_0:3; :: thesis:

end;

hence contradiction by A1, A970, A971, A969, Th1, SPRECT_4:6; :: thesis:

end;

then g = f /^ 0 by XREAL_1:232
.= f by FINSEQ_5:28 ;
then reconsider f = f as non constant standard special_circular_sequence ;
f is clockwise_oriented

proof

f /. 2 in LSeg ((f /. 1),(f /. (1 + 1))) by RLTOPSP1:68;
then A988: f /. 2 in L~ f by A572, SPPOL_2:15;
(NW-corner (L~ f)) `1 = W-bound (L~ f) by EUCLID:52;
then A989: (NW-corner (L~ f)) `1 <= (f /. 2) `1 by A988, PSCOMP_1:24;
len (Gauge (C,n)) >= 3 by A231, NAT_1:12;
then A990: 1 < len (Gauge (C,n)) by XXREAL_0:2;
(NE-corner (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;
then A991: (f /. 2) `1 <= (NE-corner (L~ f)) `1 by A988, PSCOMP_1:24;
for k being 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 ) by A427;
then A992: N-min (L~ f) = f /. 1 by A569, A606, Th30;
consider i being Nat such that
A993: 1 <= i and
A994: i + 1 <= len (Gauge (C,n)) and
A995: ( f /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) & f /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) ) and
N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) and
N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) by A606;
i < len (Gauge (C,n)) by A994, NAT_1:13;
then A996: ( (N-min (L~ f)) `2 = N-bound (L~ f) & ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 = ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 ) by A2, A990, A993, EUCLID:52, GOBOARD5:1;
1 <= i + 1 by NAT_1:12;
then A997: ((Gauge (C,n)) * ((i + 1),(width (Gauge (C,n))))) `2 = ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 by A2, A990, A994, GOBOARD5:1;
( (NW-corner (L~ f)) `2 = (NE-corner (L~ f)) `2 & (NE-corner (L~ f)) `2 = N-bound (L~ f) ) by EUCLID:52, PSCOMP_1:27;
then f /. 2 in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A992, A995, A996, A997, A989, A991, GOBOARD7:8;
then f /. 2 in (LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) /\ (L~ f) by A988, XBOOLE_0:def 4;
hence f is clockwise_oriented by A992, SPRECT_2:30; :: thesis:

end;

then reconsider f = f as non constant standard clockwise_oriented special_circular_sequence ;
take f ; :: thesis:
thus f is_sequence_on Gauge (C,n) by A427; :: thesis:
thus ex i being Nat st
( 1 <= i & i + 1 <= len (Gauge (C,n)) & f /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) & f /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) & N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) ) by A606; :: thesis:
let m be Nat; :: thesis:
assume that
A998: 1 <= m and
A999: m + 2 <= len f ; :: thesis:
A1000: F . ((m + 1) + 1) = f | ((m + 1) + 1) by A488, A578, A999;
A1001: m + 1 < m + 2 by XREAL_1:6;
then A1002: f | (m + 1) = F . (m + 1) by A488, A578, A999, XXREAL_0:2;
A1003: m + 1 <= len f by A999, A1001, XXREAL_0:2;
then A1004: front_left_cell ((F . (m + 1)),m,(Gauge (C,n))) = front_left_cell (f,m,(Gauge (C,n))) by A569, A998, A1002, GOBRD13:42;
A1005: ( m = (m + 1) -' 1 & m + 1 > 1 ) by A998, NAT_1:13, NAT_D:34;
A1006: front_right_cell ((F . (m + 1)),m,(Gauge (C,n))) = front_right_cell (f,m,(Gauge (C,n))) by A569, A998, A1003, A1002, GOBRD13:42;

hereby :: thesis:

assume ( front_left_cell (f,m,(Gauge (C,n))) misses C & front_right_cell (f,m,(Gauge (C,n))) misses C ) ; :: thesis:
then F . ((m + 1) + 1) turns_right m, Gauge (C,n) by A456, A1005, A1004, A1006;
hence f turns_right m, Gauge (C,n) by A998, A1000, GOBRD13:43; :: thesis:

end;

hereby :: thesis:

assume ( front_left_cell (f,m,(Gauge (C,n))) misses C & front_right_cell (f,m,(Gauge (C,n))) meets C ) ; :: thesis:
then F . ((m + 1) + 1) goes_straight m, Gauge (C,n) by A456, A1005, A1004, A1006;
hence f goes_straight m, Gauge (C,n) by A998, A1000, GOBRD13:45; :: thesis:

end;

assume front_left_cell (f,m,(Gauge (C,n))) meets C ; :: thesis:
then F . ((m + 1) + 1) turns_left m, Gauge (C,n) by A456, A1005, A1004;
hence f turns_left m, Gauge (C,n) by A998, A1000, GOBRD13:44; :: thesis: