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₁[ Element of NAT , set , set ] means ( ( $1 = 0 implies ex i being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT
for x being set ex y being set st S₁[k,x,y]

proof

let k be Element of NAT ; :: thesis:
let x be set ; :: thesis:
consider m being Element of 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 Th30;

per cases by NAT_1:26;

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;
thus ex y being set st S₁[k,x,y] :: thesis:

proof

per cases ;

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

thus ex y being set st S₁[k,x,y] :: thesis:

proof

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:237;
then A12: ((len f) -' 1) + (1 + 1) = (len f) + 1 ;
A13: ((len f) -' 1) + 1 in dom f by A7, A9, A11, FINSEQ_3:27;
A14: 1 <= (len f) -' 1 by A7, A9, NAT_D:49;
then consider i1, j1, i2, j2 being Element of 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:6;
A20: i1 <= len (Gauge C,n) by A15, MATRIX_1:39;
A21: 1 <= j2 + 1 by NAT_1:12;
A22: 1 <= i2 by A17, MATRIX_1:39;
A23: j1 <= width (Gauge C,n) by A15, MATRIX_1:39;
A24: 1 <= i2 + 1 by NAT_1:12;
A25: 1 <= j2 by A17, MATRIX_1:39;
(len f) -' 1 <= len f by NAT_D:35;
then A26: (len f) -' 1 in dom f by A14, FINSEQ_3:27;
A27: j2 <= width (Gauge C,n) by A17, MATRIX_1:39;
then A28: j2 -' 1 <= width (Gauge C,n) by NAT_D:44;
A29: i2 <= len (Gauge C,n) by A17, MATRIX_1:39;
then A30: i2 -' 1 <= len (Gauge C,n) by NAT_D:44;
thus ex y being set st S₁[k,x,y] :: thesis:

proof

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:

thus ex y being set st S₁[k,x,y] :: thesis:

proof

per cases by A19;

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

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

now

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

proof

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

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

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

now

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:8;
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:23;
hence contradiction by A2, A23, JORDAN8:19; :: thesis:

end;

hence [(i2' + 1),j2'] in Indices (Gauge C,n) by A25, A27, A24, A41, A42, MATRIX_1:37; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i2' + 1),j2' by A12, A41, A42, FINSEQ_4:82; :: thesis:

end;

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

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

end;

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

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

end;

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

hence ( [(i2' -' 1),j2'] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i2' -' 1),j2' ) 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

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

proof

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

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

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

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

end;

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

now

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:25;
then cell (Gauge C,n),i1,0 meets C by XREAL_1:234;
hence contradiction by A20, JORDAN8:20; :: thesis:

end;

hence [i2',(j2' -' 1)] in Indices (Gauge C,n) by A22, A29, A28, A50, A53, MATRIX_1:37; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i2',(j2' -' 1) by A12, A50, A53, FINSEQ_4:82; :: thesis:

end;

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

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

end;

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

hence ( [(i2' -' 1),j2'] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i2' -' 1),j2' ) 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

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

proof

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

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

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

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

end;

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

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

end;

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

now

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:8;
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:27;
hence contradiction by A29, JORDAN8:18; :: thesis:

end;

hence [i2',(j2' + 1)] in Indices (Gauge C,n) by A2, A22, A29, A21, A60, A63, MATRIX_1:37; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i2',(j2' + 1) by A12, A60, A63, FINSEQ_4:82; :: thesis:

end;

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

hence ( [(i2' -' 1),j2'] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i2' -' 1),j2' ) 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

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

proof

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

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

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

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

end;

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

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

end;

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

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

end;

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

now

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:29;
then cell (Gauge C,n),0 ,j2 meets C by XREAL_1:234;
hence contradiction by A2, A27, JORDAN8:21; :: thesis:

end;

hence [(i2' -' 1),j2'] in Indices (Gauge C,n) by A25, A27, A30, A74, A75, MATRIX_1:37; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i2' -' 1),j2' by A12, A74, A75, FINSEQ_4:82; :: 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:

thus ex y being set st S₁[k,x,y] :: thesis:

proof

per cases by A19;

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

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

now

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

proof

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

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

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

now

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:8;
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:36;
hence contradiction by A20, JORDAN8:18; :: thesis:

end;

hence [i2',(j2' + 1)] in Indices (Gauge C,n) by A2, A22, A29, A21, A86, A87, MATRIX_1:37; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i2',(j2' + 1) by A12, A86, A87, FINSEQ_4:82; :: thesis:

end;

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

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

end;

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

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

end;

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

hence ( [i2',(j2' -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i2',(j2' -' 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

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

proof

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

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

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

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

end;

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

now

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:8;
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:38;
hence contradiction by A2, A23, JORDAN8:19, NAT_D:44; :: thesis:

end;

hence [(i2' + 1),j2'] in Indices (Gauge C,n) by A25, A27, A24, A95, A98, MATRIX_1:37; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i2' + 1),j2' by A12, A95, A98, FINSEQ_4:82; :: thesis:

end;

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

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

end;

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

hence ( [i2',(j2' -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i2',(j2' -' 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

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

proof

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

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

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

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

end;

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

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

end;

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

now

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:40;
then cell (Gauge C,n),0 ,j1 meets C by XREAL_1:234;
hence contradiction by A2, A23, JORDAN8:21; :: thesis:

end;

hence [(i2' -' 1),j2'] in Indices (Gauge C,n) by A25, A27, A30, A106, A109, MATRIX_1:37; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i2' -' 1),j2' by A12, A106, A109, FINSEQ_4:82; :: thesis:

end;

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

hence ( [i2',(j2' -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i2',(j2' -' 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

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

proof

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

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

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

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

end;

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

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

end;

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

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

end;

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

now

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:42;
then cell (Gauge C,n),(i1 -' 1),0 meets C by XREAL_1:234;
hence contradiction by A20, JORDAN8:20, NAT_D:44; :: thesis:

end;

hence [i2',(j2' -' 1)] in Indices (Gauge C,n) by A22, A29, A28, A119, A120, MATRIX_1:37; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i2',(j2' -' 1) by A12, A119, A120, FINSEQ_4:82; :: 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:

thus ex y being set st S₁[k,x,y] :: thesis:

proof

per cases by A19;

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

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

now

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

proof

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

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

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

now

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:35;
then cell (Gauge C,n),0 ,j2 meets C by XREAL_1:234;
hence contradiction by A2, A27, JORDAN8:21; :: thesis:

end;

hence [(i2' -' 1),j2'] in Indices (Gauge C,n) by A25, A27, A30, A131, A132, MATRIX_1:37; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i2' -' 1),j2' by A12, A131, A132, FINSEQ_4:82; :: thesis:

end;

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

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

end;

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

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

end;

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

hence ( [(i2' + 1),j2'] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i2' + 1),j2' ) 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

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

proof

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

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

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

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

end;

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

now

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:8;
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:37;
hence contradiction by A29, JORDAN8:18; :: thesis:

end;

hence [i2',(j2' + 1)] in Indices (Gauge C,n) by A2, A22, A29, A21, A139, A142, MATRIX_1:37; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i2',(j2' + 1) by A12, A139, A142, FINSEQ_4:82; :: thesis:

end;

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

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

end;

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

hence ( [(i2' + 1),j2'] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i2' + 1),j2' ) 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

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

proof

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

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

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

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

end;

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

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

end;

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

now

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:39;
then cell (Gauge C,n),(i2 -' 1),0 meets C by XREAL_1:234;
hence contradiction by A29, JORDAN8:20, NAT_D:44; :: thesis:

end;

hence [i2',(j2' -' 1)] in Indices (Gauge C,n) by A22, A29, A28, A150, A153, MATRIX_1:37; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i2',(j2' -' 1) by A12, A150, A153, FINSEQ_4:82; :: thesis:

end;

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

hence ( [(i2' + 1),j2'] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i2' + 1),j2' ) 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

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

proof

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

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

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

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

end;

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

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

end;

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

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

end;

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

now

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:8;
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:41;
hence contradiction by A2, A27, JORDAN8:19, NAT_D:44; :: thesis:

end;

hence [(i2' + 1),j2'] in Indices (Gauge C,n) by A25, A27, A24, A163, A164, MATRIX_1:37; :: thesis:
thus f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i2' + 1),j2' by A12, A163, A164, FINSEQ_4:82; :: 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 Element of NAT holds S₁[k,F . k,F . (k + 1)] from RECDEF_1:sch 1(A3);
defpred S₂[ Element of NAT ] means F . $1 is FinSequence of (TOP-REAL 2);
A172: {} = <*> the carrier of (TOP-REAL 2) ;
A173: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

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

per cases by NAT_1:26;

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:

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

proof

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

per cases ;

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

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

proof

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 Element of 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 Element of 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 Element of 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 Element of NAT holds S₂[k] from NAT_1:sch 1(A182, A173);
rng F c= the carrier of (TOP-REAL 2) *

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng F ; :: thesis:
then ex x being set st
( x in dom F & F . x = y ) by FUNCT_1:def 5;
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 Function of NAT ,(the carrier of (TOP-REAL 2) * ) by A169, FUNCT_2:def 1, RELSET_1:11;
defpred S₃[ Element of NAT ] means len (F . $1) = $1;
A184: for k being Element of NAT st S₃[k] holds
S₃[k + 1]

proof

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

per cases by NAT_1:26;

suppose k = 0 ; :: thesis:

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

end;

suppose k = 1 ; :: thesis:

hence S₃[k + 1] by A186, FINSEQ_1:61; :: 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 Element of 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 Element of 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 Element of 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:19; :: 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:19; :: thesis:

end;

A191: S₃[ 0 ] by A170, CARD_1:47;
A192: for k being Element of NAT holds S₃[k] from NAT_1:sch 1(A191, A184);

A193: now

let k be Element of NAT ; :: thesis:
assume that
A194: F . k is_sequence_on Gauge C,n and
A195: for m being Element of 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:237;
then A198: right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C by A195;
let i1, j1, i2, j2 be Element of 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_1:39;
A204: 1 <= i2 + 1 by NAT_1:12;
A205: 1 <= j2 by A201, MATRIX_1:39;
A206: j2 <= width (Gauge C,n) by A201, MATRIX_1:39;
A207: j1 <= width (Gauge C,n) by A199, MATRIX_1:39;

hereby :: thesis:

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

now

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:8;
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:23;
hence contradiction by A2, A207, JORDAN8:19; :: thesis:

end;

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

end;

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

hereby :: thesis:

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

now

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:25;
then cell (Gauge C,n),i1,0 meets C by XREAL_1:234;
hence contradiction by A210, JORDAN8:20; :: thesis:

end;

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

end;

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

hereby :: thesis:

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

now

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:8;
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:27;
hence contradiction by A203, JORDAN8:18; :: thesis:

end;

hence [i2,(j2 + 1)] in Indices (Gauge C,n) by A2, A211, A203, A214, MATRIX_1:37; :: 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

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:29;
then cell (Gauge C,n),0 ,j2 meets C by XREAL_1:234;
hence contradiction by A2, A206, JORDAN8:21; :: thesis:

end;

hence [(i2 -' 1),j2] in Indices (Gauge C,n) by A205, A206, A217, MATRIX_1:37; :: 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

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:8;
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:36;
hence contradiction by A210, JORDAN8:18; :: thesis:

end;

hence [i2,(j2 + 1)] in Indices (Gauge C,n) by A2, A211, A203, A214, MATRIX_1:37; :: 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

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:8;
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:38;
hence contradiction by A2, A207, JORDAN8:19, NAT_D:44; :: thesis:

end;

hence [(i2 + 1),j2] in Indices (Gauge C,n) by A205, A206, A204, MATRIX_1:37; :: 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

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:40;
then cell (Gauge C,n),0 ,j1 meets C by XREAL_1:234;
hence contradiction by A2, A207, JORDAN8:21; :: thesis:

end;

hence [(i2 -' 1),j2] in Indices (Gauge C,n) by A205, A206, A217, MATRIX_1:37; :: 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

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:42;
then cell (Gauge C,n),(i1 -' 1),0 meets C by XREAL_1:234;
hence contradiction by A210, JORDAN8:20, NAT_D:44; :: thesis:

end;

hence [i2,(j2 -' 1)] in Indices (Gauge C,n) by A211, A203, A212, MATRIX_1:37; :: 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

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:35;
then cell (Gauge C,n),0 ,j2 meets C by XREAL_1:234;
hence contradiction by A2, A206, JORDAN8:21; :: thesis:

end;

hence [(i2 -' 1),j2] in Indices (Gauge C,n) by A205, A206, A217, MATRIX_1:37; :: 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

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:8;
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:37;
hence contradiction by A203, JORDAN8:18; :: thesis:

end;

hence [i2,(j2 + 1)] in Indices (Gauge C,n) by A2, A211, A203, A214, MATRIX_1:37; :: 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

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:39;
then cell (Gauge C,n),(i2 -' 1),0 meets C by XREAL_1:234;
hence contradiction by A203, JORDAN8:20, NAT_D:44; :: thesis:

end;

hence [i2,(j2 -' 1)] in Indices (Gauge C,n) by A211, A203, A212, MATRIX_1:37; :: 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

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:8;
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:41;
hence contradiction by A2, A206, JORDAN8:19, NAT_D:44; :: thesis:

end;

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

end;

defpred S₄[ Element of NAT ] means ( F . $1 is_sequence_on Gauge C,n & ( for m being Element of 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 Element of NAT st S₄[k] holds
S₄[k + 1]

proof

A233: 2 |^ n > 0 by NEWTON:102;
A234: 1 <= len (Gauge C,n) by A231, NAT_1:12;
let k be Element of NAT ; :: thesis:
assume that
A235: F . k is_sequence_on Gauge C,n and
A236: for m being Element of 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:26;

suppose A239: k = 0 ; :: thesis:

then consider i being Element of 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_1:37;

A244: now

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

end;

now

let l be Element of 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:27;
then l = 1 by XXREAL_0:1;
hence for i1, j1, i2, j2 being Element of 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
(abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A238, A239, A246, FINSEQ_3:27; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A244, GOBOARD1:def 11; :: thesis:
let m be Element of 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 Element of 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_1:37;
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_1:37;
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:26;

A258: now

let l be Element of 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:27;
then A261: ( l = 0 or l = 1 or l = 2 ) by NAT_1:27;
let i1, j1, i2, j2 be Element of 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:27, GOBOARD1:21;
then A263: abs (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:27, GOBOARD1:21;
then abs (i2 - i1) = 1 by ABSVALUE:def 1;
hence (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A263, UNIFORM1:13; :: thesis:

end;

now

let l be Element of NAT ; :: thesis:
assume A264: l in dom (F . (k + 1)) ; :: thesis:
then l <= 2 by A238, A249, FINSEQ_3:27;
then ( l = 0 or l = 1 or l = 2 ) by NAT_1:27;
hence ex i, j being Element of 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:27; :: thesis:

end;

hence A265: F . (k + 1) is_sequence_on Gauge C,n by A258, GOBOARD1:def 11; :: thesis:
A266: ( i < i + 1 & i + 1 < (i + 1) + 1 ) by NAT_1:13;
let m be Element of NAT ; :: thesis:
assume that
A267: 1 <= m and
A268: m + 1 <= len (F . (k + 1)) ; :: thesis:
1 + 1 <= m + 1 by A267, XREAL_1:8;
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

N-bound C > S-bound C by JORDAN8:12;
then (N-bound C) - (S-bound C) > (S-bound C) - (S-bound C) by XREAL_1:11;
then ((N-bound C) - (S-bound C)) / (2 |^ n) > 0 by A233, XREAL_1:141;
then A271: (N-bound C) + 0 < (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) by XREAL_1:8;
[1,(len (Gauge C,n))] in Indices (Gauge C,n) by A2, A234, MATRIX_1:37;
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:56;
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 set 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:71;
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:88 ;
then N-bound C < s by A278, A272, A271, XXREAL_0:2;
hence contradiction by A277, A276, EUCLID:56; :: 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:13;
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:27;
A281: ((len (F . k)) -' 1) + 1 = len (F . k) by A237, A279, XREAL_1:237;
then A282: ((len (F . k)) -' 1) + (1 + 1) = (len (F . k)) + 1 ;
A283: 1 <= (len (F . k)) -' 1 by A237, A279, NAT_D:49;
then consider i1, j1, i2, j2 being Element of NAT such that
A284: [i1,j1] in Indices (Gauge C,n) and
A285: (F . k) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 and
A286: [i2,j2] in Indices (Gauge C,n) and
A287: (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:6;
A288: ( i1 = i2 & j1 + 1 = j2 implies [(i2 + 1),j2] in Indices (Gauge C,n) ) by A193, A235, A236, A279, A284, A285, A286, A287;
A289: ( 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, A284, A285, A286, A287;
A290: ( 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, A284, A285, A286, A287;
A291: ( 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, A284, A285, A286, A287;
A292: ( 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, A284, A285, A286, A287;
A293: ( i1 = i2 + 1 & j1 = j2 implies [i2,(j2 + 1)] in Indices (Gauge C,n) ) by A193, A235, A236, A279, A284, A285, A286, A287;
A294: ( i1 + 1 = i2 & j1 = j2 implies [i2,(j2 -' 1)] in Indices (Gauge C,n) ) by A193, A235, A236, A279, A284, A285, A286, A287;
A295: 1 <= j2 by A286, MATRIX_1:39;
A296: right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C by A236, A283, A281;
A297: ( 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, A284, A285, A286, A287;
A298: ( 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, A284, A285, A286, A287;
A299: ( 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, A284, A285, A286, A287;
A300: ( i1 = i2 & j1 = j2 + 1 implies [(i2 -' 1),j2] in Indices (Gauge C,n) ) by A193, A235, A236, A279, A284, A285, A286, A287;
A301: ( 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, A284, A285, A286, A287;
(len (F . k)) -' 1 <= len (F . k) by NAT_D:35;
then A302: (len (F . k)) -' 1 in dom (F . k) by A283, FINSEQ_3:27;
A303: 1 <= i2 by A286, MATRIX_1:39;
thus A304: 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 Element of NAT such that
A305: (F . k) ^ <*((Gauge C,n) * i,j)*> turns_right (len (F . k)) -' 1, Gauge C,n and
A306: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A171, A235, A237, A279, A296;
thus F . (k + 1) is_sequence_on Gauge C,n :: thesis:

proof

set f = (F . k) ^ <*((Gauge C,n) * i,j)*>;
A307: ((F . k) ^ <*((Gauge C,n) * i,j)*>) /. ((len (F . k)) + 1) = (Gauge C,n) * i,j by FINSEQ_4:82;
A308: ( ((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 A285, A287, A302, A280, FINSEQ_4:83;

per cases by A281, A284, A286, A282, A305, A308, GOBRD13:def 6;

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

now

let i1', j1', i2', j2' be Element of NAT ; :: thesis:
assume A311: ( [i1',j1'] in Indices (Gauge C,n) & [i2',j2'] in Indices (Gauge C,n) & (F . k) /. (len (F . k)) = (Gauge C,n) * i1',j1' & (Gauge C,n) * (i2 + 1),j2 = (Gauge C,n) * i2',j2' ) ; :: thesis:
then ( j2 = j1' & j2 = j2' ) by A286, A287, A288, A309, GOBOARD1:21;
then A312: abs (j2' - j1') = 0 by ABSVALUE:def 1;
( i2 = i1' & i2 + 1 = i2' ) by A286, A287, A288, A309, A311, GOBOARD1:21;
hence (abs (i2' - i1')) + (abs (j2' - j1')) = 1 by A312, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A235, A237, A279, A288, A306, A307, A309, A310, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i1', j1', i2', j2' be Element of NAT ; :: thesis:
assume A315: ( [i1',j1'] in Indices (Gauge C,n) & [i2',j2'] in Indices (Gauge C,n) & (F . k) /. (len (F . k)) = (Gauge C,n) * i1',j1' & (Gauge C,n) * i2,(j2 -' 1) = (Gauge C,n) * i2',j2' ) ; :: thesis:
then ( j2 = j1' & j2 -' 1 = j2' ) by A286, A287, A294, A313, GOBOARD1:21;
then j1' - j2' = j2 - (j2 - 1) by A295, XREAL_1:235;
then A316: abs (j1' - j2') = 1 by ABSVALUE:def 1;
( i2 = i1' & i2 = i2' ) by A286, A287, A294, A313, A315, GOBOARD1:21;
then abs (i2' - i1') = 0 by ABSVALUE:def 1;
hence (abs (i2' - i1')) + (abs (j2' - j1')) = 1 by A316, UNIFORM1:13; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A235, A237, A279, A294, A306, A307, A313, A314, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i1', j1', i2', j2' be Element of NAT ; :: thesis:
assume A319: ( [i1',j1'] in Indices (Gauge C,n) & [i2',j2'] in Indices (Gauge C,n) & (F . k) /. (len (F . k)) = (Gauge C,n) * i1',j1' & (Gauge C,n) * i2,(j2 + 1) = (Gauge C,n) * i2',j2' ) ; :: thesis:
then ( i2 = i1' & i2 = i2' ) by A286, A287, A293, A317, GOBOARD1:21;
then A320: abs (i2' - i1') = 0 by ABSVALUE:def 1;
( j2 = j1' & j2 + 1 = j2' ) by A286, A287, A293, A317, A319, GOBOARD1:21;
hence (abs (i2' - i1')) + (abs (j2' - j1')) = 1 by A320, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A235, A237, A279, A293, A306, A307, A317, A318, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i1', j1', i2', j2' be Element of NAT ; :: thesis:
assume A323: ( [i1',j1'] in Indices (Gauge C,n) & [i2',j2'] in Indices (Gauge C,n) & (F . k) /. (len (F . k)) = (Gauge C,n) * i1',j1' & (Gauge C,n) * (i2 -' 1),j2 = (Gauge C,n) * i2',j2' ) ; :: thesis:
then ( i2 = i1' & i2 -' 1 = i2' ) by A286, A287, A300, A321, GOBOARD1:21;
then i1' - i2' = i2 - (i2 - 1) by A303, XREAL_1:235;
then A324: abs (i1' - i2') = 1 by ABSVALUE:def 1;
( j2 = j1' & j2 = j2' ) by A286, A287, A300, A321, A323, GOBOARD1:21;
then abs (j2' - j1') = 0 by ABSVALUE:def 1;
hence (abs (i2' - i1')) + (abs (j2' - j1')) = 1 by A324, UNIFORM1:13; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A235, A237, A279, A300, A306, A307, A321, A322, CARD_1:47, JORDAN8:9; :: thesis:

end;

suppose A325: ( 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 Element of NAT such that
A326: (F . k) ^ <*((Gauge C,n) * i,j)*> goes_straight (len (F . k)) -' 1, Gauge C,n and
A327: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A171, A235, A237, A279, A296;
thus F . (k + 1) is_sequence_on Gauge C,n :: thesis:

proof

set f = (F . k) ^ <*((Gauge C,n) * i,j)*>;
A328: ((F . k) ^ <*((Gauge C,n) * i,j)*>) /. ((len (F . k)) + 1) = (Gauge C,n) * i,j by FINSEQ_4:82;
A329: ( ((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 A285, A287, A302, A280, FINSEQ_4:83;

per cases by A281, A284, A286, A282, A326, A329, GOBRD13:def 8;

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

now

let i1', j1', i2', j2' be Element of NAT ; :: thesis:
assume A332: ( [i1',j1'] in Indices (Gauge C,n) & [i2',j2'] in Indices (Gauge C,n) & (F . k) /. (len (F . k)) = (Gauge C,n) * i1',j1' & (Gauge C,n) * i2,(j2 + 1) = (Gauge C,n) * i2',j2' ) ; :: thesis:
then ( i2 = i1' & i2 = i2' ) by A286, A287, A299, A325, A330, GOBOARD1:21;
then A333: abs (i2' - i1') = 0 by ABSVALUE:def 1;
( j2 = j1' & j2 + 1 = j2' ) by A286, A287, A299, A325, A330, A332, GOBOARD1:21;
hence (abs (i2' - i1')) + (abs (j2' - j1')) = 1 by A333, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A235, A237, A279, A299, A325, A327, A328, A330, A331, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i1', j1', i2', j2' be Element of NAT ; :: thesis:
assume A336: ( [i1',j1'] in Indices (Gauge C,n) & [i2',j2'] in Indices (Gauge C,n) & (F . k) /. (len (F . k)) = (Gauge C,n) * i1',j1' & (Gauge C,n) * (i2 + 1),j2 = (Gauge C,n) * i2',j2' ) ; :: thesis:
then ( j2 = j1' & j2 = j2' ) by A286, A287, A298, A325, A334, GOBOARD1:21;
then A337: abs (j2' - j1') = 0 by ABSVALUE:def 1;
( i2 = i1' & i2 + 1 = i2' ) by A286, A287, A298, A325, A334, A336, GOBOARD1:21;
hence (abs (i2' - i1')) + (abs (j2' - j1')) = 1 by A337, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A235, A237, A279, A298, A325, A327, A328, A334, A335, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i1', j1', i2', j2' be Element of NAT ; :: thesis:
assume A340: ( [i1',j1'] in Indices (Gauge C,n) & [i2',j2'] in Indices (Gauge C,n) & (F . k) /. (len (F . k)) = (Gauge C,n) * i1',j1' & (Gauge C,n) * (i2 -' 1),j2 = (Gauge C,n) * i2',j2' ) ; :: thesis:
then ( i2 = i1' & i2 -' 1 = i2' ) by A286, A287, A297, A325, A338, GOBOARD1:21;
then i1' - i2' = i2 - (i2 - 1) by A303, XREAL_1:235;
then A341: abs (i1' - i2') = 1 by ABSVALUE:def 1;
( j2 = j1' & j2 = j2' ) by A286, A287, A297, A325, A338, A340, GOBOARD1:21;
then abs (j2' - j1') = 0 by ABSVALUE:def 1;
hence (abs (i2' - i1')) + (abs (j2' - j1')) = 1 by A341, UNIFORM1:13; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A235, A237, A279, A297, A325, A327, A328, A338, A339, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i1', j1', i2', j2' be Element of NAT ; :: thesis:
assume A344: ( [i1',j1'] in Indices (Gauge C,n) & [i2',j2'] in Indices (Gauge C,n) & (F . k) /. (len (F . k)) = (Gauge C,n) * i1',j1' & (Gauge C,n) * i2,(j2 -' 1) = (Gauge C,n) * i2',j2' ) ; :: thesis:
then ( j2 = j1' & j2 -' 1 = j2' ) by A286, A287, A292, A325, A342, GOBOARD1:21;
then j1' - j2' = j2 - (j2 - 1) by A295, XREAL_1:235;
then A345: abs (j1' - j2') = 1 by ABSVALUE:def 1;
( i2 = i1' & i2 = i2' ) by A286, A287, A292, A325, A342, A344, GOBOARD1:21;
then abs (i2' - i1') = 0 by ABSVALUE:def 1;
hence (abs (i2' - i1')) + (abs (j2' - j1')) = 1 by A345, UNIFORM1:13; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A235, A237, A279, A292, A325, A327, A328, A342, A343, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

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

proof

set f = (F . k) ^ <*((Gauge C,n) * i,j)*>;
A349: ((F . k) ^ <*((Gauge C,n) * i,j)*>) /. ((len (F . k)) + 1) = (Gauge C,n) * i,j by FINSEQ_4:82;
A350: ( ((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 A285, A287, A302, A280, FINSEQ_4:83;

per cases by A281, A284, A286, A282, A347, A350, GOBRD13:def 7;

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

now

let i1', j1', i2', j2' be Element of NAT ; :: thesis:
assume A353: ( [i1',j1'] in Indices (Gauge C,n) & [i2',j2'] in Indices (Gauge C,n) & (F . k) /. (len (F . k)) = (Gauge C,n) * i1',j1' & (Gauge C,n) * (i2 -' 1),j2 = (Gauge C,n) * i2',j2' ) ; :: thesis:
then ( i2 = i1' & i2 -' 1 = i2' ) by A286, A287, A291, A346, A351, GOBOARD1:21;
then i1' - i2' = i2 - (i2 - 1) by A303, XREAL_1:235;
then A354: abs (i1' - i2') = 1 by ABSVALUE:def 1;
( j2 = j1' & j2 = j2' ) by A286, A287, A291, A346, A351, A353, GOBOARD1:21;
then abs (j2' - j1') = 0 by ABSVALUE:def 1;
hence (abs (i2' - i1')) + (abs (j2' - j1')) = 1 by A354, UNIFORM1:13; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A235, A237, A279, A291, A346, A348, A349, A351, A352, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i1', j1', i2', j2' be Element of NAT ; :: thesis:
assume A357: ( [i1',j1'] in Indices (Gauge C,n) & [i2',j2'] in Indices (Gauge C,n) & (F . k) /. (len (F . k)) = (Gauge C,n) * i1',j1' & (Gauge C,n) * i2,(j2 + 1) = (Gauge C,n) * i2',j2' ) ; :: thesis:
then ( i2 = i1' & i2 = i2' ) by A286, A287, A290, A346, A355, GOBOARD1:21;
then A358: abs (i2' - i1') = 0 by ABSVALUE:def 1;
( j2 = j1' & j2 + 1 = j2' ) by A286, A287, A290, A346, A355, A357, GOBOARD1:21;
hence (abs (i2' - i1')) + (abs (j2' - j1')) = 1 by A358, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A235, A237, A279, A290, A346, A348, A349, A355, A356, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i1', j1', i2', j2' be Element of NAT ; :: thesis:
assume A361: ( [i1',j1'] in Indices (Gauge C,n) & [i2',j2'] in Indices (Gauge C,n) & (F . k) /. (len (F . k)) = (Gauge C,n) * i1',j1' & (Gauge C,n) * i2,(j2 -' 1) = (Gauge C,n) * i2',j2' ) ; :: thesis:
then ( j2 = j1' & j2 -' 1 = j2' ) by A286, A287, A289, A346, A359, GOBOARD1:21;
then j1' - j2' = j2 - (j2 - 1) by A295, XREAL_1:235;
then A362: abs (j1' - j2') = 1 by ABSVALUE:def 1;
( i2 = i1' & i2 = i2' ) by A286, A287, A289, A346, A359, A361, GOBOARD1:21;
then abs (i2' - i1') = 0 by ABSVALUE:def 1;
hence (abs (i2' - i1')) + (abs (j2' - j1')) = 1 by A362, UNIFORM1:13; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A235, A237, A279, A289, A346, A348, A349, A359, A360, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i1', j1', i2', j2' be Element of NAT ; :: thesis:
assume A365: ( [i1',j1'] in Indices (Gauge C,n) & [i2',j2'] in Indices (Gauge C,n) & (F . k) /. (len (F . k)) = (Gauge C,n) * i1',j1' & (Gauge C,n) * (i2 + 1),j2 = (Gauge C,n) * i2',j2' ) ; :: thesis:
then ( j2 = j1' & j2 = j2' ) by A286, A287, A301, A346, A363, GOBOARD1:21;
then A366: abs (j2' - j1') = 0 by ABSVALUE:def 1;
( i2 = i1' & i2 + 1 = i2' ) by A286, A287, A301, A346, A363, A365, GOBOARD1:21;
hence (abs (i2' - i1')) + (abs (j2' - j1')) = 1 by A366, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A235, A237, A279, A301, A346, A348, A349, A363, A364, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

per cases ;

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

A371: (j2 -' 1) + 1 = j2 by A295, XREAL_1:237;
A372: (i2 -' 1) + 1 = i2 by A303, XREAL_1:237;
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 A373: ( 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 A374: ex i, j being Element of 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, A296;
then A375: (F . (k + 1)) /. (len (F . k)) = (Gauge C,n) * i2,j2 by A287, A280, FINSEQ_4:83;
A376: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 by A285, A302, A374, FINSEQ_4:83;

now

per cases by A281, A284, A286, A282, A374, A376, A375, GOBRD13:def 6;

suppose that A377: ( i1 = i2 & j1 + 1 = j2 ) and
A378: (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, A283, A281, A284, A285, A286, A287, A377, GOBRD13:36;
hence left_cell (F . (k + 1)),m,(Gauge C,n) misses C by A237, A238, A286, A288, A304, A367, A370, A373, A375, A377, A378, GOBRD13:24; :: thesis:
( j2 -' 1 = j1 & cell (Gauge C,n),i1,j1 meets C ) by A235, A283, A281, A284, A285, A286, A287, A296, A377, GOBRD13:23, NAT_D:34;
hence right_cell (F . (k + 1)),m,(Gauge C,n) meets C by A237, A238, A286, A288, A304, A367, A370, A375, A377, A378, GOBRD13:25; :: thesis:

end;

suppose that A379: ( i1 + 1 = i2 & j1 = j2 ) and
A380: (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, A283, A281, A284, A285, A286, A287, A379, GOBRD13:38;
hence left_cell (F . (k + 1)),m,(Gauge C,n) misses C by A237, A238, A286, A294, A304, A367, A370, A371, A373, A375, A379, A380, GOBRD13:28; :: thesis:
( i2 -' 1 = i1 & cell (Gauge C,n),i1,(j1 -' 1) meets C ) by A235, A283, A281, A284, A285, A286, A287, A296, A379, GOBRD13:25, NAT_D:34;
hence right_cell (F . (k + 1)),m,(Gauge C,n) meets C by A237, A238, A286, A294, A304, A367, A370, A371, A375, A379, A380, GOBRD13:29; :: thesis:

end;

suppose that A381: ( i1 = i2 + 1 & j1 = j2 ) and
A382: (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, A283, A281, A284, A285, A286, A287, A381, GOBRD13:40;
hence left_cell (F . (k + 1)),m,(Gauge C,n) misses C by A237, A238, A286, A293, A304, A367, A370, A373, A375, A381, A382, GOBRD13:22; :: thesis:
cell (Gauge C,n),i2,j2 meets C by A235, A283, A281, A284, A285, A286, A287, A296, A381, GOBRD13:27;
hence right_cell (F . (k + 1)),m,(Gauge C,n) meets C by A237, A238, A286, A293, A304, A367, A370, A375, A381, A382, GOBRD13:23; :: thesis:

end;

suppose that A383: ( i1 = i2 & j1 = j2 + 1 ) and
A384: (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, A283, A281, A284, A285, A286, A287, A383, GOBRD13:42;
hence left_cell (F . (k + 1)),m,(Gauge C,n) misses C by A237, A238, A286, A300, A304, A367, A370, A372, A373, A375, A383, A384, GOBRD13:26; :: thesis:
cell (Gauge C,n),(i2 -' 1),j2 meets C by A235, A283, A281, A284, A285, A286, A287, A296, A383, GOBRD13:29;
hence right_cell (F . (k + 1)),m,(Gauge C,n) meets C by A237, A238, A286, A300, A304, A367, A370, A372, A375, A383, A384, GOBRD13:27; :: 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 A385: ( 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 A386: ex i, j being Element of 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, A296;
then A387: (F . (k + 1)) /. (len (F . k)) = (Gauge C,n) * i2,j2 by A287, A280, FINSEQ_4:83;
A388: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 by A285, A302, A386, FINSEQ_4:83;

now

per cases by A281, A284, A286, A282, A386, A388, A387, GOBRD13:def 8;

suppose that A389: ( i1 = i2 & j1 + 1 = j2 ) and
A390: (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, A283, A281, A284, A285, A286, A287, A389, GOBRD13:35;
hence left_cell (F . (k + 1)),m,(Gauge C,n) misses C by A237, A238, A286, A299, A304, A367, A370, A385, A387, A389, A390, GOBRD13:22; :: thesis:
front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),i1,j2 by A235, A283, A281, A284, A285, A286, A287, A389, GOBRD13:36;
hence right_cell (F . (k + 1)),m,(Gauge C,n) meets C by A237, A238, A286, A299, A304, A367, A370, A385, A387, A389, A390, GOBRD13:23; :: thesis:

end;

suppose that A391: ( i1 + 1 = i2 & j1 = j2 ) and
A392: (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, A283, A281, A284, A285, A286, A287, A391, GOBRD13:37;
hence left_cell (F . (k + 1)),m,(Gauge C,n) misses C by A237, A238, A286, A298, A304, A367, A370, A385, A387, A391, A392, GOBRD13:24; :: thesis:
front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),i2,(j2 -' 1) by A235, A283, A281, A284, A285, A286, A287, A391, GOBRD13:38;
hence right_cell (F . (k + 1)),m,(Gauge C,n) meets C by A237, A238, A286, A298, A304, A367, A370, A385, A387, A391, A392, GOBRD13:25; :: thesis:

end;

suppose that A393: ( i1 = i2 + 1 & j1 = j2 ) and
A394: (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, A283, A281, A284, A285, A286, A287, A393, GOBRD13:39;
hence left_cell (F . (k + 1)),m,(Gauge C,n) misses C by A237, A238, A286, A297, A304, A367, A370, A372, A385, A387, A393, A394, GOBRD13:26; :: thesis:
front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),(i2 -' 1),j2 by A235, A283, A281, A284, A285, A286, A287, A393, GOBRD13:40;
hence right_cell (F . (k + 1)),m,(Gauge C,n) meets C by A237, A238, A286, A297, A304, A367, A370, A372, A385, A387, A393, A394, GOBRD13:27; :: thesis:

end;

suppose that A395: ( i1 = i2 & j1 = j2 + 1 ) and
A396: (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, A283, A281, A284, A285, A286, A287, A395, GOBRD13:41;
hence left_cell (F . (k + 1)),m,(Gauge C,n) misses C by A237, A238, A286, A292, A304, A367, A370, A371, A385, A387, A395, A396, GOBRD13:28; :: thesis:
front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),(i2 -' 1),(j2 -' 1) by A235, A283, A281, A284, A285, A286, A287, A395, GOBRD13:42;
hence right_cell (F . (k + 1)),m,(Gauge C,n) meets C by A237, A238, A286, A292, A304, A367, A370, A371, A385, A387, A395, A396, GOBRD13:29; :: 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 A397: front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C ; :: thesis:

then A398: ex i, j being Element of 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, A296;
then A399: (F . (k + 1)) /. (len (F . k)) = (Gauge C,n) * i2,j2 by A287, A280, FINSEQ_4:83;
A400: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 by A285, A302, A398, FINSEQ_4:83;

now

per cases by A281, A284, A286, A282, A398, A400, A399, GOBRD13:def 7;

suppose that A401: ( i1 = i2 & j1 + 1 = j2 ) and
A402: (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, A283, A281, A284, A285, A286, A287, A369, A401, GOBRD13:22, NAT_D:34;
hence left_cell (F . (k + 1)),m,(Gauge C,n) misses C by A237, A238, A286, A291, A304, A367, A370, A372, A397, A399, A401, A402, GOBRD13:26; :: thesis:
front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),(i1 -' 1),j2 by A235, A283, A281, A284, A285, A286, A287, A401, GOBRD13:35;
hence right_cell (F . (k + 1)),m,(Gauge C,n) meets C by A237, A238, A286, A291, A304, A367, A370, A372, A397, A399, A401, A402, GOBRD13:27; :: thesis:

end;

suppose that A403: ( i1 + 1 = i2 & j1 = j2 ) and
A404: (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, A283, A281, A284, A285, A286, A287, A369, A403, GOBRD13:24, NAT_D:34;
hence left_cell (F . (k + 1)),m,(Gauge C,n) misses C by A237, A238, A286, A290, A304, A367, A370, A397, A399, A403, A404, GOBRD13:22; :: thesis:
front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),i2,j2 by A235, A283, A281, A284, A285, A286, A287, A403, GOBRD13:37;
hence right_cell (F . (k + 1)),m,(Gauge C,n) meets C by A237, A238, A286, A290, A304, A367, A370, A397, A399, A403, A404, GOBRD13:23; :: thesis:

end;

suppose that A405: ( i1 = i2 + 1 & j1 = j2 ) and
A406: (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, A283, A281, A284, A285, A286, A287, A369, A405, GOBRD13:26;
hence left_cell (F . (k + 1)),m,(Gauge C,n) misses C by A237, A238, A286, A289, A304, A367, A370, A371, A397, A399, A405, A406, GOBRD13:28; :: thesis:
front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),(i2 -' 1),(j2 -' 1) by A235, A283, A281, A284, A285, A286, A287, A405, GOBRD13:39;
hence right_cell (F . (k + 1)),m,(Gauge C,n) meets C by A237, A238, A286, A289, A304, A367, A370, A371, A397, A399, A405, A406, GOBRD13:29; :: thesis:

end;

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

cell (Gauge C,n),i2,j2 misses C by A235, A283, A281, A284, A285, A286, A287, A369, A407, GOBRD13:28;
hence left_cell (F . (k + 1)),m,(Gauge C,n) misses C by A237, A238, A286, A301, A304, A367, A370, A397, A399, A407, A408, GOBRD13:24; :: thesis:
front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),i2,(j2 -' 1) by A235, A283, A281, A284, A285, A286, A287, A407, GOBRD13:41;
hence right_cell (F . (k + 1)),m,(Gauge C,n) meets C by A237, A238, A286, A301, A304, A367, A370, A397, A399, A407, A408, GOBRD13:25; :: 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 A368, XXREAL_0:1;
then A409: m + 1 <= len (F . k) by A237, A238, NAT_1:13;
then consider i1, j1, i2, j2 being Element of NAT such that
A410: [i1,j1] in Indices (Gauge C,n) and
A411: (F . k) /. m = (Gauge C,n) * i1,j1 and
A412: [i2,j2] in Indices (Gauge C,n) and
A413: (F . k) /. (m + 1) = (Gauge C,n) * i2,j2 and
A414: ( ( 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, A367, JORDAN8:6;
A415: ( left_cell (F . k),m,(Gauge C,n) misses C & right_cell (F . k),m,(Gauge C,n) meets C ) by A236, A367, A409;

A416: now

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 Element of NAT such that
(F . k) ^ <*((Gauge C,n) * i,j)*> turns_right (len (F . k)) -' 1, Gauge C,n and
A417: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A171, A235, A237, A279, A296;
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) misses C & front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C ) ; :: thesis:

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

end;

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

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

end;

1 <= m + 1 by NAT_1:12;
then m + 1 in dom (F . k) by A409, FINSEQ_3:27;
then A420: (F . (k + 1)) /. (m + 1) = (Gauge C,n) * i2,j2 by A413, A416, FINSEQ_4:83;
m <= len (F . k) by A409, NAT_1:13;
then m in dom (F . k) by A367, FINSEQ_3:27;
then A421: (F . (k + 1)) /. m = (Gauge C,n) * i1,j1 by A411, A416, FINSEQ_4:83;

now

per cases by A414;

suppose A422: ( 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, A367, A409, A410, A411, A412, A413, GOBRD13:22, GOBRD13:23;
hence ( left_cell (F . (k + 1)),m,(Gauge C,n) misses C & right_cell (F . (k + 1)),m,(Gauge C,n) meets C ) by A304, A367, A368, A410, A412, A415, A421, A420, A422, GOBRD13:22, GOBRD13:23; :: thesis:

end;

suppose A423: ( 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, A367, A409, A410, A411, A412, A413, GOBRD13:24, GOBRD13:25;
hence ( left_cell (F . (k + 1)),m,(Gauge C,n) misses C & right_cell (F . (k + 1)),m,(Gauge C,n) meets C ) by A304, A367, A368, A410, A412, A415, A421, A420, A423, GOBRD13:24, GOBRD13:25; :: thesis:

end;

suppose A424: ( 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, A367, A409, A410, A411, A412, A413, GOBRD13:26, GOBRD13:27;
hence ( left_cell (F . (k + 1)),m,(Gauge C,n) misses C & right_cell (F . (k + 1)),m,(Gauge C,n) meets C ) by A304, A367, A368, A410, A412, A415, A421, A420, A424, GOBRD13:26, GOBRD13:27; :: thesis:

end;

suppose A425: ( 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, A367, A409, A410, A411, A412, A413, GOBRD13:28, GOBRD13:29;
hence ( left_cell (F . (k + 1)),m,(Gauge C,n) misses C & right_cell (F . (k + 1)),m,(Gauge C,n) meets C ) by A304, A367, A368, A410, A412, A415, A421, A420, A425, GOBRD13:28, GOBRD13:29; :: 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 Element of NAT st
( w = $1 & $1 >= 1 & ex m being Element of NAT st
( m in dom (F . w) & m <> len (F . w) & (F . w) /. m = (F . w) /. (len (F . w)) ) );
A426: S₄[ 0 ]

proof

( ( for n being Element of NAT st n in dom (F . 0 ) holds
ex i, j being Element of NAT st
( [i,j] in Indices (Gauge C,n) & (F . 0 ) /. n = (Gauge C,n) * i,j ) ) & ( for n being Element of NAT st n in dom (F . 0 ) & n + 1 in dom (F . 0 ) holds
for m, k, i, j being Element of 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
(abs (m - i)) + (abs (k - j)) = 1 ) ) by A170;
hence F . 0 is_sequence_on Gauge C,n by GOBOARD1:def 11; :: thesis:
let m be Element of NAT ; :: thesis:
assume that
1 <= m and
A427: 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, A427, CARD_1:47; :: thesis:

end;

A428: for k being Element of NAT holds S₄[k] from NAT_1:sch 1(A426, A232);
A429: for k, i1, i2, j1, j2 being Element of 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 Element of NAT ; :: thesis:
assume that
A430: k > 1 and
A431: [i1,j1] in Indices (Gauge C,n) and
A432: (F . k) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 and
A433: [i2,j2] in Indices (Gauge C,n) and
A434: (F . k) /. (len (F . k)) = (Gauge C,n) * i2,j2 ; :: thesis:
A435: len (F . k) = k by A192;
then A436: ((len (F . k)) -' 1) + 1 = len (F . k) by A430, XREAL_1:237;
then A437: ((len (F . k)) -' 1) + (1 + 1) = (len (F . k)) + 1 ;
A438: 1 <= (len (F . k)) -' 1 by A430, A435, NAT_D:49;
then A439: right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C by A428, A436;
(len (F . k)) -' 1 <= len (F . k) by NAT_D:35;
then A440: (len (F . k)) -' 1 in dom (F . k) by A438, FINSEQ_3:27;
A441: ( j1 + 1 > j1 & j2 + 1 > j2 ) by NAT_1:13;
A442: F . k is_sequence_on Gauge C,n by A428;
A443: ( i1 + 1 > i1 & i2 + 1 > i2 ) by NAT_1:13;
A444: len (F . k) in dom (F . k) by A430, A435, FINSEQ_3:27;

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 Element of NAT such that
A445: (F . k) ^ <*((Gauge C,n) * i,j)*> turns_right (len (F . k)) -' 1, Gauge C,n and
A446: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A171, A430, A442, A435, A439;
thus F . (k + 1) turns_right (len (F . k)) -' 1, Gauge C,n by A445, A446; :: thesis:
A447: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge C,n) * i,j by A446, FINSEQ_4:82;
A448: ( (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 & (F . (k + 1)) /. (len (F . k)) = (Gauge C,n) * i2,j2 ) by A432, A434, A440, A444, A446, FINSEQ_4:83;
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 A431, A433, A436, A437, A441, A445, A446, A447, GOBRD13:def 6; :: 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 A431, A433, A436, A437, A443, A445, A446, A448, A447, GOBRD13:def 6; :: 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 A431, A433, A436, A437, A443, A445, A446, A448, A447, GOBRD13:def 6; :: 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 A431, A433, A436, A437, A441, A445, A446, A448, A447, GOBRD13:def 6; :: 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 Element of NAT such that
A449: (F . k) ^ <*((Gauge C,n) * i,j)*> goes_straight (len (F . k)) -' 1, Gauge C,n and
A450: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A171, A430, A442, A435, A439;
thus F . (k + 1) goes_straight (len (F . k)) -' 1, Gauge C,n by A449, A450; :: thesis:
A451: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge C,n) * i,j by A450, FINSEQ_4:82;
A452: ( (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 & (F . (k + 1)) /. (len (F . k)) = (Gauge C,n) * i2,j2 ) by A432, A434, A440, A444, A450, FINSEQ_4:83;
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 A431, A433, A436, A437, A441, A449, A450, A451, GOBRD13:def 8; :: 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 A431, A433, A436, A437, A443, A449, A450, A452, A451, GOBRD13:def 8; :: 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 A431, A433, A436, A437, A443, A449, A450, A452, A451, GOBRD13:def 8; :: 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 A431, A433, A436, A437, A441, A449, A450, A452, A451, GOBRD13:def 8; :: thesis:

end;

assume front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C ; :: thesis:
then consider i, j being Element of NAT such that
A453: (F . k) ^ <*((Gauge C,n) * i,j)*> turns_left (len (F . k)) -' 1, Gauge C,n and
A454: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A171, A430, A442, A435, A439;
A455: (F . (k + 1)) /. (len (F . k)) = (Gauge C,n) * i2,j2 by A434, A444, A454, FINSEQ_4:83;
thus F . (k + 1) turns_left (len (F . k)) -' 1, Gauge C,n by A453, A454; :: thesis:
A456: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge C,n) * i,j by A454, FINSEQ_4:82;
A457: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 by A432, A440, A454, FINSEQ_4:83;
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 A431, A433, A436, A437, A441, A453, A454, A455, A456, GOBRD13:def 7; :: 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 A431, A433, A436, A437, A443, A453, A454, A457, A455, A456, GOBRD13:def 7; :: 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 A431, A433, A436, A437, A443, A453, A454, A457, A455, A456, GOBRD13:def 7; :: 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 A431, A433, A436, A437, A441, A453, A454, A457, A455, A456, GOBRD13:def 7; :: thesis:

end;

A458: for k being Element of 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 Element of NAT ; :: thesis:
assume A459: k > 1 ; :: thesis:
A460: F . k is_sequence_on Gauge C,n by A428;
A461: len (F . k) = k by A192;
then ( 1 <= (len (F . k)) -' 1 & ((len (F . k)) -' 1) + 1 = len (F . k) ) by A459, NAT_D:49, XREAL_1:237;
then ex i1, j1, i2, j2 being Element of 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 A460, JORDAN8:6;
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 A429, A459, A461; :: thesis:

end;

defpred S₆[ Element of NAT ] means for m being Element of NAT st m <= $1 holds
(F . $1) | m = F . m;
A462: S₆[ 0 ]

proof

let m be Element of NAT ; :: thesis:
assume A463: m <= 0 ; :: thesis:
then (F . 0 ) | 0 = (F . 0 ) | m ;
hence (F . 0 ) | m = F . m by A170, A463; :: thesis:

end;

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

proof

let k be Element of NAT ; :: thesis:
A465: F . k is_sequence_on Gauge C,n by A428;
A466: len (F . k) = k by A192;
len (Gauge C,n) >= 4 by JORDAN8:13;
then A467: ( 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 A468: k < 1 ; :: thesis:

consider i being Element of NAT such that
A469: 1 <= i and
A470: 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
A471: 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 A470, NAT_1:13;
hence [i,j] in Indices (Gauge C,n) by A467, A469, MATRIX_1:37; :: thesis:
k = 0 by A468, NAT_1:14;
hence F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A170, A471, FINSEQ_1:47; :: thesis:

end;

suppose A472: k = 1 ; :: thesis:

consider i being Element of NAT such that
A473: 1 <= i and
A474: i + 1 <= len (Gauge C,n) and
A475: ( 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
A476: 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 A473, NAT_1:13;
hence [(i + 1),j] in Indices (Gauge C,n) by A467, A474, MATRIX_1:37; :: thesis:
consider i' being Element of NAT such that
A477: ( 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) ) and
A478: F . (1 + 1) = <*((Gauge C,n) * i',(width (Gauge C,n))),((Gauge C,n) * (i' + 1),(width (Gauge C,n)))*> by A171;
i = i' by A473, A474, A475, A477, Th31;
hence F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i + 1),j)*> by A472, A476, A478, FINSEQ_1:def 9; :: thesis:

end;

suppose A479: k > 1 ; :: thesis:

then ( 1 <= (len (F . k)) -' 1 & ((len (F . k)) -' 1) + 1 = len (F . k) ) by A466, NAT_D:49, XREAL_1:237;
then consider i1, j1, i2, j2 being Element of NAT such that
A480: ( [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
A481: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A465, JORDAN8:6;

now

per cases ;

suppose A482: ( 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

per cases by A481;

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 A429, A479, A480, A482;
hence ex i, j being Element of 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 A429, A479, A480, A482;
hence ex i, j being Element of 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 A429, A479, A480, A482;
hence ex i, j being Element of 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 A429, A479, A480, A482;
hence ex i, j being Element of 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 Element of NAT st
( [i,j] in Indices (Gauge C,n) & F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> ) ; :: thesis:

end;

suppose A483: ( 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

per cases by A481;

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 A429, A479, A480, A483;
hence ex i, j being Element of 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 A429, A479, A480, A483;
hence ex i, j being Element of 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 A429, A479, A480, A483;
hence ex i, j being Element of 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 A429, A479, A480, A483;
hence ex i, j being Element of 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 Element of NAT st
( [i,j] in Indices (Gauge C,n) & F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> ) ; :: thesis:

end;

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

now

per cases by A481;

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 A429, A479, A480, A484;
hence ex i, j being Element of 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 A429, A479, A480, A484;
hence ex i, j being Element of 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 A429, A479, A480, A484;
hence ex i, j being Element of 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 A429, A479, A480, A484;
hence ex i, j being Element of 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 Element of 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 Element of NAT st
( [i,j] in Indices (Gauge C,n) & F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> ) ; :: thesis:

end;

A485: for k being Element of NAT st S₆[k] holds
S₆[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A486: for m being Element of NAT st m <= k holds
(F . k) | m = F . m ; :: thesis:
let m be Element of NAT ; :: thesis:
assume A487: m <= k + 1 ; :: thesis:

per cases by A487, XXREAL_0:1;

suppose m < k + 1 ; :: thesis:

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

end;

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

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

end;

A490: for k being Element of NAT holds S₆[k] from NAT_1:sch 1(A462, A485);
defpred S₇[ Element of NAT ] means F . $1 is unfolded ;
A491: for k being Element of NAT st S₇[k] holds
S₇[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A492: F . k is unfolded ; :: thesis:
A493: F . k is_sequence_on Gauge C,n by A428;

per cases ;

suppose k <= 1 ; :: thesis:

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

end;

suppose A494: k > 1 ; :: thesis:

set m = k -' 1;
A495: (k -' 1) + 1 = k by A494, XREAL_1:237;
A496: len (F . k) = k by A192;
A497: 1 <= k -' 1 by A494, NAT_D:49;
then consider i1, j1, i2, j2 being Element of NAT such that
A498: [i1,j1] in Indices (Gauge C,n) and
A499: (F . k) /. (k -' 1) = (Gauge C,n) * i1,j1 and
A500: [i2,j2] in Indices (Gauge C,n) and
A501: (F . k) /. (len (F . k)) = (Gauge C,n) * i2,j2 and
A502: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A493, A495, A496, JORDAN8:6;
A503: LSeg (F . k),(k -' 1) = LSeg ((Gauge C,n) * i1,j1),((Gauge C,n) * i2,j2) by A497, A495, A496, A499, A501, TOPREAL1:def 5;
A504: 1 <= j2 by A500, MATRIX_1:39;
then A505: (j2 -' 1) + 1 = j2 by XREAL_1:237;
A506: 1 <= j1 by A498, MATRIX_1:39;
A507: 1 <= i2 by A500, MATRIX_1:39;
then A508: (i2 -' 1) + 1 = i2 by XREAL_1:237;
A509: i1 <= len (Gauge C,n) by A498, MATRIX_1:39;
A510: j2 <= width (Gauge C,n) by A500, MATRIX_1:39;
A511: 1 <= i1 by A498, MATRIX_1:39;
A512: j1 <= width (Gauge C,n) by A498, MATRIX_1:39;
A513: i2 <= len (Gauge C,n) by A500, MATRIX_1:39;

now

per cases ;

suppose A514: ( 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

per cases by A502;

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

then [(i2 + 1),j2] in Indices (Gauge C,n) by A429, A494, A496, A498, A499, A500, A501, A514;
then i2 + 1 <= len (Gauge C,n) by MATRIX_1:39;
then A516: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * (i2 + 1),j2)) = {((F . k) /. (len (F . k)))} by A501, A511, A506, A510, A503, A515, GOBOARD7:17;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 + 1),j2)*> by A429, A494, A496, A498, A499, A500, A501, A514, A515;
hence S₇[k + 1] by A492, A495, A496, A516, SPPOL_2:31; :: thesis:

end;

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

then [i2,(j2 -' 1)] in Indices (Gauge C,n) by A429, A494, A496, A498, A499, A500, A501, A514;
then 1 <= j2 -' 1 by MATRIX_1:39;
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 A501, A511, A512, A513, A505, A503, A517, GOBOARD7:18;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 -' 1))*> by A429, A494, A496, A498, A499, A500, A501, A514, A517;
hence S₇[k + 1] by A492, A495, A496, A518, SPPOL_2:31; :: thesis:

end;

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

then [i2,(j2 + 1)] in Indices (Gauge C,n) by A429, A494, A496, A498, A499, A500, A501, A514;
then j2 + 1 <= width (Gauge C,n) by MATRIX_1:39;
then A520: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * i2,(j2 + 1))) = {((F . k) /. (len (F . k)))} by A501, A509, A506, A507, A503, A519, GOBOARD7:19;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 + 1))*> by A429, A494, A496, A498, A499, A500, A501, A514, A519;
hence S₇[k + 1] by A492, A495, A496, A520, SPPOL_2:31; :: thesis:

end;

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

then [(i2 -' 1),j2] in Indices (Gauge C,n) by A429, A494, A496, A498, A499, A500, A501, A514;
then 1 <= i2 -' 1 by MATRIX_1:39;
then A522: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * (i2 -' 1),j2)) = {((F . k) /. (len (F . k)))} by A501, A509, A512, A504, A508, A503, A521, GOBOARD7:20;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 -' 1),j2)*> by A429, A494, A496, A498, A499, A500, A501, A514, A521;
hence S₇[k + 1] by A492, A495, A496, A522, SPPOL_2:31; :: thesis:

end;

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

end;

suppose A523: ( 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

per cases by A502;

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

then [i2,(j2 + 1)] in Indices (Gauge C,n) by A429, A494, A496, A498, A499, A500, A501, A523;
then A525: j2 + 1 <= width (Gauge C,n) by MATRIX_1:39;
j2 + 1 = j1 + (1 + 1) by A524;
then A526: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * i2,(j2 + 1))) = {((F . k) /. (len (F . k)))} by A501, A511, A509, A506, A503, A524, A525, GOBOARD7:15;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 + 1))*> by A429, A494, A496, A498, A499, A500, A501, A523, A524;
hence S₇[k + 1] by A492, A495, A496, A526, SPPOL_2:31; :: thesis:

end;

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

then [(i2 + 1),j2] in Indices (Gauge C,n) by A429, A494, A496, A498, A499, A500, A501, A523;
then A528: i2 + 1 <= len (Gauge C,n) by MATRIX_1:39;
i2 + 1 = i1 + (1 + 1) by A527;
then A529: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * (i2 + 1),j2)) = {((F . k) /. (len (F . k)))} by A501, A511, A506, A512, A503, A527, A528, GOBOARD7:16;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 + 1),j2)*> by A429, A494, A496, A498, A499, A500, A501, A523, A527;
hence S₇[k + 1] by A492, A495, A496, A529, SPPOL_2:31; :: thesis:

end;

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

then [(i2 -' 1),j2] in Indices (Gauge C,n) by A429, A494, A496, A498, A499, A500, A501, A523;
then A531: 1 <= i2 -' 1 by MATRIX_1:39;
((i2 -' 1) + 1) + 1 = (i2 -' 1) + (1 + 1) ;
then A532: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * (i2 -' 1),j2)) = {((F . k) /. (len (F . k)))} by A501, A509, A506, A512, A508, A503, A530, A531, GOBOARD7:16;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 -' 1),j2)*> by A429, A494, A496, A498, A499, A500, A501, A523, A530;
hence S₇[k + 1] by A492, A495, A496, A532, SPPOL_2:31; :: thesis:

end;

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

then [i2,(j2 -' 1)] in Indices (Gauge C,n) by A429, A494, A496, A498, A499, A500, A501, A523;
then A534: 1 <= j2 -' 1 by MATRIX_1:39;
((j2 -' 1) + 1) + 1 = (j2 -' 1) + (1 + 1) ;
then A535: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * i2,(j2 -' 1))) = {((F . k) /. (len (F . k)))} by A501, A511, A509, A512, A505, A503, A533, A534, GOBOARD7:15;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 -' 1))*> by A429, A494, A496, A498, A499, A500, A501, A523, A533;
hence S₇[k + 1] by A492, A495, A496, A535, SPPOL_2:31; :: thesis:

end;

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

end;

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

now

per cases by A502;

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

then [(i2 -' 1),j2] in Indices (Gauge C,n) by A429, A494, A496, A498, A499, A500, A501, A536;
then 1 <= i2 -' 1 by MATRIX_1:39;
then A538: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * (i2 -' 1),j2)) = {((F . k) /. (len (F . k)))} by A501, A509, A506, A510, A508, A503, A537, GOBOARD7:18;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 -' 1),j2)*> by A429, A494, A496, A498, A499, A500, A501, A536, A537;
hence S₇[k + 1] by A492, A495, A496, A538, SPPOL_2:31; :: thesis:

end;

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

then [i2,(j2 + 1)] in Indices (Gauge C,n) by A429, A494, A496, A498, A499, A500, A501, A536;
then j2 + 1 <= width (Gauge C,n) by MATRIX_1:39;
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 A501, A511, A506, A513, A503, A539, GOBOARD7:20;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 + 1))*> by A429, A494, A496, A498, A499, A500, A501, A536, A539;
hence S₇[k + 1] by A492, A495, A496, A540, SPPOL_2:31; :: thesis:

end;

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

then [i2,(j2 -' 1)] in Indices (Gauge C,n) by A429, A494, A496, A498, A499, A500, A501, A536;
then 1 <= j2 -' 1 by MATRIX_1:39;
then A542: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * i2,(j2 -' 1))) = {((F . k) /. (len (F . k)))} by A501, A509, A512, A507, A505, A503, A541, GOBOARD7:17;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 -' 1))*> by A429, A494, A496, A498, A499, A500, A501, A536, A541;
hence S₇[k + 1] by A492, A495, A496, A542, SPPOL_2:31; :: thesis:

end;

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

then [(i2 + 1),j2] in Indices (Gauge C,n) by A429, A494, A496, A498, A499, A500, A501, A536;
then i2 + 1 <= len (Gauge C,n) by MATRIX_1:39;
then A544: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * (i2 + 1),j2)) = {((F . k) /. (len (F . k)))} by A501, A511, A512, A504, A503, A543, GOBOARD7:19;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 + 1),j2)*> by A429, A494, A496, A498, A499, A500, A501, A536, A543;
hence S₇[k + 1] by A492, A495, A496, A544, SPPOL_2:31; :: thesis:

end;

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

end;

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

end;

now

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

proof

let k be Element of NAT ; :: thesis:
assume A547: F . k is one-to-one ; :: thesis:

now

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

per cases by A551, A556, NAT_1:8;

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

then A558: m in dom (F . k) by A552, A555, FINSEQ_3:27;
then A559: (F . (k + 1)) /. m = (F . k) /. m by A554, FINSEQ_4:83;
A560: n in dom (F . k) by A553, A555, A557, FINSEQ_3:27;
then (F . (k + 1)) /. n = (F . k) /. n by A554, FINSEQ_4:83;
hence n = m by A547, A550, A560, A558, A559, PARTFUN2:17; :: thesis:

end;

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

hence n = m by A545, A549, A550, A556, NAT_1:12; :: thesis:

end;

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

hence n = m by A545, A548, A550, A556, NAT_1:12; :: thesis:

end;

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

hence n = m ; :: thesis:

end;

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

end;

A561: S₈[ 0 ] by A170;
A562: for k being Element of NAT holds S₈[k] from NAT_1:sch 1(A561, A546);
A563: for k being Element of NAT holds card (rng (F . k)) = k

proof

let k be Element of NAT ; :: thesis:
F . k is one-to-one by A562;
hence card (rng (F . k)) = len (F . k) by FINSEQ_4:77
.= 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 A428;
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, GOBRD13:9, NAT_1:44;
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 A563; :: thesis:

end;

then A564: ex k being Nat st S₅[k] ;
consider k being Nat such that
A565: S₅[k] and
A566: for l being Nat st S₅[l] holds
k <= l from NAT_1:sch 5(A564);
reconsider k = k as Element of NAT by ORDINAL1:def 13;
consider m being Element of NAT such that
A567: m in dom (F . k) and
A568: m <> len (F . k) and
A569: (F . k) /. m = (F . k) /. (len (F . k)) by A565;
A570: 1 <= m by A567, FINSEQ_3:27;
reconsider f = F . k as non empty FinSequence of (TOP-REAL 2) by A565;
A571: f is_sequence_on Gauge C,n by A428;
A572: m <= len f by A567, FINSEQ_3:27;
then A573: m < len f by A568, XXREAL_0:1;
then 1 < len f by A570, XXREAL_0:2;
then A574: len f >= 1 + 1 by NAT_1:13;
A575: S₇[ 0 ] by A170, CARD_1:47, SPPOL_2:27;
for k being Element of NAT holds S₇[k] from NAT_1:sch 1(A575, A491);
then reconsider f = f as non constant non empty special unfolded FinSequence of (TOP-REAL 2) by A571, A574, JORDAN8:7, JORDAN8:8;
A576: m + 1 <= len f by A573, 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 A577: m -' 1 < len f by A576, XXREAL_0:2;
then A578: len (f /^ (m -' 1)) = (len f) - (m -' 1) by RFINSEQ:def 2;
then (m -' 1) - (m -' 1) < len (f /^ (m -' 1)) by A577, XREAL_1:11;
then reconsider g = f /^ (m -' 1) as non empty FinSequence of (TOP-REAL 2) by CARD_1:47;
len g in dom g by FINSEQ_5:6;
then A579: g /. (len g) = f /. ((m -' 1) + (len g)) by FINSEQ_5:30
.= f /. (len f) by A578 ;
A580: len (F . k) = k by A192;
A581: for j, i being Element of NAT st 1 <= i & i < len g & 1 <= j & j < len g & g /. i = g /. j holds
i = j

proof

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

per cases by A587, XXREAL_0:1;

suppose A592: i < j ; :: thesis:

set l = (m -' 1) + j;
set m' = (m -' 1) + i;
A593: (m -' 1) + i < (m -' 1) + j by A592, XREAL_1:8;
A594: len (F . ((m -' 1) + j)) = (m -' 1) + j by A192;
A595: (m -' 1) + j < k by A580, A578, A585, XREAL_1:22;
then A596: f | ((m -' 1) + j) = F . ((m -' 1) + j) by A490;
0 + j <= (m -' 1) + j by XREAL_1:8;
then A597: 1 <= (m -' 1) + j by A584, XXREAL_0:2;
then (m -' 1) + j in dom (F . ((m -' 1) + j)) by A594, FINSEQ_3:27;
then A598: (F . ((m -' 1) + j)) /. ((m -' 1) + j) = f /. ((m -' 1) + j) by A596, FINSEQ_4:85;
0 + i <= (m -' 1) + i by XREAL_1:8;
then 1 <= (m -' 1) + i by A582, XXREAL_0:2;
then A599: (m -' 1) + i in dom (F . ((m -' 1) + j)) by A593, A594, FINSEQ_3:27;
then (F . ((m -' 1) + j)) /. ((m -' 1) + i) = f /. ((m -' 1) + i) by A596, FINSEQ_4:85;
hence contradiction by A566, A586, A589, A590, A593, A595, A597, A594, A599, A598, FINSEQ_5:30; :: thesis:

end;

suppose A600: j < i ; :: thesis:

set l = (m -' 1) + i;
set m' = (m -' 1) + j;
A601: (m -' 1) + j < (m -' 1) + i by A600, XREAL_1:8;
A602: len (F . ((m -' 1) + i)) = (m -' 1) + i by A192;
A603: (m -' 1) + i < k by A580, A578, A583, XREAL_1:22;
then A604: f | ((m -' 1) + i) = F . ((m -' 1) + i) by A490;
0 + i <= (m -' 1) + i by XREAL_1:8;
then A605: 1 <= (m -' 1) + i by A582, XXREAL_0:2;
then (m -' 1) + i in dom (F . ((m -' 1) + i)) by A602, FINSEQ_3:27;
then A606: (F . ((m -' 1) + i)) /. ((m -' 1) + i) = f /. ((m -' 1) + i) by A604, FINSEQ_4:85;
0 + j <= (m -' 1) + j by XREAL_1:8;
then 1 <= (m -' 1) + j by A584, XXREAL_0:2;
then A607: (m -' 1) + j in dom (F . ((m -' 1) + i)) by A601, A602, FINSEQ_3:27;
then (F . ((m -' 1) + i)) /. ((m -' 1) + j) = f /. ((m -' 1) + j) by A604, FINSEQ_4:85;
hence contradiction by A566, A586, A588, A591, A601, A603, A605, A602, A607, A606, FINSEQ_5:30; :: thesis:

end;

A608: now

consider i being Element of NAT such that
A609: ( 1 <= i & i + 1 <= len (Gauge C,n) ) and
A610: ( 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
A611: 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 A609; :: thesis:
A612: f | 2 = F . 2 by A490, A580, A574;
A613: len (f | 2) = 2 by A574, FINSEQ_1:80;
then 1 in dom (f | 2) by FINSEQ_3:27;
hence f /. 1 = (f | 2) /. 1 by FINSEQ_4:85
.= (Gauge C,n) * i,(width (Gauge C,n)) by A611, A612, FINSEQ_4:26 ;
:: thesis:
2 in dom (f | 2) by A613, FINSEQ_3:27;
hence f /. 2 = (f | 2) /. 2 by FINSEQ_4:85
.= (Gauge C,n) * (i + 1),(width (Gauge C,n)) by A611, A612, FINSEQ_4:26 ;
:: 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 A610; :: thesis:

end;

1 in dom g by FINSEQ_5:6;
then A614: g /. 1 = f /. ((m -' 1) + 1) by FINSEQ_5:30
.= f /. m by A570, XREAL_1:237 ;
A615: for j, i being Element of NAT st 1 < i & i < j & j <= len g holds
g /. i <> g /. j

proof

let j, i be Element of NAT ; :: thesis:
assume that
A616: 1 < i and
A617: i < j and
A618: j <= len g and
A619: g /. i = g /. j ; :: thesis:
A620: 1 < j by A616, A617, XXREAL_0:2;
A621: i < len g by A617, A618, XXREAL_0:2;
then A622: 1 < len g by A616, XXREAL_0:2;

per cases ;

suppose j <> len g ; :: thesis:

then j < len g by A618, XXREAL_0:1;
hence contradiction by A581, A616, A617, A619, A620, A621; :: thesis:

end;

suppose j = len g ; :: thesis:

hence contradiction by A569, A614, A579, A581, A616, A617, A619, A622; :: thesis:

end;

(m + 1) - (m -' 1) <= len g by A576, A578, XREAL_1:11;
then A623: (m + 1) - (m - 1) <= len g by A570, XREAL_1:235;
then A624: ((1 + m) - m) + 1 <= len g ;
A625: g is_sequence_on Gauge C,n by A428, JORDAN8:5;
then A626: g is standard by JORDAN8:7;
A627: not g is constant

proof

take 1 ; :: according to GOBOARD1:def 2 :: thesis:
take 2 ; :: thesis:
thus A628: 1 in dom g by FINSEQ_5:6; :: thesis:
thus A629: 2 in dom g by A623, FINSEQ_3:27; :: thesis:
then g /. 1 <> g /. (1 + 1) by A626, FINSEQ_5:6, GOBOARD7:31;
then g . 1 <> g /. (1 + 1) by A628, PARTFUN1:def 8;
hence not g . 1 = g . 2 by A629, PARTFUN1:def 8; :: thesis:

end;

A630: for j, i being Element of NAT st 1 <= i & i < j & j < len g holds
g /. i <> g /. j

proof

let j, i be Element of NAT ; :: thesis:
assume that
A631: ( 1 <= i & i < j & j < len g ) and
A632: g /. i = g /. j ; :: thesis:
( 1 < j & i < len g ) by A631, XXREAL_0:2;
hence contradiction by A581, A631, A632; :: thesis:

end;

g is s.c.c.

proof

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

per cases by A634, NAT_1:14;

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

then A641: j + 1 <= len g by NAT_1:13;
then A642: LSeg g,j = LSeg (g /. j),(g /. (j + 1)) by A635, TOPREAL1:def 5;
consider i1', j1', i2', j2' being Element of NAT such that
A643: [i1',j1'] in Indices (Gauge C,n) and
A644: g /. j = (Gauge C,n) * i1',j1' and
A645: [i2',j2'] in Indices (Gauge C,n) and
A646: g /. (j + 1) = (Gauge C,n) * i2',j2' and
A647: ( ( i1' = i2' & j1' + 1 = j2' ) or ( i1' + 1 = i2' & j1' = j2' ) or ( i1' = i2' + 1 & j1' = j2' ) or ( i1' = i2' & j1' = j2' + 1 ) ) by A625, A635, A641, JORDAN8:6;
A648: 1 <= i1' by A643, MATRIX_1:39;
A649: j2' <= width (Gauge C,n) by A645, MATRIX_1:39;
A650: 1 <= i2' by A645, MATRIX_1:39;
A651: i1' <= len (Gauge C,n) by A643, MATRIX_1:39;
A652: 1 <= j2' by A645, MATRIX_1:39;
A653: j1' <= width (Gauge C,n) by A643, MATRIX_1:39;
A654: i2' <= len (Gauge C,n) by A645, MATRIX_1:39;
A655: 1 <= j1' by A643, MATRIX_1:39;
A656: i + 1 < len g by A633, A640, XXREAL_0:2;
then A657: LSeg g,i = LSeg (g /. i),(g /. (i + 1)) by A640, TOPREAL1:def 5;
A658: i < len g by A656, NAT_1:13;
consider i1, j1, i2, j2 being Element of NAT such that
A659: [i1,j1] in Indices (Gauge C,n) and
A660: g /. i = (Gauge C,n) * i1,j1 and
A661: [i2,j2] in Indices (Gauge C,n) and
A662: g /. (i + 1) = (Gauge C,n) * i2,j2 and
A663: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A625, A640, A656, JORDAN8:6;
A664: 1 <= i1 by A659, MATRIX_1:39;
A665: j2 <= width (Gauge C,n) by A661, MATRIX_1:39;
A666: j1 <= width (Gauge C,n) by A659, MATRIX_1:39;
A667: 1 <= j2 by A661, MATRIX_1:39;
A668: 1 <= j1 by A659, MATRIX_1:39;
A669: i2 <= len (Gauge C,n) by A661, MATRIX_1:39;
A670: i1 <= len (Gauge C,n) by A659, MATRIX_1:39;
A671: 1 < i + 1 by A640, NAT_1:13;
assume A672: LSeg g,i meets LSeg g,j ; :: thesis:
A673: 1 <= i2 by A661, MATRIX_1:39;

now

per cases by A663, A647;

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

then A675: ( j1 = j1' or j1 = j1' + 1 or j1 + 1 = j1' ) by A657, A660, A662, A664, A670, A668, A665, A642, A644, A646, A648, A651, A655, A649, A672, GOBOARD7:24;
i1 = i1' by A657, A660, A662, A664, A670, A668, A665, A642, A644, A646, A648, A651, A655, A649, A672, A674, GOBOARD7:21;
hence contradiction by A581, A615, A633, A637, A636, A635, A639, A640, A656, A658, A660, A662, A641, A644, A646, A674, A675; :: thesis:

end;

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

then ( ( i1 = i1' & j1 = j1' ) or ( i1 = i1' & j1 + 1 = j1' ) or ( i1 = i1' + 1 & j1 = j1' ) or ( i1 = i1' + 1 & j1 + 1 = j1' ) ) by A657, A660, A662, A664, A670, A668, A665, A642, A644, A646, A648, A655, A653, A654, A672, GOBOARD7:23;
hence contradiction by A581, A615, A633, A638, A635, A639, A640, A671, A658, A660, A662, A641, A644, A646, A676; :: thesis:

end;

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

then ( ( i1 = i2' & j1' = j1 ) or ( i1 = i2' & j1 + 1 = j1' ) or ( i1 = i2' + 1 & j1' = j1 ) or ( i1 = i2' + 1 & j1 + 1 = j1' ) ) by A657, A660, A662, A664, A670, A668, A665, A642, A644, A646, A651, A655, A653, A650, A672, GOBOARD7:23;
hence contradiction by A581, A615, A633, A638, A635, A639, A640, A671, A658, A660, A662, A641, A644, A646, A677; :: thesis:

end;

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

then A679: ( j1 = j2' or j1 = j2' + 1 or j1 + 1 = j2' ) by A657, A660, A662, A664, A670, A668, A665, A642, A644, A646, A648, A651, A653, A652, A672, GOBOARD7:24;
i1 = i1' by A657, A660, A662, A664, A670, A668, A665, A642, A644, A646, A648, A651, A653, A652, A672, A678, GOBOARD7:21;
hence contradiction by A581, A615, A633, A638, A635, A640, A671, A658, A660, A662, A641, A644, A646, A678, A679; :: thesis:

end;

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

then ( ( i1' = i1 & j1 = j1' ) or ( i1' = i1 & j1' + 1 = j1 ) or ( i1' = i1 + 1 & j1 = j1' ) or ( i1' = i1 + 1 & j1' + 1 = j1 ) ) by A657, A660, A662, A664, A668, A666, A669, A642, A644, A646, A648, A651, A655, A649, A672, GOBOARD7:23;
hence contradiction by A581, A615, A633, A638, A635, A639, A640, A671, A658, A660, A662, A641, A644, A646, A680; :: thesis:

end;

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

then A682: ( i1 = i1' or i1 = i1' + 1 or i1 + 1 = i1' ) by A657, A660, A662, A664, A668, A666, A669, A642, A644, A646, A648, A655, A653, A654, A672, GOBOARD7:25;
j1 = j1' by A657, A660, A662, A664, A668, A666, A669, A642, A644, A646, A648, A655, A653, A654, A672, A681, GOBOARD7:22;
hence contradiction by A581, A615, A633, A637, A636, A635, A639, A640, A656, A658, A660, A662, A641, A644, A646, A681, A682; :: thesis:

end;

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

then A684: ( i1 = i2' or i1 = i2' + 1 or i1 + 1 = i2' ) by A657, A660, A662, A664, A668, A666, A669, A642, A644, A646, A651, A655, A653, A650, A672, GOBOARD7:25;
j1 = j1' by A657, A660, A662, A664, A668, A666, A669, A642, A644, A646, A651, A655, A653, A650, A672, A683, GOBOARD7:22;
hence contradiction by A581, A615, A638, A635, A639, A640, A671, A658, A660, A662, A641, A644, A646, A683, A684; :: thesis:

end;

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

then ( ( i1' = i1 & j1 = j2' ) or ( i1' = i1 & j2' + 1 = j1 ) or ( i1' = i1 + 1 & j1 = j2' ) or ( i1' = i1 + 1 & j2' + 1 = j1 ) ) by A657, A660, A662, A664, A668, A666, A669, A642, A644, A646, A648, A651, A653, A652, A672, GOBOARD7:23;
hence contradiction by A581, A615, A633, A638, A635, A639, A640, A671, A658, A660, A662, A641, A644, A646, A685; :: thesis:

end;

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

then ( ( i1' = i2 & j1' = j1 ) or ( i1' = i2 & j1' + 1 = j1 ) or ( i1' = i2 + 1 & j1' = j1 ) or ( i1' = i2 + 1 & j1' + 1 = j1 ) ) by A657, A660, A662, A670, A668, A666, A673, A642, A644, A646, A648, A651, A655, A649, A672, GOBOARD7:23;
hence contradiction by A581, A615, A633, A638, A635, A639, A640, A671, A658, A660, A662, A641, A644, A646, A686; :: thesis:

end;

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

then A688: ( i2 = i1' or i2 = i1' + 1 or i2 + 1 = i1' ) by A657, A660, A662, A670, A668, A666, A673, A642, A644, A646, A648, A655, A653, A654, A672, GOBOARD7:25;
j1 = j1' by A657, A660, A662, A670, A668, A666, A673, A642, A644, A646, A648, A655, A653, A654, A672, A687, GOBOARD7:22;
hence contradiction by A581, A615, A633, A638, A635, A640, A671, A658, A660, A662, A641, A644, A646, A687, A688; :: thesis:

end;

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

then A690: ( i2 = i2' or i2 = i2' + 1 or i2 + 1 = i2' ) by A657, A660, A662, A670, A668, A666, A673, A642, A644, A646, A651, A655, A653, A650, A672, GOBOARD7:25;
j1 = j1' by A657, A660, A662, A670, A668, A666, A673, A642, A644, A646, A651, A655, A653, A650, A672, A689, GOBOARD7:22;
hence contradiction by A615, A633, A638, A639, A640, A671, A660, A662, A641, A644, A646, A689, A690; :: thesis:

end;

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

then ( ( i1' = i2 & j2' = j1 ) or ( i1' = i2 & j2' + 1 = j1 ) or ( i1' = i2 + 1 & j2' = j1 ) or ( i1' = i2 + 1 & j2' + 1 = j1 ) ) by A657, A660, A662, A670, A668, A666, A673, A642, A644, A646, A648, A651, A653, A652, A672, GOBOARD7:23;
hence contradiction by A581, A615, A633, A638, A635, A639, A640, A671, A658, A660, A662, A641, A644, A646, A691; :: thesis:

end;

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

then A693: ( j2 = j1' or j2 = j1' + 1 or j2 + 1 = j1' ) by A657, A660, A662, A664, A670, A666, A667, A642, A644, A646, A648, A651, A655, A649, A672, GOBOARD7:24;
i1 = i1' by A657, A660, A662, A664, A670, A666, A667, A642, A644, A646, A648, A651, A655, A649, A672, A692, GOBOARD7:21;
hence contradiction by A581, A615, A633, A638, A635, A640, A671, A658, A660, A662, A641, A644, A646, A692, A693; :: thesis:

end;

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

then ( ( i1 = i1' & j2 = j1' ) or ( i1 = i1' & j2 + 1 = j1' ) or ( i1 = i1' + 1 & j2 = j1' ) or ( i1 = i1' + 1 & j2 + 1 = j1' ) ) by A657, A660, A662, A664, A670, A666, A667, A642, A644, A646, A648, A655, A653, A654, A672, GOBOARD7:23;
hence contradiction by A581, A615, A633, A638, A635, A639, A640, A671, A658, A660, A662, A641, A644, A646, A694; :: thesis:

end;

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

then ( ( i1 = i2' & j2 = j1' ) or ( i1 = i2' & j2 + 1 = j1' ) or ( i1 = i2' + 1 & j2 = j1' ) or ( i1 = i2' + 1 & j2 + 1 = j1' ) ) by A657, A660, A662, A664, A670, A666, A667, A642, A644, A646, A651, A655, A653, A650, A672, GOBOARD7:23;
hence contradiction by A581, A615, A633, A638, A635, A639, A640, A671, A658, A660, A662, A641, A644, A646, A695; :: thesis:

end;

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

then A697: ( j2 = j2' or j2 = j2' + 1 or j2 + 1 = j2' ) by A657, A660, A662, A664, A670, A666, A667, A642, A644, A646, A648, A651, A653, A652, A672, GOBOARD7:24;
i1 = i1' by A657, A660, A662, A664, A670, A666, A667, A642, A644, A646, A648, A651, A653, A652, A672, A696, GOBOARD7:21;
hence contradiction by A615, A633, A638, A639, A640, A671, A660, A662, A641, A644, A646, A696, A697; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

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

end;

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

then A699: i + 1 < len g by A638, XXREAL_0:2;
then A700: LSeg g,i = LSeg (g /. i),(g /. (i + 1)) by A698, TOPREAL1:def 5;
A701: i < len g by A699, NAT_1:13;
consider i1, j1, i2, j2 being Element of NAT such that
A702: [i1,j1] in Indices (Gauge C,n) and
A703: g /. i = (Gauge C,n) * i1,j1 and
A704: [i2,j2] in Indices (Gauge C,n) and
A705: g /. (i + 1) = (Gauge C,n) * i2,j2 and
A706: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A625, A698, A699, JORDAN8:6;
A707: 1 <= i1 by A702, MATRIX_1:39;
A708: j2 <= width (Gauge C,n) by A704, MATRIX_1:39;
A709: j1 <= width (Gauge C,n) by A702, MATRIX_1:39;
A710: 1 <= j2 by A704, MATRIX_1:39;
A711: 1 <= j1 by A702, MATRIX_1:39;
A712: i2 <= len (Gauge C,n) by A704, MATRIX_1:39;
A713: i1 <= len (Gauge C,n) by A702, MATRIX_1:39;
A714: 1 < i + 1 by A698, NAT_1:13;
assume A715: LSeg g,i meets LSeg g,j ; :: thesis:
consider i1', j1', i2', j2' being Element of NAT such that
A716: [i1',j1'] in Indices (Gauge C,n) and
A717: g /. j = (Gauge C,n) * i1',j1' and
A718: [i2',j2'] in Indices (Gauge C,n) and
A719: g /. (j + 1) = (Gauge C,n) * i2',j2' and
A720: ( ( i1' = i2' & j1' + 1 = j2' ) or ( i1' + 1 = i2' & j1' = j2' ) or ( i1' = i2' + 1 & j1' = j2' ) or ( i1' = i2' & j1' = j2' + 1 ) ) by A625, A635, A698, JORDAN8:6;
A721: 1 <= i1' by A716, MATRIX_1:39;
A722: j2' <= width (Gauge C,n) by A718, MATRIX_1:39;
A723: 1 <= i2' by A718, MATRIX_1:39;
A724: i1' <= len (Gauge C,n) by A716, MATRIX_1:39;
A725: 1 <= j2' by A718, MATRIX_1:39;
A726: j1' <= width (Gauge C,n) by A716, MATRIX_1:39;
A727: i2' <= len (Gauge C,n) by A718, MATRIX_1:39;
A728: 1 <= j1' by A716, MATRIX_1:39;
A729: j < len g by A698, NAT_1:12;
A730: LSeg g,j = LSeg (g /. j),(g /. (j + 1)) by A635, A698, TOPREAL1:def 5;
A731: 1 <= i2 by A704, MATRIX_1:39;

now

per cases by A706, A720;

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

then A733: ( j1 = j1' or j1 = j1' + 1 or j1 + 1 = j1' ) by A700, A703, A705, A707, A713, A711, A708, A730, A717, A719, A721, A724, A728, A722, A715, GOBOARD7:24;
i1 = i1' by A700, A703, A705, A707, A713, A711, A708, A730, A717, A719, A721, A724, A728, A722, A715, A732, GOBOARD7:21;
hence contradiction by A630, A633, A638, A636, A639, A698, A729, A703, A705, A717, A719, A732, A733; :: thesis:

end;

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

then ( ( i1 = i1' & j1 = j1' ) or ( i1 = i1' & j1 + 1 = j1' ) or ( i1 = i1' + 1 & j1 = j1' ) or ( i1 = i1' + 1 & j1 + 1 = j1' ) ) by A700, A703, A705, A707, A713, A711, A708, A730, A717, A719, A721, A728, A726, A727, A715, GOBOARD7:23;
hence contradiction by A581, A630, A633, A638, A635, A639, A698, A714, A701, A729, A703, A705, A717, A719, A734; :: thesis:

end;

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

then ( ( i1 = i2' & j1' = j1 ) or ( i1 = i2' & j1 + 1 = j1' ) or ( i1 = i2' + 1 & j1' = j1 ) or ( i1 = i2' + 1 & j1 + 1 = j1' ) ) by A700, A703, A705, A707, A713, A711, A708, A730, A717, A719, A724, A728, A726, A723, A715, GOBOARD7:23;
hence contradiction by A581, A630, A633, A638, A635, A639, A698, A714, A701, A729, A703, A705, A717, A719, A735; :: thesis:

end;

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

then A737: ( j1 = j2' or j1 = j2' + 1 or j1 + 1 = j2' ) by A700, A703, A705, A707, A713, A711, A708, A730, A717, A719, A721, A724, A726, A725, A715, GOBOARD7:24;
i1 = i1' by A700, A703, A705, A707, A713, A711, A708, A730, A717, A719, A721, A724, A726, A725, A715, A736, GOBOARD7:21;
hence contradiction by A581, A615, A633, A638, A635, A698, A714, A701, A729, A703, A705, A717, A719, A736, A737; :: thesis:

end;

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

then ( ( i1' = i1 & j1 = j1' ) or ( i1' = i1 & j1' + 1 = j1 ) or ( i1' = i1 + 1 & j1 = j1' ) or ( i1' = i1 + 1 & j1' + 1 = j1 ) ) by A700, A703, A705, A707, A711, A709, A712, A730, A717, A719, A721, A724, A728, A722, A715, GOBOARD7:23;
hence contradiction by A581, A630, A633, A638, A636, A635, A639, A698, A701, A729, A703, A705, A717, A719, A738; :: thesis:

end;

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

then A740: ( i1 = i1' or i1 = i1' + 1 or i1 + 1 = i1' ) by A700, A703, A705, A707, A711, A709, A712, A730, A717, A719, A721, A728, A726, A727, A715, GOBOARD7:25;
j1 = j1' by A700, A703, A705, A707, A711, A709, A712, A730, A717, A719, A721, A728, A726, A727, A715, A739, GOBOARD7:22;
hence contradiction by A630, A633, A638, A636, A639, A698, A729, A703, A705, A717, A719, A739, A740; :: thesis:

end;

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

then A742: ( i1 = i2' or i1 = i2' + 1 or i1 + 1 = i2' ) by A700, A703, A705, A707, A711, A709, A712, A730, A717, A719, A724, A728, A726, A723, A715, GOBOARD7:25;
j1 = j1' by A700, A703, A705, A707, A711, A709, A712, A730, A717, A719, A724, A728, A726, A723, A715, A741, GOBOARD7:22;
hence contradiction by A581, A630, A638, A635, A639, A698, A714, A701, A729, A703, A705, A717, A719, A741, A742; :: thesis:

end;

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

then ( ( i1' = i1 & j1 = j2' ) or ( i1' = i1 & j2' + 1 = j1 ) or ( i1' = i1 + 1 & j1 = j2' ) or ( i1' = i1 + 1 & j2' + 1 = j1 ) ) by A700, A703, A705, A707, A711, A709, A712, A730, A717, A719, A721, A724, A726, A725, A715, GOBOARD7:23;
hence contradiction by A581, A630, A633, A638, A635, A639, A698, A714, A701, A729, A703, A705, A717, A719, A743; :: thesis:

end;

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

then ( ( i1' = i2 & j1' = j1 ) or ( i1' = i2 & j1' + 1 = j1 ) or ( i1' = i2 + 1 & j1' = j1 ) or ( i1' = i2 + 1 & j1' + 1 = j1 ) ) by A700, A703, A705, A713, A711, A709, A731, A730, A717, A719, A721, A724, A728, A722, A715, GOBOARD7:23;
hence contradiction by A581, A630, A633, A638, A635, A639, A698, A714, A701, A729, A703, A705, A717, A719, A744; :: thesis:

end;

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

then A746: ( i2 = i1' or i2 = i1' + 1 or i2 + 1 = i1' ) by A700, A703, A705, A713, A711, A709, A731, A730, A717, A719, A721, A728, A726, A727, A715, GOBOARD7:25;
j1 = j1' by A700, A703, A705, A713, A711, A709, A731, A730, A717, A719, A721, A728, A726, A727, A715, A745, GOBOARD7:22;
hence contradiction by A581, A615, A633, A638, A635, A698, A714, A701, A729, A703, A705, A717, A719, A745, A746; :: thesis:

end;

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

then A748: ( i2 = i2' or i2 = i2' + 1 or i2 + 1 = i2' ) by A700, A703, A705, A713, A711, A709, A731, A730, A717, A719, A724, A728, A726, A723, A715, GOBOARD7:25;
j1 = j1' by A700, A703, A705, A713, A711, A709, A731, A730, A717, A719, A724, A728, A726, A723, A715, A747, GOBOARD7:22;
hence contradiction by A630, A633, A638, A639, A698, A714, A729, A703, A705, A717, A719, A747, A748; :: thesis:

end;

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

then ( ( i1' = i2 & j2' = j1 ) or ( i1' = i2 & j2' + 1 = j1 ) or ( i1' = i2 + 1 & j2' = j1 ) or ( i1' = i2 + 1 & j2' + 1 = j1 ) ) by A700, A703, A705, A713, A711, A709, A731, A730, A717, A719, A721, A724, A726, A725, A715, GOBOARD7:23;
hence contradiction by A581, A630, A633, A638, A635, A639, A698, A714, A701, A729, A703, A705, A717, A719, A749; :: thesis:

end;

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

then A751: ( j2 = j1' or j2 = j1' + 1 or j2 + 1 = j1' ) by A700, A703, A705, A707, A713, A709, A710, A730, A717, A719, A721, A724, A728, A722, A715, GOBOARD7:24;
i1 = i1' by A700, A703, A705, A707, A713, A709, A710, A730, A717, A719, A721, A724, A728, A722, A715, A750, GOBOARD7:21;
hence contradiction by A581, A615, A633, A638, A635, A698, A714, A701, A729, A703, A705, A717, A719, A750, A751; :: thesis:

end;

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

then ( ( i1 = i1' & j2 = j1' ) or ( i1 = i1' & j2 + 1 = j1' ) or ( i1 = i1' + 1 & j2 = j1' ) or ( i1 = i1' + 1 & j2 + 1 = j1' ) ) by A700, A703, A705, A707, A713, A709, A710, A730, A717, A719, A721, A728, A726, A727, A715, GOBOARD7:23;
hence contradiction by A581, A630, A633, A638, A635, A639, A698, A714, A701, A729, A703, A705, A717, A719, A752; :: thesis:

end;

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

then ( ( i1 = i2' & j2 = j1' ) or ( i1 = i2' & j2 + 1 = j1' ) or ( i1 = i2' + 1 & j2 = j1' ) or ( i1 = i2' + 1 & j2 + 1 = j1' ) ) by A700, A703, A705, A707, A713, A709, A710, A730, A717, A719, A724, A728, A726, A723, A715, GOBOARD7:23;
hence contradiction by A581, A630, A633, A638, A635, A639, A698, A714, A701, A729, A703, A705, A717, A719, A753; :: thesis:

end;

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

then A755: ( j2 = j2' or j2 = j2' + 1 or j2 + 1 = j2' ) by A700, A703, A705, A707, A713, A709, A710, A730, A717, A719, A721, A724, A726, A725, A715, GOBOARD7:24;
i1 = i1' by A700, A703, A705, A707, A713, A709, A710, A730, A717, A719, A721, A724, A726, A725, A715, A754, GOBOARD7:21;
hence contradiction by A630, A633, A638, A639, A698, A714, A729, A703, A705, A717, A719, A754, A755; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then reconsider g = g as non constant standard special_circular_sequence by A569, A614, A579, A625, A627, FINSEQ_6:def 1, JORDAN8:7;
A756: for i being Element of 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 Element of NAT ; :: thesis:
assume A757: ( 1 <= i & i + 1 <= len f ) ; :: thesis:
consider i1, j1, i2, j2 being Element of NAT such that
A758: [i1,j1] in Indices (Gauge C,n) and
A759: f /. i = (Gauge C,n) * i1,j1 and
A760: [i2,j2] in Indices (Gauge C,n) and
A761: f /. (i + 1) = (Gauge C,n) * i2,j2 and
A762: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A571, A757, JORDAN8:6;
A763: i1 <= len (Gauge C,n) by A758, MATRIX_1:39;
A764: j2 <= width (Gauge C,n) by A760, MATRIX_1:39;
A765: j1 <= width (Gauge C,n) by A758, MATRIX_1:39;
A766: ( j1 + 1 > j1 & j2 + 1 > j2 ) by NAT_1:13;
A767: i2 <= len (Gauge C,n) by A760, MATRIX_1:39;
A768: ( i1 + 1 > i1 & i2 + 1 > i2 ) by NAT_1:13;

per cases by A762;

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

then right_cell f,i,(Gauge C,n) = cell (Gauge C,n),i1,j1 by A571, A757, A758, A759, A760, A761, A766, GOBRD13:def 2;
hence right_cell f,i,(Gauge C,n) = Cl (Int (right_cell f,i,(Gauge C,n))) by A763, A765, GOBRD11:35; :: thesis:

end;

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

A770: j1 -' 1 <= width (Gauge C,n) by A765, NAT_D:44;
right_cell f,i,(Gauge C,n) = cell (Gauge C,n),i1,(j1 -' 1) by A571, A757, A758, A759, A760, A761, A768, A769, GOBRD13:def 2;
hence right_cell f,i,(Gauge C,n) = Cl (Int (right_cell f,i,(Gauge C,n))) by A763, A770, 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 A571, A757, A758, A759, A760, A761, A768, GOBRD13:def 2;
hence right_cell f,i,(Gauge C,n) = Cl (Int (right_cell f,i,(Gauge C,n))) by A767, A764, GOBRD11:35; :: thesis:

end;

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

A772: i1 -' 1 <= len (Gauge C,n) by A763, NAT_D:44;
right_cell f,i,(Gauge C,n) = cell (Gauge C,n),(i1 -' 1),j2 by A571, A757, A758, A759, A760, A761, A766, A771, GOBRD13:def 2;
hence right_cell f,i,(Gauge C,n) = Cl (Int (right_cell f,i,(Gauge C,n))) by A764, A772, GOBRD11:35; :: thesis:

end;

now

A773: 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 Element of 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 A774: L~ h c= L~ f ; :: thesis:
let Comp be Subset of (TOP-REAL 2); :: thesis:
assume A775: Comp is_a_component_of (L~ h) ` ; :: thesis:
let n be Element of NAT ; :: thesis:
assume that
A776: ( 1 <= n & n + 1 <= len f ) and
A777: f /. n in Comp and
A778: 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 A571, A776, Th10;
then f /. n in rc by A778, XBOOLE_0:def 5;
then A779: rc meets Comp by A777, XBOOLE_0:3;
A780: rc meets C

proof

right_cell f,n,(Gauge C,n) meets C by A428, A776;
then consider p being set such that
A781: p in right_cell f,n,(Gauge C,n) and
A782: p in C by XBOOLE_0:3;
reconsider p = p as Element of (TOP-REAL 2) by A781;

now

take a = p; :: thesis:

now

assume p in L~ h ; :: thesis:
then consider j being Element of NAT such that
A783: ( 1 <= j & j + 1 <= len f ) and
A784: p in LSeg f,j by A774, SPPOL_2:13;
p in (left_cell f,j,(Gauge C,n)) /\ (right_cell f,j,(Gauge C,n)) by A428, A783, A784, GOBRD13:30;
then A785: p in left_cell f,j,(Gauge C,n) by XBOOLE_0:def 4;
left_cell f,j,(Gauge C,n) misses C by A428, A783;
hence contradiction by A782, A785, XBOOLE_0:3; :: thesis:

end;

hence a in rc by A781, XBOOLE_0:def 5; :: thesis:
thus a in C by A782; :: thesis:

end;

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

end;

Int (right_cell f,n,(Gauge C,n)) misses L~ f by A571, A776, Th17;
then Int (right_cell f,n,(Gauge C,n)) misses L~ h by A774, XBOOLE_1:63;
then A786: Int (right_cell f,n,(Gauge C,n)) c= (L~ h) ` by SUBSET_1:43;
A787: rc = (right_cell f,n,(Gauge C,n)) /\ ((L~ h) ` ) by SUBSET_1:32;
then A788: rc c= (L~ h) ` by XBOOLE_1:17;
rc c= right_cell f,n,(Gauge C,n) by XBOOLE_1:36;
then A789: ( Int (right_cell f,n,(Gauge C,n)) c= right_cell f,n,(Gauge C,n) & rc c= Cl (Int (right_cell f,n,(Gauge C,n))) ) by A571, A776, Th13, TOPS_1:44;
Int (right_cell f,n,(Gauge C,n)) is connected by A571, A776, Th12;
then rc is connected by A787, A786, A789, CONNSP_1:19, XBOOLE_1:19;
then rc c= Comp by A775, A779, A788, GOBOARD9:6;
hence C meets Comp by A780, XBOOLE_1:63; :: thesis:

end;

L~ g is closed by SPPOL_1:49;
then (L~ g) ` is open by TOPS_1:29;
then A790: (L~ g) ` = Int ((L~ g) ` ) by TOPS_1:55;
A791: L~ g c= L~ f by JORDAN3:75;
A792: for j, k being Element of NAT st 1 <= j & j <= k holds
(F . k) /. j = (F . j) /. j

proof

let j, k be Element of NAT ; :: thesis:
assume that
A793: 1 <= j and
A794: j <= k ; :: thesis:
j <= len (F . k) by A192, A794;
then len ((F . k) | j) = j by FINSEQ_1:80;
then A795: j in dom ((F . k) | j) by A793, FINSEQ_3:27;
(F . k) | j = F . j by A490, A794;
hence (F . k) /. j = (F . j) /. j by A795, FINSEQ_4:85; :: thesis:

end;

assume m <> 1 ; :: thesis:
then A796: 1 < m by A570, XXREAL_0:1;
A797: for n being Element of NAT st 1 <= n & n <= m -' 1 holds
not f /. n in L~ g

proof

A798: 2 <= len (Gauge C,n) by A231, NAT_1:12;
let n be Element of NAT ; :: thesis:
assume that
A799: 1 <= n and
A800: n <= m -' 1 ; :: thesis:
set p = f /. n;
A801: n <= len f by A577, A800, XXREAL_0:2;
then A802: f /. n in Values (Gauge C,n) by A428, A799, Th8;
assume f /. n in L~ g ; :: thesis:
then consider j being Element of NAT such that
A803: (m -' 1) + 1 <= j and
A804: j + 1 <= len f and
A805: f /. n in LSeg f,j by A577, Th9;
A806: j < k by A580, A804, NAT_1:13;
A807: n < (m -' 1) + 1 by A800, NAT_1:13;
then A808: n < j by A803, XXREAL_0:2;
A809: (m -' 1) + 1 = m by A570, XREAL_1:237;
then A810: 1 < j by A796, A803, XXREAL_0:2;

per cases by A2, A428, A804, A805, A810, A798, A802, Th25;

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

A812: n <> len (F . j) by A192, A803, A807;
n <= len (F . j) by A192, A808;
then A813: n in dom (F . j) by A799, FINSEQ_3:27;
(F . j) /. n = (F . n) /. n by A792, A799, A808
.= f /. n by A580, A792, A799, A801
.= (F . j) /. j by A792, A810, A806, A811
.= (F . j) /. (len (F . j)) by A192 ;
hence contradiction by A566, A810, A806, A813, A812; :: thesis:

end;

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

now

per cases by A580, A804, XXREAL_0:1;

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

A816: n <> len (F . m) by A192, A807, A809;
n <= len (F . m) by A192, A807, A809;
then A817: n in dom (F . m) by A799, FINSEQ_3:27;
(F . m) /. n = (F . n) /. n by A792, A799, A807, A809
.= (F . k) /. k by A580, A792, A799, A801, A814, A815
.= (F . m) /. m by A569, A580, A570, A572, A792
.= (F . m) /. (len (F . m)) by A192 ;
hence contradiction by A566, A580, A570, A573, A817, A816; :: thesis:

end;

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

set l = j + 1;
A819: 1 <= j + 1 by NAT_1:11;
A820: ( n < n + 1 & n + 1 < j + 1 ) by A808, XREAL_1:8, XREAL_1:31;
then A821: n <> len (F . (j + 1)) by A192;
A822: n < j + 1 by A820, XXREAL_0:2;
then n <= len (F . (j + 1)) by A192;
then A823: n in dom (F . (j + 1)) by A799, FINSEQ_3:27;
(F . (j + 1)) /. n = (F . n) /. n by A792, A799, A822
.= f /. n by A580, A792, A799, A801
.= (F . (j + 1)) /. (j + 1) by A792, A814, A818, A819
.= (F . (j + 1)) /. (len (F . (j + 1))) by A192 ;
hence contradiction by A566, A818, A823, A821, NAT_1:11; :: thesis:

end;

hence contradiction ; :: thesis:

end;

C meets RightComp (Rev g)

proof

1 <= len g by A624, XREAL_1:147;
then A824: ((len g) -' 1) + 2 = (len g) + 1 by Lm1;
A825: 1 - 1 < m - 1 by A796, XREAL_1:11;
A826: (m -' 1) + 2 = m + 1 by A570, 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;
A827: (1 + 1) - 1 <= (len g) - 1 by A623, XREAL_1:11;
(1 + 1) -' 1 <= (len g) -' 1 by A623, NAT_D:42;
then A828: 1 <= (len g) -' 1 by NAT_D:34;
then (m -' 1) + 1 <= (m -' 1) + ((len g) -' 1) by XREAL_1:8;
then m -' 1 < (m -' 1) + ((len g) -' 1) by NAT_1:13;
then A829: m -' 1 <> len (F . ((m -' 1) + ((len g) -' 1))) by A192;
A830: 1 + 1 <= len (Rev g) by A623, FINSEQ_5:def 3;
then (1 + 1) -' 1 <= (len (Rev g)) -' 1 by NAT_D:42;
then A831: 1 <= (len (Rev g)) -' 1 by NAT_D:34;
1 < len (Rev g) by A830, NAT_1:13;
then A832: ((len (Rev g)) -' 1) + 1 = len (Rev g) by XREAL_1:237;
A833: Rev g is_sequence_on Gauge C,n by A625, Th7;
then consider p1, p2, q1, q2 being Element of NAT such that
A834: [p1,p2] in Indices (Gauge C,n) and
A835: (Rev g) /. 1 = (Gauge C,n) * p1,p2 and
A836: [q1,q2] in Indices (Gauge C,n) and
A837: (Rev g) /. 2 = (Gauge C,n) * q1,q2 and
A838: ( ( p1 = q1 & p2 + 1 = q2 ) or ( p1 + 1 = q1 & p2 = q2 ) or ( p1 = q1 + 1 & p2 = q2 ) or ( p1 = q1 & p2 = q2 + 1 ) ) by A830, JORDAN8:6;
A839: 1 <= p1 by A834, MATRIX_1:39;
A840: p2 <= width (Gauge C,n) by A834, MATRIX_1:39;
A841: p1 <= len (Gauge C,n) by A834, MATRIX_1:39;
A842: 1 <= p2 by A834, MATRIX_1:39;
A843: (Rev g) /. 1 = f /. m by A569, A579, FINSEQ_5:68;
(len g) -' 1 <= len g by NAT_D:44;
then A844: (len g) -' 1 in dom g by A828, FINSEQ_3:27;
then A845: (Rev g) /. 2 = g /. ((len g) -' 1) by A824, FINSEQ_5:69
.= f /. ((m -' 1) + ((len g) -' 1)) by A844, FINSEQ_5:30 ;
(m -' 1) + ((len g) -' 1) = (m + ((len g) -' 1)) -' 1 by A570, NAT_D:38
.= (((len g) -' 1) + m) - 1 by A828, NAT_D:37
.= (((len g) - 1) + m) - 1 by A827, XREAL_0:def 2
.= (((k - (m - 1)) - 1) + m) - 1 by A580, A578, A825, XREAL_0:def 2
.= k - 1 ;
then A846: k = ((m -' 1) + ((len g) -' 1)) + 1 ;
then A847: (m -' 1) + ((len g) -' 1) < k by XREAL_1:31;
(len g) -' 1 <= (m -' 1) + ((len g) -' 1) by NAT_1:11;
then A848: 1 <= (m -' 1) + ((len g) -' 1) by A828, XXREAL_0:2;
then A849: right_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) meets C by A428, A580, A846;
A850: (m -' 1) + 1 = m by A570, XREAL_1:237;
then A851: 1 <= m -' 1 by A796, NAT_1:13;
then A852: right_cell f,(m -' 1),(Gauge C,n) meets C by A428, A572, A850;
m -' 1 <= (m -' 1) + ((len g) -' 1) by NAT_1:11;
then m -' 1 <= len (F . ((m -' 1) + ((len g) -' 1))) by A192;
then A853: m -' 1 in dom (F . ((m -' 1) + ((len g) -' 1))) by A851, FINSEQ_3:27;
not f /. (m -' 1) in L~ g by A797, A851;
then A854: not f /. (m -' 1) in L~ (Rev g) by SPPOL_2:22;

per cases by A838;

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

consider a1, a2, p'1, p'2 being Element of NAT such that
A856: [a1,a2] in Indices (Gauge C,n) and
A857: f /. (m -' 1) = (Gauge C,n) * a1,a2 and
A858: ( [p'1,p'2] in Indices (Gauge C,n) & (Rev g) /. 1 = (Gauge C,n) * p'1,p'2 ) and
A859: ( ( a1 = p'1 & a2 + 1 = p'2 ) or ( a1 + 1 = p'1 & a2 = p'2 ) or ( a1 = p'1 + 1 & a2 = p'2 ) or ( a1 = p'1 & a2 = p'2 + 1 ) ) by A571, A572, A843, A850, A851, JORDAN8:6;
A860: 1 <= a2 by A856, MATRIX_1:39;
thus C meets RightComp (Rev g) :: thesis:

proof

per cases by A859;

suppose A861: ( a1 = p'1 & a2 + 1 = p'2 ) ; :: thesis:

A862: ( (m -' 1) + 1 <= len (F . m) & f /. ((m -' 1) + 1) = (F . m) /. m ) by A192, A580, A570, A572, A792, A850;
A863: (F . k) | (m + 1) = F . (m + 1) by A490, A580, A576;
A864: a1 = p1 by A834, A835, A858, A861, GOBOARD1:21;
A865: m -' 1 <= m by A850, NAT_1:11;
A866: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A580, A577, A792, A851
.= (F . m) /. (m -' 1) by A792, A851, A865 ;
A867: 2 in dom g by A623, FINSEQ_3:27;
A868: a2 + 1 = p2 by A834, A835, A858, A861, GOBOARD1:21;
then A869: 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 A428, A569, A580, A843, A846, A848, A845, A834, A835, A836, A837, A855, GOBRD13:29
.= front_left_cell (F . m),(m -' 1),(Gauge C,n) by A428, A843, A850, A851, A834, A835, A856, A857, A864, A868, A866, A862, GOBRD13:35 ;
then F . (m + 1) turns_left m -' 1, Gauge C,n by A458, A796, A849;
then A870: ( a2 + 1 > a2 & f turns_left m -' 1, Gauge C,n ) by A851, A826, A863, GOBRD13:45, NAT_1:13;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A824, FINSEQ_5:def 3;
then A871: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A867, FINSEQ_5:69
.= f /. (m + 1) by A826, A867, FINSEQ_5:30 ;
A872: (Rev g) /. 1 = g /. 1 by A569, A614, A579, FINSEQ_5:68
.= (Rev g) /. (len g) by FINSEQ_5:68
.= (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));
A873: RightComp (Rev g) is_a_component_of (L~ (Rev g)) ` by GOBOARD9:def 2;
A874: (p1 -' 1) + 1 = p1 by A839, XREAL_1:237;
A875: p2 + 1 > a2 + 1 by A868, NAT_1:13;
then A876: [(p1 -' 1),p2] in Indices (Gauge C,n) by A843, A850, A834, A835, A856, A857, A870, GOBRD13:def 7;
then A877: 1 <= p1 -' 1 by MATRIX_1:39;
f /. (m + 1) = (Gauge C,n) * (p1 -' 1),p2 by A843, A850, A826, A834, A835, A856, A857, A875, A870, GOBRD13:def 7;
then right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) = cell (Gauge C,n),(p1 -' 1),a2 by A833, A831, A832, A834, A835, A876, A869, A874, A871, A872, GOBRD13:25;
then f /. (m -' 1) in right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) by A841, A840, A857, A860, A864, A868, A877, A874, Th22;
then A878: f /. (m -' 1) in (right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g)) by A854, 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 A791, A833, A831, A832, Th29, SPPOL_2:22;
hence C meets RightComp (Rev g) by A572, A773, A850, A851, A854, A878, A873; :: thesis:

end;

suppose A879: ( a1 + 1 = p'1 & a2 = p'2 ) ; :: thesis:

then a1 + 1 = p1 by A834, A835, A858, GOBOARD1:21;
then A880: q1 -' 1 = a1 by A855, NAT_D:34;
a2 = p2 by A834, A835, A858, A879, GOBOARD1:21;
then right_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) = cell (Gauge C,n),a1,a2 by A428, A569, A580, A843, A846, A848, A845, A834, A835, A836, A837, A855, A880, GOBRD13:29
.= left_cell f,(m -' 1),(Gauge C,n) by A428, A572, A843, A850, A851, A856, A857, A858, A879, GOBRD13:24 ;
hence C meets RightComp (Rev g) by A428, A572, A850, A851, A849; :: thesis:

end;

suppose ( a1 = p'1 + 1 & a2 = p'2 ) ; :: thesis:

then ( a1 = p1 + 1 & a2 = p2 ) by A834, A835, A858, GOBOARD1:21;
then right_cell f,(m -' 1),(Gauge C,n) = cell (Gauge C,n),p1,p2 by A428, A572, A843, A850, A851, A834, A835, A856, A857, GOBRD13:27
.= left_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) by A428, A569, A580, A843, A846, A848, A845, A834, A835, A836, A837, A855, GOBRD13:28 ;
hence C meets RightComp (Rev g) by A428, A580, A846, A848, A852; :: thesis:

end;

suppose ( a1 = p'1 & a2 = p'2 + 1 ) ; :: thesis:

then A881: ( a1 = q1 & a2 = q2 ) by A834, A835, A855, A858, GOBOARD1:21;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A792, A851, NAT_1:11
.= (Rev g) /. 2 by A580, A577, A792, A851, A837, A857, A881
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A792, A847, A848, A845
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A192 ;
hence C meets RightComp (Rev g) by A566, A847, A848, A853, A829; :: thesis:

end;

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

consider a1, a2, p'1, p'2 being Element of NAT such that
A883: [a1,a2] in Indices (Gauge C,n) and
A884: f /. (m -' 1) = (Gauge C,n) * a1,a2 and
A885: ( [p'1,p'2] in Indices (Gauge C,n) & (Rev g) /. 1 = (Gauge C,n) * p'1,p'2 ) and
A886: ( ( a1 = p'1 & a2 + 1 = p'2 ) or ( a1 + 1 = p'1 & a2 = p'2 ) or ( a1 = p'1 + 1 & a2 = p'2 ) or ( a1 = p'1 & a2 = p'2 + 1 ) ) by A571, A572, A843, A850, A851, JORDAN8:6;
A887: 1 <= a1 by A883, MATRIX_1:39;
thus C meets RightComp (Rev g) :: thesis:

proof

per cases by A886;

suppose A888: ( a1 = p'1 & a2 + 1 = p'2 ) ; :: thesis:

then a2 + 1 = p2 by A834, A835, A885, GOBOARD1:21;
then A889: q2 -' 1 = a2 by A882, NAT_D:34;
A890: a1 = p1 by A834, A835, A885, A888, GOBOARD1:21;
right_cell f,(m -' 1),(Gauge C,n) = cell (Gauge C,n),a1,a2 by A428, A572, A843, A850, A851, A883, A884, A885, A888, GOBRD13:23
.= left_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) by A428, A569, A580, A843, A846, A848, A845, A834, A835, A836, A837, A882, A890, A889, GOBRD13:26 ;
hence C meets RightComp (Rev g) by A428, A580, A846, A848, A852; :: thesis:

end;

suppose A891: ( a1 + 1 = p'1 & a2 = p'2 ) ; :: thesis:

A892: m -' 1 <= m by A850, NAT_1:11;
A893: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A580, A577, A792, A851
.= (F . m) /. (m -' 1) by A792, A851, A892 ;
A894: 2 in dom g by A623, FINSEQ_3:27;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A824, FINSEQ_5:def 3;
then A895: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A894, FINSEQ_5:69
.= f /. (m + 1) by A826, A894, FINSEQ_5:30 ;
A896: (Rev g) /. 1 = g /. 1 by A569, A614, A579, FINSEQ_5:68
.= (Rev g) /. (len g) by FINSEQ_5:68
.= (Rev g) /. (len (Rev g)) by FINSEQ_5:def 3 ;
A897: a2 = p2 by A834, A835, A885, A891, GOBOARD1:21;
A898: ( (m -' 1) + 1 <= len (F . m) & f /. ((m -' 1) + 1) = (F . m) /. m ) by A192, A580, A570, A572, A792, A850;
A899: (F . k) | (m + 1) = F . (m + 1) by A490, A580, A576;
set rc = (right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g));
A900: ( a1 < a1 + 1 & p1 < p1 + 1 ) by XREAL_1:31;
A901: a1 + 1 = p1 by A834, A835, A885, A891, GOBOARD1:21;
then A902: 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 A428, A569, A580, A843, A846, A848, A845, A834, A835, A836, A837, A882, GOBRD13:27
.= front_left_cell (F . m),(m -' 1),(Gauge C,n) by A428, A843, A850, A851, A834, A835, A883, A884, A901, A897, A893, A898, GOBRD13:37 ;
then F . (m + 1) turns_left m -' 1, Gauge C,n by A458, A796, A849;
then A903: f turns_left m -' 1, Gauge C,n by A851, A826, A899, GOBRD13:45;
then A904: [p1,(p2 + 1)] in Indices (Gauge C,n) by A843, A850, A834, A835, A883, A884, A901, A900, GOBRD13:def 7;
then A905: p2 + 1 <= width (Gauge C,n) by MATRIX_1:39;
f /. (m + 1) = (Gauge C,n) * p1,(p2 + 1) by A843, A850, A826, A834, A835, A883, A884, A901, A900, A903, GOBRD13:def 7;
then right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) = cell (Gauge C,n),(p1 -' 1),a2 by A833, A831, A832, A834, A835, A897, A904, A895, A896, GOBRD13:29;
then f /. (m -' 1) in right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) by A841, A842, A884, A887, A901, A897, A905, A902, Th22;
then A906: f /. (m -' 1) in (right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g)) by A854, XBOOLE_0:def 5;
A907: 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 A791, A833, A831, A832, Th29, SPPOL_2:22;
hence C meets RightComp (Rev g) by A572, A773, A850, A851, A854, A906, A907; :: thesis:

end;

suppose ( a1 = p'1 + 1 & a2 = p'2 ) ; :: thesis:

then A908: ( a1 = q1 & a2 = q2 ) by A834, A835, A882, A885, GOBOARD1:21;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A792, A851, NAT_1:11
.= (Rev g) /. 2 by A580, A577, A792, A851, A837, A884, A908
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A792, A847, A848, A845
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A192 ;
hence C meets RightComp (Rev g) by A566, A847, A848, A853, A829; :: thesis:

end;

suppose ( a1 = p'1 & a2 = p'2 + 1 ) ; :: thesis:

then A909: ( a1 = p1 & a2 = p2 + 1 ) by A834, A835, A885, GOBOARD1:21;
right_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) = cell (Gauge C,n),p1,p2 by A428, A569, A580, A843, A846, A848, A845, A834, A835, A836, A837, A882, GOBRD13:27
.= left_cell f,(m -' 1),(Gauge C,n) by A428, A572, A843, A850, A851, A834, A835, A883, A884, A909, GOBRD13:28 ;
hence C meets RightComp (Rev g) by A428, A572, A850, A851, A849; :: thesis:

end;

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

consider a1, a2, p'1, p'2 being Element of NAT such that
A911: [a1,a2] in Indices (Gauge C,n) and
A912: f /. (m -' 1) = (Gauge C,n) * a1,a2 and
A913: ( [p'1,p'2] in Indices (Gauge C,n) & (Rev g) /. 1 = (Gauge C,n) * p'1,p'2 ) and
A914: ( ( a1 = p'1 & a2 + 1 = p'2 ) or ( a1 + 1 = p'1 & a2 = p'2 ) or ( a1 = p'1 + 1 & a2 = p'2 ) or ( a1 = p'1 & a2 = p'2 + 1 ) ) by A571, A572, A843, A850, A851, JORDAN8:6;
A915: a1 <= len (Gauge C,n) by A911, MATRIX_1:39;
thus C meets RightComp (Rev g) :: thesis:

proof

per cases by A914;

suppose A916: ( a1 = p'1 & a2 + 1 = p'2 ) ; :: thesis:

then a2 + 1 = p2 by A834, A835, A913, GOBOARD1:21;
then A917: q2 -' 1 = a2 by A910, NAT_D:34;
a1 = p1 by A834, A835, A913, A916, GOBOARD1:21;
then A918: q1 = a1 -' 1 by A910, NAT_D:34;
right_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) = cell (Gauge C,n),q1,(q2 -' 1) by A428, A569, A580, A843, A846, A848, A845, A834, A835, A836, A837, A910, GOBRD13:25
.= left_cell f,(m -' 1),(Gauge C,n) by A428, A572, A843, A850, A851, A911, A912, A913, A916, A918, A917, GOBRD13:22 ;
hence C meets RightComp (Rev g) by A428, A572, A850, A851, A849; :: thesis:

end;

suppose ( a1 + 1 = p'1 & a2 = p'2 ) ; :: thesis:

then A919: ( a1 + 1 = p1 & a2 = p2 ) by A834, A835, A913, GOBOARD1:21;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A792, A851, NAT_1:11
.= (Rev g) /. 2 by A580, A577, A792, A851, A837, A910, A912, A919
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A792, A847, A848, A845
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A192 ;
hence C meets RightComp (Rev g) by A566, A847, A848, A853, A829; :: thesis:

end;

suppose A920: ( a1 = p'1 + 1 & a2 = p'2 ) ; :: thesis:

A921: (Rev g) /. 1 = g /. 1 by A569, A614, A579, FINSEQ_5:68
.= (Rev g) /. (len g) by FINSEQ_5:68
.= (Rev g) /. (len (Rev g)) by FINSEQ_5:def 3 ;
A922: a1 = p1 + 1 by A834, A835, A913, A920, GOBOARD1:21;
p1 + 1 > p1 by XREAL_1:31;
then A923: a1 + 1 > p1 by A922, NAT_1:13;
A924: m -' 1 <= m by A850, NAT_1:11;
A925: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A580, A577, A792, A851
.= (F . m) /. (m -' 1) by A792, A851, A924 ;
A926: 2 in dom g by A623, FINSEQ_3:27;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A824, FINSEQ_5:def 3;
then A927: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A926, FINSEQ_5:69
.= f /. (m + 1) by A826, A926, FINSEQ_5:30 ;
A928: (F . k) | (m + 1) = F . (m + 1) by A490, A580, A576;
set rc = (right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g));
A929: RightComp (Rev g) is_a_component_of (L~ (Rev g)) ` by GOBOARD9:def 2;
A930: (p2 -' 1) + 1 = p2 by A842, XREAL_1:237;
A931: f /. ((m -' 1) + 1) = (F . m) /. m by A580, A570, A572, A792, A850;
A932: ( p1 -' 1 = q1 & (m -' 1) + 1 <= len (F . m) ) by A192, A850, A910, NAT_D:34;
A933: a2 = p2 by A834, A835, A913, A920, GOBOARD1:21;
right_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) = cell (Gauge C,n),q1,(q2 -' 1) by A428, A569, A580, A843, A846, A848, A845, A834, A835, A836, A837, A910, GOBRD13:25
.= front_left_cell (F . m),(m -' 1),(Gauge C,n) by A428, A843, A850, A851, A834, A835, A910, A911, A912, A922, A933, A932, A925, A931, GOBRD13:39 ;
then F . (m + 1) turns_left m -' 1, Gauge C,n by A458, A796, A849;
then A934: f turns_left m -' 1, Gauge C,n by A851, A826, A928, GOBRD13:45;
A935: a2 + 1 > p2 by A933, NAT_1:13;
then A936: [p1,(p2 -' 1)] in Indices (Gauge C,n) by A843, A850, A834, A835, A911, A912, A933, A923, A934, GOBRD13:def 7;
then A937: 1 <= p2 -' 1 by MATRIX_1:39;
f /. (m + 1) = (Gauge C,n) * p1,(p2 -' 1) by A843, A850, A826, A834, A835, A911, A912, A933, A935, A923, A934, GOBRD13:def 7;
then right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) = cell (Gauge C,n),p1,(p2 -' 1) by A833, A831, A832, A834, A835, A936, A930, A927, A921, GOBRD13:23;
then f /. (m -' 1) in right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) by A839, A840, A912, A915, A922, A933, A937, A930, Th22;
then A938: f /. (m -' 1) in (right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g)) by A854, 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 A791, A833, A831, A832, Th29, SPPOL_2:22;
hence C meets RightComp (Rev g) by A572, A773, A850, A851, A854, A938, A929; :: thesis:

end;

suppose A939: ( a1 = p'1 & a2 = p'2 + 1 ) ; :: thesis:

then a1 = p1 by A834, A835, A913, GOBOARD1:21;
then A940: q1 = a1 -' 1 by A910, NAT_D:34;
a2 = p2 + 1 by A834, A835, A913, A939, GOBOARD1:21;
then right_cell f,(m -' 1),(Gauge C,n) = cell (Gauge C,n),q1,q2 by A428, A572, A843, A850, A851, A910, A911, A912, A913, A939, A940, GOBRD13:29
.= left_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) by A428, A569, A580, A843, A846, A848, A845, A834, A835, A836, A837, A910, GOBRD13:24 ;
hence C meets RightComp (Rev g) by A428, A580, A846, A848, A852; :: thesis:

end;

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

consider a1, a2, p'1, p'2 being Element of NAT such that
A942: [a1,a2] in Indices (Gauge C,n) and
A943: f /. (m -' 1) = (Gauge C,n) * a1,a2 and
A944: ( [p'1,p'2] in Indices (Gauge C,n) & (Rev g) /. 1 = (Gauge C,n) * p'1,p'2 ) and
A945: ( ( a1 = p'1 & a2 + 1 = p'2 ) or ( a1 + 1 = p'1 & a2 = p'2 ) or ( a1 = p'1 + 1 & a2 = p'2 ) or ( a1 = p'1 & a2 = p'2 + 1 ) ) by A571, A572, A843, A850, A851, JORDAN8:6;
A946: a2 <= width (Gauge C,n) by A942, MATRIX_1:39;
thus C meets RightComp (Rev g) :: thesis:

proof

per cases by A945;

suppose ( a1 = p'1 & a2 + 1 = p'2 ) ; :: thesis:

then A947: ( a1 = p1 & a2 + 1 = p2 ) by A834, A835, A944, GOBOARD1:21;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A792, A851, NAT_1:11
.= (Rev g) /. 2 by A580, A577, A792, A851, A837, A941, A943, A947
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A792, A847, A848, A845
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A192 ;
hence C meets RightComp (Rev g) by A566, A847, A848, A853, A829; :: thesis:

end;

suppose A948: ( a1 + 1 = p'1 & a2 = p'2 ) ; :: thesis:

then a2 = p2 by A834, A835, A944, GOBOARD1:21;
then A949: a2 -' 1 = q2 by A941, NAT_D:34;
a1 + 1 = p1 by A834, A835, A944, A948, GOBOARD1:21;
then A950: a1 = q1 -' 1 by A941, NAT_D:34;
right_cell f,(m -' 1),(Gauge C,n) = cell (Gauge C,n),a1,(a2 -' 1) by A428, A572, A843, A850, A851, A942, A943, A944, A948, GOBRD13:25
.= left_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) by A428, A569, A580, A843, A846, A848, A845, A834, A835, A836, A837, A941, A950, A949, GOBRD13:22 ;
hence C meets RightComp (Rev g) by A428, A580, A846, A848, A852; :: thesis:

end;

suppose A951: ( a1 = p'1 + 1 & a2 = p'2 ) ; :: thesis:

then a2 = p2 by A834, A835, A944, GOBOARD1:21;
then A952: a2 -' 1 = q2 by A941, NAT_D:34;
A953: a1 = p1 + 1 by A834, A835, A944, A951, GOBOARD1:21;
right_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) = cell (Gauge C,n),q1,q2 by A428, A569, A580, A843, A846, A848, A845, A834, A835, A836, A837, A941, GOBRD13:23
.= left_cell f,(m -' 1),(Gauge C,n) by A428, A572, A843, A850, A851, A941, A942, A943, A944, A951, A953, A952, GOBRD13:26 ;
hence C meets RightComp (Rev g) by A428, A572, A850, A851, A849; :: thesis:

end;

suppose A954: ( a1 = p'1 & a2 = p'2 + 1 ) ; :: thesis:

set rc = (right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g));
A955: RightComp (Rev g) is_a_component_of (L~ (Rev g)) ` by GOBOARD9:def 2;
A956: 2 in dom g by A623, FINSEQ_3:27;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A824, FINSEQ_5:def 3;
then A957: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A956, FINSEQ_5:69
.= f /. (m + 1) by A826, A956, FINSEQ_5:30 ;
A958: (Rev g) /. 1 = g /. 1 by A569, A614, A579, FINSEQ_5:68
.= (Rev g) /. (len g) by FINSEQ_5:68
.= (Rev g) /. (len (Rev g)) by FINSEQ_5:def 3 ;
A959: a1 = p1 by A834, A835, A944, A954, GOBOARD1:21;
A960: m -' 1 <= m by A850, NAT_1:11;
A961: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A580, A577, A792, A851
.= (F . m) /. (m -' 1) by A792, A851, A960 ;
A962: ( p2 -' 1 = q2 & (m -' 1) + 1 <= len (F . m) ) by A192, A850, A941, NAT_D:34;
A963: f /. ((m -' 1) + 1) = (F . m) /. m by A580, A570, A572, A792, A850;
A964: (F . k) | (m + 1) = F . (m + 1) by A490, A580, A576;
A965: a2 = p2 + 1 by A834, A835, A944, A954, GOBOARD1:21;
right_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) = cell (Gauge C,n),q1,q2 by A428, A569, A580, A843, A846, A848, A845, A834, A835, A836, A837, A941, GOBRD13:23
.= front_left_cell (F . m),(m -' 1),(Gauge C,n) by A428, A843, A850, A851, A834, A835, A941, A942, A943, A959, A965, A962, A961, A963, GOBRD13:41 ;
then F . (m + 1) turns_left m -' 1, Gauge C,n by A458, A796, A849;
then A966: ( p2 + 1 > p2 & f turns_left m -' 1, Gauge C,n ) by A851, A826, A964, GOBRD13:45, NAT_1:13;
A967: a2 + 1 > p2 + 1 by A965, NAT_1:13;
then A968: [(p1 + 1),p2] in Indices (Gauge C,n) by A843, A850, A834, A835, A942, A943, A966, GOBRD13:def 7;
then A969: p1 + 1 <= len (Gauge C,n) by MATRIX_1:39;
f /. (m + 1) = (Gauge C,n) * (p1 + 1),p2 by A843, A850, A826, A834, A835, A942, A943, A967, A966, GOBRD13:def 7;
then right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) = cell (Gauge C,n),p1,p2 by A833, A831, A832, A834, A835, A968, A957, A958, GOBRD13:27;
then f /. (m -' 1) in right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) by A839, A842, A943, A946, A959, A965, A969, Th22;
then A970: f /. (m -' 1) in (right_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g)) by A854, 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 A791, A833, A831, A832, Th29, SPPOL_2:22;
hence C meets RightComp (Rev g) by A572, A773, A850, A851, A854, A970, A955; :: thesis:

end;

then A971: ( LeftComp g is_a_component_of (L~ g) ` & C meets LeftComp g ) by GOBOARD9:27, GOBOARD9:def 1;
reconsider Lg' = (L~ g) ` as Subset of (TOP-REAL 2) ;
A972: RightComp g is_a_component_of (L~ g) ` by GOBOARD9:def 2;
A973: C c= Lg'

proof

let c be set ; :: according to TARSKI:def 3 :: thesis:
assume that
A974: c in C and
A975: not c in Lg' ; :: thesis:
reconsider c = c as Point of (TOP-REAL 2) by A974;
consider i being Element of NAT such that
A976: 1 <= i and
A977: i + 1 <= len g and
A978: c in LSeg (g /. i),(g /. (i + 1)) by A975, SPPOL_2:14, SUBSET_1:50;
A979: 1 <= i + (m -' 1) by A976, NAT_1:12;
i + 1 in dom g by A976, A977, GOBOARD2:3;
then A980: g /. (i + 1) = f /. ((i + 1) + (m -' 1)) by FINSEQ_5:30;
(i + 1) + (m -' 1) = (i + (m -' 1)) + 1 ;
then A981: (i + (m -' 1)) + 1 <= (len g) + (m -' 1) by A977, XREAL_1:8;
i in dom g by A976, A977, GOBOARD2:3;
then g /. i = f /. (i + (m -' 1)) by FINSEQ_5:30;
then c in LSeg f,(i + (m -' 1)) by A578, A978, A980, A979, A981, TOPREAL1:def 5;
then c in (left_cell f,(i + (m -' 1)),(Gauge C,n)) /\ (right_cell f,(i + (m -' 1)),(Gauge C,n)) by A428, A578, A979, A981, GOBRD13:30;
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 A974, XBOOLE_0:3;
hence contradiction by A428, A578, A979, A981; :: thesis:

end;

A982: 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 A428, A570, A576;
then consider p being set such that
A983: p in right_cell f,m,(Gauge C,n) and
A984: p in C by XBOOLE_0:3;
reconsider p = p as Element of (TOP-REAL 2) by A983;

now

reconsider u = p as Element of (Euclid 2) by TOPREAL3:13;
take a = p; :: thesis:
thus a in C by A984; :: thesis:
consider r being real number such that
A985: r > 0 and
A986: Ball u,r c= (L~ g) ` by A973, A790, A984, GOBOARD6:8;
reconsider r = r as Real by XREAL_0:def 1;
A987: p in Ball u,r by A985, GOBOARD6:4;
reconsider B = Ball u,r as non empty Subset of (TOP-REAL 2) by A982, A985, GOBOARD6:4, TOPMETR:16;
A988: p in B by A985, GOBOARD6:4;
( right_cell f,m,(Gauge C,n) = Cl (Int (right_cell f,m,(Gauge C,n))) & B is open ) by A570, A576, A756, GOBOARD6:6;
then A989: Int (right_cell f,m,(Gauge C,n)) meets B by A983, A987, TOPS_1:39;
( Int (right_cell g,1,(Gauge C,n)) c= Int (right_cell g,1) & Int (right_cell g,1) c= RightComp g ) by A625, A624, GOBOARD9:28, GOBRD13:34, TOPS_1:48;
then Int (right_cell g,1,(Gauge C,n)) c= RightComp g by XBOOLE_1:1;
then Int (right_cell f,((m -' 1) + 1),(Gauge C,n)) c= RightComp g by A571, A577, A624, GOBRD13:33;
then ( B is connected & Int (right_cell f,m,(Gauge C,n)) c= RightComp g ) by A570, SPRECT_3:17, XREAL_1:237;
then B c= RightComp g by A972, A986, A989, GOBOARD9:6;
hence a in RightComp g by A988; :: thesis:

end;

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

end;

hence contradiction by A1, A972, A973, A971, Th3, SPRECT_4:7; :: thesis:

end;

then g = f /^ 0 by XREAL_1:234
.= f by FINSEQ_5:31 ;
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:69;
then A990: f /. 2 in L~ f by A574, SPPOL_2:15;
(NW-corner (L~ f)) `1 = W-bound (L~ f) by EUCLID:56;
then A991: (NW-corner (L~ f)) `1 <= (f /. 2) `1 by A990, PSCOMP_1:71;
len (Gauge C,n) >= 3 by A231, NAT_1:12;
then A992: 1 < len (Gauge C,n) by XXREAL_0:2;
(NE-corner (L~ f)) `1 = E-bound (L~ f) by EUCLID:56;
then A993: (f /. 2) `1 <= (NE-corner (L~ f)) `1 by A990, PSCOMP_1:71;
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
( left_cell f,k,(Gauge C,n) misses C & right_cell f,k,(Gauge C,n) meets C ) by A428;
then A994: N-min (L~ f) = f /. 1 by A571, A608, Th32;
consider i being Element of NAT such that
A995: 1 <= i and
A996: i + 1 <= len (Gauge C,n) and
A997: ( 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 A608;
i < len (Gauge C,n) by A996, NAT_1:13;
then A998: ( (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, A992, A995, EUCLID:56, GOBOARD5:2;
1 <= i + 1 by NAT_1:12;
then A999: ((Gauge C,n) * (i + 1),(width (Gauge C,n))) `2 = ((Gauge C,n) * 1,(width (Gauge C,n))) `2 by A2, A992, A996, GOBOARD5:2;
( (NW-corner (L~ f)) `2 = (NE-corner (L~ f)) `2 & (NE-corner (L~ f)) `2 = N-bound (L~ f) ) by EUCLID:56, PSCOMP_1:82;
then f /. 2 in LSeg (NW-corner (L~ f)),(NE-corner (L~ f)) by A994, A997, A998, A999, A991, A993, GOBOARD7:9;
then f /. 2 in (LSeg (NW-corner (L~ f)),(NE-corner (L~ f))) /\ (L~ f) by A990, XBOOLE_0:def 4;
hence f is clockwise_oriented by A994, SPRECT_2:34; :: 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 A428; :: thesis:
thus ex i being Element of 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 A608; :: thesis:
let m be Element of NAT ; :: thesis:
assume that
A1000: 1 <= m and
A1001: m + 2 <= len f ; :: thesis:
A1002: F . ((m + 1) + 1) = f | ((m + 1) + 1) by A490, A580, A1001;
A1003: m + 1 < m + 2 by XREAL_1:8;
then A1004: f | (m + 1) = F . (m + 1) by A490, A580, A1001, XXREAL_0:2;
A1005: m + 1 <= len f by A1001, A1003, XXREAL_0:2;
then A1006: front_left_cell (F . (m + 1)),m,(Gauge C,n) = front_left_cell f,m,(Gauge C,n) by A571, A1000, A1004, GOBRD13:43;
A1007: ( m = (m + 1) -' 1 & m + 1 > 1 ) by A1000, NAT_1:13, NAT_D:34;
A1008: front_right_cell (F . (m + 1)),m,(Gauge C,n) = front_right_cell f,m,(Gauge C,n) by A571, A1000, A1005, A1004, GOBRD13:43;

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 A458, A1007, A1006, A1008;
hence f turns_right m, Gauge C,n by A1000, A1001, A1002, GOBRD13:44; :: 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 A458, A1007, A1006, A1008;
hence f goes_straight m, Gauge C,n by A1000, A1001, A1002, GOBRD13:46; :: 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 A458, A1007, A1006;
hence f turns_left m, Gauge C,n by A1000, A1001, A1002, GOBRD13:45; :: thesis: