set XS = X-SpanStart C,n;
set YS = Y-SpanStart C,n;
set G = Gauge C,n;
A2: len (Gauge C,n) = (2 |^ n) + 3 by JORDAN8:def 1;
defpred S₁[ Element of NAT , set , set ] means ( ( $1 = 0 implies $3 = <*((Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n))*> ) & ( $1 = 1 implies $3 = <*((Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n)),((Gauge C,n) * ((X-SpanStart C,n) -' 1),(Y-SpanStart 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 & left_cell f,((len f) -' 1),(Gauge C,n) meets C implies ( ( front_right_cell f,((len f) -' 1),(Gauge C,n) misses C & front_left_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_left (len f) -' 1, Gauge C,n & $3 = f ^ <*((Gauge C,n) * i,j)*> ) ) & ( front_right_cell f,((len f) -' 1),(Gauge C,n) misses C & 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)*> goes_straight (len f) -' 1, Gauge C,n & $3 = f ^ <*((Gauge C,n) * i,j)*> ) ) & ( 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)*> turns_right (len f) -' 1, Gauge C,n & $3 = f ^ <*((Gauge C,n) * i,j)*> ) ) ) ) & ( ( not f is_sequence_on Gauge C,n or left_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 = {} ) );
A3: 1 + 1 <= X-SpanStart C,n by JORDAN1H:58;
A4: TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;
A5: [(X-SpanStart C,n),(Y-SpanStart C,n)] in Indices (Gauge C,n) by A1, JORDAN11:8;
A6: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A7: for k being Element of NAT
for x being set ex y being set st S₁[k,x,y]

let k be Element of NAT ; :: thesis:
let x be set ; :: thesis:

per cases by NAT_1:26;

suppose A8: k = 0 ; :: thesis:

take <*((Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n))*> ; :: thesis:
thus S₁[k,x,<*((Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n))*>] by A8; :: thesis:

end;

suppose A9: k = 1 ; :: thesis:

take <*((Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n)),((Gauge C,n) * ((X-SpanStart C,n) -' 1),(Y-SpanStart C,n))*> ; :: thesis:
thus S₁[k,x,<*((Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n)),((Gauge C,n) * ((X-SpanStart C,n) -' 1),(Y-SpanStart C,n))*>] by A9; :: thesis:

end;

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

reconsider f = x as FinSequence of (TOP-REAL 2) by A11;
thus ex y being set st S₁[k,x,y] :: thesis:

proof

per cases ;

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

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

proof

per cases ;

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

A14: ((len f) -' 1) + 1 = len f by A10, A12, XREAL_1:237;
then A15: ((len f) -' 1) + (1 + 1) = (len f) + 1 ;
A16: ((len f) -' 1) + 1 in dom f by A10, A12, A14, FINSEQ_3:27;
A17: 1 <= (len f) -' 1 by A10, A12, NAT_D:49;
then consider i1, j1, i2, j2 being Element of NAT such that
A18: [i1,j1] in Indices (Gauge C,n) and
A19: f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 and
A20: [i2,j2] in Indices (Gauge C,n) and
A21: f /. (((len f) -' 1) + 1) = (Gauge C,n) * i2,j2 and
A22: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A13, A14, JORDAN8:6;
A23: i1 <= len (Gauge C,n) by A18, MATRIX_1:39;
A24: 1 <= j2 + 1 by NAT_1:12;
A25: 1 <= i2 by A20, MATRIX_1:39;
A26: j1 <= width (Gauge C,n) by A18, MATRIX_1:39;
A27: 1 <= i2 + 1 by NAT_1:12;
A28: 1 <= j2 by A20, MATRIX_1:39;
(len f) -' 1 <= len f by NAT_D:35;
then A29: (len f) -' 1 in dom f by A17, FINSEQ_3:27;
A30: j2 <= width (Gauge C,n) by A20, MATRIX_1:39;
then A31: j2 -' 1 <= width (Gauge C,n) by NAT_D:44;
A32: i2 <= len (Gauge C,n) by A20, MATRIX_1:39;
then A33: 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 A34: ( front_right_cell f,((len f) -' 1),(Gauge C,n) misses C & front_left_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 A22;

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

now

A36: now

assume i2 -' 1 < 1 ; :: thesis:
then i2 <= 1 by NAT_1:14, NAT_D:36;
then i2 = 1 by A25, XXREAL_0:1;
then cell (Gauge C,n),(1 -' 1),j1 meets C by A13, A17, A14, A18, A19, A20, A21, A35, GOBRD13:22;
then cell (Gauge C,n),0 ,j1 meets C by XREAL_1:234;
hence contradiction by A6, A26, JORDAN8:21; :: thesis:

end;

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A37: [i19,j19] in Indices (Gauge C,n) and
A38: [i29,j29] in Indices (Gauge C,n) and
A39: f1 /. ((len f) -' 1) = (Gauge C,n) * i19,j19 and
A40: f1 /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A41: f /. ((len f) -' 1) = (Gauge C,n) * i19,j19 by A29, A39, FINSEQ_4:83;
A42: f /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 by A16, A40, FINSEQ_4:83;
then A43: j2 = j29 by A20, A21, A38, GOBOARD1:21;
i2 = i29 by A20, A21, A38, A42, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & [(i29 -' 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 -' 1),j29 ) or ( i19 + 1 = i29 & j19 = j29 & [i29,(j29 + 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 + 1) ) or ( i19 = i29 + 1 & j19 = j29 & [i29,(j29 -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & [(i29 + 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 + 1),j29 ) ) by A18, A19, A28, A30, A33, A15, A35, A37, A41, A43, A36, FINSEQ_4:82, GOBOARD1:21, MATRIX_1:37; :: thesis:

end;

hence f1 turns_left (len f) -' 1, Gauge C,n by GOBRD13:def 7; :: thesis:
thus f1 = f ^ <*((Gauge C,n) * i,j)*> ; :: thesis:

end;

hence S₁[k,x,f1] by A10, A12, A13, A34; :: 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:

now

A45: now

assume j2 + 1 > len (Gauge C,n) ; :: thesis:
then A46: (len (Gauge C,n)) + 1 <= j2 + 1 by NAT_1:13;
j2 + 1 <= (len (Gauge C,n)) + 1 by A6, A30, XREAL_1:8;
then j2 + 1 = (len (Gauge C,n)) + 1 by A46, XXREAL_0:1;
then cell (Gauge C,n),i1,(len (Gauge C,n)) meets C by A13, A17, A14, A18, A19, A20, A21, A44, GOBRD13:24;
hence contradiction by A23, JORDAN8:18; :: thesis:

end;

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A47: [i19,j19] in Indices (Gauge C,n) and
A48: [i29,j29] in Indices (Gauge C,n) and
A49: f1 /. ((len f) -' 1) = (Gauge C,n) * i19,j19 and
A50: f1 /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A51: f /. ((len f) -' 1) = (Gauge C,n) * i19,j19 by A29, A49, FINSEQ_4:83;
A52: f /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 by A16, A50, FINSEQ_4:83;
then A53: j2 = j29 by A20, A21, A48, GOBOARD1:21;
i2 = i29 by A20, A21, A48, A52, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & [(i29 -' 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 -' 1),j29 ) or ( i19 + 1 = i29 & j19 = j29 & [i29,(j29 + 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 + 1) ) or ( i19 = i29 + 1 & j19 = j29 & [i29,(j29 -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & [(i29 + 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 + 1),j29 ) ) by A6, A18, A19, A25, A32, A24, A15, A44, A47, A51, A53, A45, FINSEQ_4:82, GOBOARD1:21, MATRIX_1:37; :: thesis:

end;

hence f1 turns_left (len f) -' 1, Gauge C,n by GOBRD13:def 7; :: thesis:
thus f1 = f ^ <*((Gauge C,n) * i,j)*> ; :: thesis:

end;

hence S₁[k,x,f1] by A10, A12, A13, A34; :: 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:

now

A55: now

assume j2 -' 1 < 1 ; :: thesis:
then j2 <= 1 by NAT_1:14, NAT_D:36;
then j2 = 1 by A28, XXREAL_0:1;
then cell (Gauge C,n),i2,(1 -' 1) meets C by A13, A17, A14, A18, A19, A20, A21, A54, GOBRD13:26;
then cell (Gauge C,n),i2,0 meets C by XREAL_1:234;
hence contradiction by A32, JORDAN8:20; :: thesis:

end;

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A56: [i19,j19] in Indices (Gauge C,n) and
A57: [i29,j29] in Indices (Gauge C,n) and
A58: f1 /. ((len f) -' 1) = (Gauge C,n) * i19,j19 and
A59: f1 /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A60: f /. ((len f) -' 1) = (Gauge C,n) * i19,j19 by A29, A58, FINSEQ_4:83;
A61: f /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 by A16, A59, FINSEQ_4:83;
then A62: j2 = j29 by A20, A21, A57, GOBOARD1:21;
i2 = i29 by A20, A21, A57, A61, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & [(i29 -' 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 -' 1),j29 ) or ( i19 + 1 = i29 & j19 = j29 & [i29,(j29 + 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 + 1) ) or ( i19 = i29 + 1 & j19 = j29 & [i29,(j29 -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & [(i29 + 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 + 1),j29 ) ) by A18, A19, A25, A32, A31, A15, A54, A56, A60, A62, A55, FINSEQ_4:82, GOBOARD1:21, MATRIX_1:37; :: thesis:

end;

hence f1 turns_left (len f) -' 1, Gauge C,n by GOBRD13:def 7; :: thesis:
thus f1 = f ^ <*((Gauge C,n) * i,j)*> ; :: thesis:

end;

hence S₁[k,x,f1] by A10, A12, A13, A34; :: thesis:

end;

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

now

A64: now

assume i2 + 1 > len (Gauge C,n) ; :: thesis:
then A65: (len (Gauge C,n)) + 1 <= i2 + 1 by NAT_1:13;
i2 + 1 <= (len (Gauge C,n)) + 1 by A32, XREAL_1:8;
then i2 + 1 = (len (Gauge C,n)) + 1 by A65, XXREAL_0:1;
then cell (Gauge C,n),(len (Gauge C,n)),j2 meets C by A13, A17, A14, A18, A19, A20, A21, A63, GOBRD13:28;
hence contradiction by A6, A30, JORDAN8:19; :: thesis:

end;

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A66: [i19,j19] in Indices (Gauge C,n) and
A67: [i29,j29] in Indices (Gauge C,n) and
A68: f1 /. ((len f) -' 1) = (Gauge C,n) * i19,j19 and
A69: f1 /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A70: f /. ((len f) -' 1) = (Gauge C,n) * i19,j19 by A29, A68, FINSEQ_4:83;
A71: f /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 by A16, A69, FINSEQ_4:83;
then A72: j2 = j29 by A20, A21, A67, GOBOARD1:21;
i2 = i29 by A20, A21, A67, A71, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & [(i29 -' 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 -' 1),j29 ) or ( i19 + 1 = i29 & j19 = j29 & [i29,(j29 + 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 + 1) ) or ( i19 = i29 + 1 & j19 = j29 & [i29,(j29 -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & [(i29 + 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 + 1),j29 ) ) by A18, A19, A28, A30, A27, A15, A63, A66, A70, A72, A64, FINSEQ_4:82, GOBOARD1:21, MATRIX_1:37; :: thesis:

end;

hence f1 turns_left (len f) -' 1, Gauge C,n by GOBRD13:def 7; :: thesis:
thus f1 = f ^ <*((Gauge C,n) * i,j)*> ; :: thesis:

end;

hence S₁[k,x,f1] by A10, A12, A13, A34; :: thesis:

end;

suppose A73: ( front_right_cell f,((len f) -' 1),(Gauge C,n) misses C & 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 A22;

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

now

A75: now

assume j2 + 1 > len (Gauge C,n) ; :: thesis:
then A76: (len (Gauge C,n)) + 1 <= j2 + 1 by NAT_1:13;
j2 + 1 <= (len (Gauge C,n)) + 1 by A6, A30, XREAL_1:8;
then j2 + 1 = (len (Gauge C,n)) + 1 by A76, XXREAL_0:1;
then cell (Gauge C,n),(i1 -' 1),(len (Gauge C,n)) meets C by A13, A17, A14, A18, A19, A20, A21, A73, A74, GOBRD13:35;
hence contradiction by A23, JORDAN8:18, NAT_D:44; :: thesis:

end;

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A77: [i19,j19] in Indices (Gauge C,n) and
A78: [i29,j29] in Indices (Gauge C,n) and
A79: f1 /. ((len f) -' 1) = (Gauge C,n) * i19,j19 and
A80: f1 /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A81: f /. ((len f) -' 1) = (Gauge C,n) * i19,j19 by A29, A79, FINSEQ_4:83;
A82: f /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 by A16, A80, FINSEQ_4:83;
then A83: j2 = j29 by A20, A21, A78, GOBOARD1:21;
i2 = i29 by A20, A21, A78, A82, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & [i29,(j29 + 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 + 1) ) or ( i19 + 1 = i29 & j19 = j29 & [(i29 + 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 + 1),j29 ) or ( i19 = i29 + 1 & j19 = j29 & [(i29 -' 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 -' 1),j29 ) or ( i19 = i29 & j19 = j29 + 1 & [i29,(j29 -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 -' 1) ) ) by A6, A18, A19, A25, A32, A24, A15, A74, A77, A81, A83, A75, FINSEQ_4:82, GOBOARD1:21, MATRIX_1:37; :: thesis:

end;

hence f1 goes_straight (len f) -' 1, Gauge C,n by GOBRD13:def 8; :: thesis:
thus f1 = f ^ <*((Gauge C,n) * i,j)*> ; :: thesis:

end;

hence S₁[k,x,f1] by A10, A12, A13, A73; :: thesis:

end;

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

now

A85: now

assume i2 + 1 > len (Gauge C,n) ; :: thesis:
then A86: (len (Gauge C,n)) + 1 <= i2 + 1 by NAT_1:13;
i2 + 1 <= (len (Gauge C,n)) + 1 by A32, XREAL_1:8;
then i2 + 1 = (len (Gauge C,n)) + 1 by A86, XXREAL_0:1;
then cell (Gauge C,n),(len (Gauge C,n)),j1 meets C by A13, A17, A14, A18, A19, A20, A21, A73, A84, GOBRD13:37;
hence contradiction by A6, A26, JORDAN8:19; :: thesis:

end;

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A87: [i19,j19] in Indices (Gauge C,n) and
A88: [i29,j29] in Indices (Gauge C,n) and
A89: f1 /. ((len f) -' 1) = (Gauge C,n) * i19,j19 and
A90: f1 /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A91: f /. ((len f) -' 1) = (Gauge C,n) * i19,j19 by A29, A89, FINSEQ_4:83;
A92: f /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 by A16, A90, FINSEQ_4:83;
then A93: j2 = j29 by A20, A21, A88, GOBOARD1:21;
i2 = i29 by A20, A21, A88, A92, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & [i29,(j29 + 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 + 1) ) or ( i19 + 1 = i29 & j19 = j29 & [(i29 + 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 + 1),j29 ) or ( i19 = i29 + 1 & j19 = j29 & [(i29 -' 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 -' 1),j29 ) or ( i19 = i29 & j19 = j29 + 1 & [i29,(j29 -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 -' 1) ) ) by A18, A19, A28, A30, A27, A15, A84, A87, A91, A93, A85, FINSEQ_4:82, GOBOARD1:21, MATRIX_1:37; :: thesis:

end;

hence f1 goes_straight (len f) -' 1, Gauge C,n by GOBRD13:def 8; :: thesis:
thus f1 = f ^ <*((Gauge C,n) * i,j)*> ; :: thesis:

end;

hence S₁[k,x,f1] by A10, A12, A13, A73; :: thesis:

end;

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

now

A95: now

assume i2 -' 1 < 1 ; :: thesis:
then i2 <= 1 by NAT_1:14, NAT_D:36;
then i2 = 1 by A25, XXREAL_0:1;
then cell (Gauge C,n),(1 -' 1),(j1 -' 1) meets C by A13, A17, A14, A18, A19, A20, A21, A73, A94, GOBRD13:39;
then cell (Gauge C,n),0 ,(j1 -' 1) meets C by XREAL_1:234;
hence contradiction by A6, A26, JORDAN8:21, NAT_D:44; :: thesis:

end;

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A96: [i19,j19] in Indices (Gauge C,n) and
A97: [i29,j29] in Indices (Gauge C,n) and
A98: f1 /. ((len f) -' 1) = (Gauge C,n) * i19,j19 and
A99: f1 /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A100: f /. ((len f) -' 1) = (Gauge C,n) * i19,j19 by A29, A98, FINSEQ_4:83;
A101: f /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 by A16, A99, FINSEQ_4:83;
then A102: j2 = j29 by A20, A21, A97, GOBOARD1:21;
i2 = i29 by A20, A21, A97, A101, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & [i29,(j29 + 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 + 1) ) or ( i19 + 1 = i29 & j19 = j29 & [(i29 + 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 + 1),j29 ) or ( i19 = i29 + 1 & j19 = j29 & [(i29 -' 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 -' 1),j29 ) or ( i19 = i29 & j19 = j29 + 1 & [i29,(j29 -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 -' 1) ) ) by A18, A19, A28, A30, A33, A15, A94, A96, A100, A102, A95, FINSEQ_4:82, GOBOARD1:21, MATRIX_1:37; :: thesis:

end;

hence f1 goes_straight (len f) -' 1, Gauge C,n by GOBRD13:def 8; :: thesis:
thus f1 = f ^ <*((Gauge C,n) * i,j)*> ; :: thesis:

end;

hence S₁[k,x,f1] by A10, A12, A13, A73; :: thesis:

end;

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

now

A104: now

assume j2 -' 1 < 1 ; :: thesis:
then j2 <= 1 by NAT_1:14, NAT_D:36;
then j2 = 1 by A28, XXREAL_0:1;
then cell (Gauge C,n),i1,(1 -' 1) meets C by A13, A17, A14, A18, A19, A20, A21, A73, A103, GOBRD13:41;
then cell (Gauge C,n),i1,0 meets C by XREAL_1:234;
hence contradiction by A23, JORDAN8:20; :: thesis:

end;

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A105: [i19,j19] in Indices (Gauge C,n) and
A106: [i29,j29] in Indices (Gauge C,n) and
A107: f1 /. ((len f) -' 1) = (Gauge C,n) * i19,j19 and
A108: f1 /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A109: f /. ((len f) -' 1) = (Gauge C,n) * i19,j19 by A29, A107, FINSEQ_4:83;
A110: f /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 by A16, A108, FINSEQ_4:83;
then A111: j2 = j29 by A20, A21, A106, GOBOARD1:21;
i2 = i29 by A20, A21, A106, A110, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & [i29,(j29 + 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 + 1) ) or ( i19 + 1 = i29 & j19 = j29 & [(i29 + 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 + 1),j29 ) or ( i19 = i29 + 1 & j19 = j29 & [(i29 -' 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 -' 1),j29 ) or ( i19 = i29 & j19 = j29 + 1 & [i29,(j29 -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 -' 1) ) ) by A18, A19, A25, A32, A31, A15, A103, A105, A109, A111, A104, FINSEQ_4:82, GOBOARD1:21, MATRIX_1:37; :: thesis:

end;

hence f1 goes_straight (len f) -' 1, Gauge C,n by GOBRD13:def 8; :: thesis:
thus f1 = f ^ <*((Gauge C,n) * i,j)*> ; :: thesis:

end;

hence S₁[k,x,f1] by A10, A12, A13, A73; :: thesis:

end;

suppose A112: 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 A22;

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

now

A114: now

assume i2 + 1 > len (Gauge C,n) ; :: thesis:
then A115: (len (Gauge C,n)) + 1 <= i2 + 1 by NAT_1:13;
i2 + 1 <= (len (Gauge C,n)) + 1 by A32, XREAL_1:8;
then i2 + 1 = (len (Gauge C,n)) + 1 by A115, XXREAL_0:1;
then cell (Gauge C,n),(len (Gauge C,n)),j2 meets C by A13, A17, A14, A18, A19, A20, A21, A112, A113, GOBRD13:36;
hence contradiction by A6, A30, JORDAN8:19; :: thesis:

end;

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A116: [i19,j19] in Indices (Gauge C,n) and
A117: [i29,j29] in Indices (Gauge C,n) and
A118: f1 /. ((len f) -' 1) = (Gauge C,n) * i19,j19 and
A119: f1 /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A120: f /. ((len f) -' 1) = (Gauge C,n) * i19,j19 by A29, A118, FINSEQ_4:83;
A121: f /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 by A16, A119, FINSEQ_4:83;
then A122: j2 = j29 by A20, A21, A117, GOBOARD1:21;
i2 = i29 by A20, A21, A117, A121, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & [(i29 + 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 + 1),j29 ) or ( i19 + 1 = i29 & j19 = j29 & [i29,(j29 -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 -' 1) ) or ( i19 = i29 + 1 & j19 = j29 & [i29,(j29 + 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 + 1) ) or ( i19 = i29 & j19 = j29 + 1 & [(i29 -' 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 -' 1),j29 ) ) by A18, A19, A28, A30, A27, A15, A113, A116, A120, A122, A114, FINSEQ_4:82, GOBOARD1:21, MATRIX_1:37; :: thesis:

end;

hence f1 turns_right (len f) -' 1, Gauge C,n by GOBRD13:def 6; :: thesis:
thus f1 = f ^ <*((Gauge C,n) * i,j)*> ; :: thesis:

end;

hence S₁[k,x,f1] by A10, A12, A13, A112; :: thesis:

end;

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

now

A124: now

assume j2 -' 1 < 1 ; :: thesis:
then j2 <= 1 by NAT_1:14, NAT_D:36;
then j2 = 1 by A28, XXREAL_0:1;
then cell (Gauge C,n),i2,(1 -' 1) meets C by A13, A17, A14, A18, A19, A20, A21, A112, A123, GOBRD13:38;
then cell (Gauge C,n),i2,0 meets C by XREAL_1:234;
hence contradiction by A32, JORDAN8:20; :: thesis:

end;

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A125: [i19,j19] in Indices (Gauge C,n) and
A126: [i29,j29] in Indices (Gauge C,n) and
A127: f1 /. ((len f) -' 1) = (Gauge C,n) * i19,j19 and
A128: f1 /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A129: f /. ((len f) -' 1) = (Gauge C,n) * i19,j19 by A29, A127, FINSEQ_4:83;
A130: f /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 by A16, A128, FINSEQ_4:83;
then A131: j2 = j29 by A20, A21, A126, GOBOARD1:21;
i2 = i29 by A20, A21, A126, A130, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & [(i29 + 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 + 1),j29 ) or ( i19 + 1 = i29 & j19 = j29 & [i29,(j29 -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 -' 1) ) or ( i19 = i29 + 1 & j19 = j29 & [i29,(j29 + 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 + 1) ) or ( i19 = i29 & j19 = j29 + 1 & [(i29 -' 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 -' 1),j29 ) ) by A18, A19, A25, A32, A31, A15, A123, A125, A129, A131, A124, FINSEQ_4:82, GOBOARD1:21, MATRIX_1:37; :: thesis:

end;

hence f1 turns_right (len f) -' 1, Gauge C,n by GOBRD13:def 6; :: thesis:
thus f1 = f ^ <*((Gauge C,n) * i,j)*> ; :: thesis:

end;

hence S₁[k,x,f1] by A10, A12, A13, A112; :: thesis:

end;

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

now

A133: now

assume j2 + 1 > len (Gauge C,n) ; :: thesis:
then A134: (len (Gauge C,n)) + 1 <= j2 + 1 by NAT_1:13;
j2 + 1 <= (len (Gauge C,n)) + 1 by A6, A30, XREAL_1:8;
then j2 + 1 = (len (Gauge C,n)) + 1 by A134, XXREAL_0:1;
then cell (Gauge C,n),(i2 -' 1),(len (Gauge C,n)) meets C by A13, A17, A14, A18, A19, A20, A21, A112, A132, GOBRD13:40;
hence contradiction by A32, JORDAN8:18, NAT_D:44; :: thesis:

end;

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A135: [i19,j19] in Indices (Gauge C,n) and
A136: [i29,j29] in Indices (Gauge C,n) and
A137: f1 /. ((len f) -' 1) = (Gauge C,n) * i19,j19 and
A138: f1 /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A139: f /. ((len f) -' 1) = (Gauge C,n) * i19,j19 by A29, A137, FINSEQ_4:83;
A140: f /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 by A16, A138, FINSEQ_4:83;
then A141: j2 = j29 by A20, A21, A136, GOBOARD1:21;
i2 = i29 by A20, A21, A136, A140, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & [(i29 + 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 + 1),j29 ) or ( i19 + 1 = i29 & j19 = j29 & [i29,(j29 -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 -' 1) ) or ( i19 = i29 + 1 & j19 = j29 & [i29,(j29 + 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 + 1) ) or ( i19 = i29 & j19 = j29 + 1 & [(i29 -' 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 -' 1),j29 ) ) by A6, A18, A19, A25, A32, A24, A15, A132, A135, A139, A141, A133, FINSEQ_4:82, GOBOARD1:21, MATRIX_1:37; :: thesis:

end;

hence f1 turns_right (len f) -' 1, Gauge C,n by GOBRD13:def 6; :: thesis:
thus f1 = f ^ <*((Gauge C,n) * i,j)*> ; :: thesis:

end;

hence S₁[k,x,f1] by A10, A12, A13, A112; :: thesis:

end;

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

now

A143: now

assume i2 -' 1 < 1 ; :: thesis:
then i2 <= 1 by NAT_1:14, NAT_D:36;
then i2 = 1 by A25, XXREAL_0:1;
then cell (Gauge C,n),(1 -' 1),(j2 -' 1) meets C by A13, A17, A14, A18, A19, A20, A21, A112, A142, GOBRD13:42;
then cell (Gauge C,n),0 ,(j2 -' 1) meets C by XREAL_1:234;
hence contradiction by A6, A30, JORDAN8:21, NAT_D:44; :: thesis:

end;

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A144: [i19,j19] in Indices (Gauge C,n) and
A145: [i29,j29] in Indices (Gauge C,n) and
A146: f1 /. ((len f) -' 1) = (Gauge C,n) * i19,j19 and
A147: f1 /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A148: f /. ((len f) -' 1) = (Gauge C,n) * i19,j19 by A29, A146, FINSEQ_4:83;
A149: f /. (((len f) -' 1) + 1) = (Gauge C,n) * i29,j29 by A16, A147, FINSEQ_4:83;
then A150: j2 = j29 by A20, A21, A145, GOBOARD1:21;
i2 = i29 by A20, A21, A145, A149, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & [(i29 + 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 + 1),j29 ) or ( i19 + 1 = i29 & j19 = j29 & [i29,(j29 -' 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 -' 1) ) or ( i19 = i29 + 1 & j19 = j29 & [i29,(j29 + 1)] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * i29,(j29 + 1) ) or ( i19 = i29 & j19 = j29 + 1 & [(i29 -' 1),j29] in Indices (Gauge C,n) & f1 /. (((len f) -' 1) + 2) = (Gauge C,n) * (i29 -' 1),j29 ) ) by A18, A19, A28, A30, A33, A15, A142, A144, A148, A150, A143, FINSEQ_4:82, GOBOARD1:21, MATRIX_1:37; :: thesis:

end;

hence f1 turns_right (len f) -' 1, Gauge C,n by GOBRD13:def 6; :: thesis:
thus f1 = f ^ <*((Gauge C,n) * i,j)*> ; :: thesis:

end;

hence S₁[k,x,f1] by A10, A12, A13, A112; :: thesis:

end;

suppose A151: ( not f is_sequence_on Gauge C,n or left_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 A10, A12, A151; :: thesis:

end;

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

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

end;

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

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

end;

consider F being Function such that
A154: dom F = NAT and
A155: F . 0 = {} and
A156: for k being Element of NAT holds S₁[k,F . k,F . (k + 1)] from RECDEF_1:sch 1(A7);
defpred S₂[ Element of NAT ] means F . $1 is FinSequence of (TOP-REAL 2);
A157: {} = <*> the carrier of (TOP-REAL 2) ;
A158: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A159: F . k is FinSequence of (TOP-REAL 2) ; :: thesis:

per cases by NAT_1:26;

suppose k = 0 ; :: thesis:

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

end;

suppose k = 1 ; :: thesis:

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

end;

suppose A160: k > 1 ; :: thesis:

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

proof

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

per cases ;

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

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

proof

per cases ;

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

then A163: ( 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)*> turns_right (len f) -' 1, Gauge C,n & F . (k + 1) = f ^ <*((Gauge C,n) * i,j)*> ) ) by A156, A160, A161;
A164: ( front_right_cell f,((len f) -' 1),(Gauge C,n) misses C & 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)*> goes_straight (len f) -' 1, Gauge C,n & F . (k + 1) = f ^ <*((Gauge C,n) * i,j)*> ) ) by A156, A160, A161, A162;
( front_right_cell f,((len f) -' 1),(Gauge C,n) misses C & front_left_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_left (len f) -' 1, Gauge C,n & F . (k + 1) = f ^ <*((Gauge C,n) * i,j)*> ) ) by A156, A160, A161, A162;
hence S₂[k + 1] by A164, A163; :: thesis:

end;

suppose A165: ( not f is_sequence_on Gauge C,n or left_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 A156, A160, A161, A165; :: thesis:

end;

suppose len f <> k ; :: thesis:

hence S₂[k + 1] by A156, A157, A160; :: thesis:

end;

A166: S₂[ 0 ] by A155, A157;
A167: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A166, A158);
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 A154, A167;
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 A154, FUNCT_2:def 1, RELSET_1:11;
defpred S₃[ Element of NAT ] means len (F . $1) = $1;
A168: for k being Element of NAT st S₃[k] holds
S₃[k + 1]

proof

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

per cases by NAT_1:26;

suppose k = 0 ; :: thesis:

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

end;

suppose k = 1 ; :: thesis:

hence S₃[k + 1] by A170, FINSEQ_1:61; :: thesis:

end;

suppose A171: k > 1 ; :: thesis:

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

proof

per cases ;

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

then A173: ( 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)*> turns_right (len (F . k)) -' 1, Gauge C,n & F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> ) ) by A156, A169, A171;
A174: ( front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) misses C & 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)*> goes_straight (len (F . k)) -' 1, Gauge C,n & F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> ) ) by A156, A169, A171, A172;
( front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) misses C & front_left_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_left (len (F . k)) -' 1, Gauge C,n & F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> ) ) by A156, A169, A171, A172;
hence S₃[k + 1] by A169, A174, A173, FINSEQ_2:19; :: thesis:

end;

suppose ( not F . k is_sequence_on Gauge C,n or left_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 A156, A169, A171;
hence S₃[k + 1] by A169, FINSEQ_2:19; :: 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
( right_cell (F . $1),m,(Gauge C,n) misses C & left_cell (F . $1),m,(Gauge C,n) meets C ) ) );
A175: S₃[ 0 ] by A155, CARD_1:47;
A176: for k being Element of NAT holds S₃[k] from NAT_1:sch 1(A175, A168);
A177: 1 <= X-SpanStart C,n by JORDAN1H:58, XXREAL_0:2;
A178: for k being Element of NAT st S₄[k] holds
S₄[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume that
A179: F . k is_sequence_on Gauge C,n and
A180: for m being Element of NAT st 1 <= m & m + 1 <= len (F . k) holds
( right_cell (F . k),m,(Gauge C,n) misses C & left_cell (F . k),m,(Gauge C,n) meets C ) ; :: thesis:
A181: len (F . k) = k by A176;
A182: len (F . (k + 1)) = k + 1 by A176;

per cases by NAT_1:26;

suppose A183: k = 0 ; :: thesis:

then A184: F . (k + 1) = <*((Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n))*> by A156;

A185: now

let l be Element of NAT ; :: thesis:
assume A186: l in dom (F . (k + 1)) ; :: thesis:
then A187: 1 <= l by FINSEQ_3:27;
l <= 1 by A182, A183, A186, FINSEQ_3:27;
then l = 1 by A187, 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 A5, A184, FINSEQ_4:25; :: thesis:

end;

now

let l be Element of NAT ; :: thesis:
assume that
A188: l in dom (F . (k + 1)) and
A189: l + 1 in dom (F . (k + 1)) ; :: thesis:
A190: 1 <= l by A188, FINSEQ_3:27;
l <= 1 by A182, A183, A188, FINSEQ_3:27;
then l = 1 by A190, 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 A182, A183, A189, FINSEQ_3:27; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A185, GOBOARD1:def 11; :: thesis:
let m be Element of NAT ; :: thesis:
assume that
A191: 1 <= m and
A192: m + 1 <= len (F . (k + 1)) ; :: thesis:
1 <= m + 1 by NAT_1:12;
then m + 1 = 0 + 1 by A182, A183, A192, XXREAL_0:1;
hence ( right_cell (F . (k + 1)),m,(Gauge C,n) misses C & left_cell (F . (k + 1)),m,(Gauge C,n) meets C ) by A191; :: thesis:

end;

suppose A193: k = 1 ; :: thesis:

A194: (X-SpanStart C,n) -' 1 < X-SpanStart C,n by A177, JORDAN5B:1;
A195: X-SpanStart C,n <= (X-SpanStart C,n) + 1 by NAT_1:11;
A196: [(X-SpanStart C,n),(Y-SpanStart C,n)] in Indices (Gauge C,n) by A1, JORDAN11:8;
A197: F . (k + 1) = <*((Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n)),((Gauge C,n) * ((X-SpanStart C,n) -' 1),(Y-SpanStart C,n))*> by A156, A193;
then A198: (F . (k + 1)) /. 1 = (Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n) by FINSEQ_4:26;
A199: [((X-SpanStart C,n) -' 1),(Y-SpanStart C,n)] in Indices (Gauge C,n) by A1, JORDAN11:9;
A200: (F . (k + 1)) /. 2 = (Gauge C,n) * ((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) by A197, FINSEQ_4:26;

A201: now

let l be Element of NAT ; :: thesis:
assume that
A202: l in dom (F . (k + 1)) and
A203: l + 1 in dom (F . (k + 1)) ; :: thesis:
let i1, j1, i2, j2 be Element of NAT ; :: thesis:
assume that
A204: [i1,j1] in Indices (Gauge C,n) and
A205: [i2,j2] in Indices (Gauge C,n) and
A206: (F . (k + 1)) /. l = (Gauge C,n) * i1,j1 and
A207: (F . (k + 1)) /. (l + 1) = (Gauge C,n) * i2,j2 ; :: thesis:
l <= 2 by A182, A193, A202, FINSEQ_3:27;
then A208: ( l = 0 or l = 1 or l = 2 ) by NAT_1:27;
then A209: i2 = (X-SpanStart C,n) -' 1 by A182, A193, A200, A199, A202, A203, A205, A207, FINSEQ_3:27, GOBOARD1:21;
A210: j1 = Y-SpanStart C,n by A198, A200, A196, A199, A202, A208, A204, A206, FINSEQ_3:27, GOBOARD1:21;
j2 = Y-SpanStart C,n by A182, A193, A198, A200, A196, A199, A203, A208, A205, A207, FINSEQ_3:27, GOBOARD1:21;
then A211: abs (j1 - j2) = 0 by A210, ABSVALUE:def 1;
i1 = X-SpanStart C,n by A182, A193, A198, A196, A202, A203, A208, A204, A206, FINSEQ_3:27, GOBOARD1:21;
then i2 + 1 = i1 by A3, A209, NAT_D:43, NAT_D:55;
hence (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A211, ABSVALUE:def 1; :: thesis:

end;

now

let l be Element of NAT ; :: thesis:
assume A212: l in dom (F . (k + 1)) ; :: thesis:
then l <= 2 by A182, A193, 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 A198, A200, A196, A199, A212, FINSEQ_3:27; :: thesis:

end;

hence A213: F . (k + 1) is_sequence_on Gauge C,n by A201, GOBOARD1:def 11; :: thesis:
let m be Element of NAT ; :: thesis:
assume that
A214: 1 <= m and
A215: m + 1 <= len (F . (k + 1)) ; :: thesis:
1 + 1 <= m + 1 by A214, XREAL_1:8;
then A216: m + 1 = 1 + 1 by A182, A193, A215, XXREAL_0:1;
then right_cell (F . (k + 1)),m,(Gauge C,n) = cell (Gauge C,n),((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) by A198, A200, A196, A199, A213, A215, A194, A195, GOBRD13:def 2;
hence right_cell (F . (k + 1)),m,(Gauge C,n) misses C by A1, JORDAN11:11; :: thesis:
left_cell (F . (k + 1)),m,(Gauge C,n) = cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) -' 1) by A198, A200, A196, A199, A213, A215, A216, A194, A195, GOBRD13:def 3;
hence left_cell (F . (k + 1)),m,(Gauge C,n) meets C by A1, JORDAN11:10; :: thesis:

end;

suppose A217: k > 1 ; :: thesis:

then A218: len (F . k) in dom (F . k) by A181, FINSEQ_3:27;
A219: ((len (F . k)) -' 1) + 1 = len (F . k) by A181, A217, XREAL_1:237;
then A220: ((len (F . k)) -' 1) + (1 + 1) = (len (F . k)) + 1 ;
A221: 1 <= (len (F . k)) -' 1 by A181, A217, NAT_D:49;
then consider i1, j1, i2, j2 being Element of NAT such that
A222: [i1,j1] in Indices (Gauge C,n) and
A223: (F . k) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 and
A224: [i2,j2] in Indices (Gauge C,n) and
A225: (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 A179, A219, JORDAN8:6;
A226: ( front_left_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 A179, A181, A217, A222, A223, A224, A225, JORDAN1H:67;
(i1 + 1) + 1 = i1 + 2 ;
then A227: ( front_left_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 A179, A181, A217, A222, A223, A224, A225, JORDAN1H:66;
(j1 + 1) + 1 = j1 + 2 ;
then A228: ( front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C & i1 = i2 & j1 + 1 = j2 implies [i1,(j2 + 1)] in Indices (Gauge C,n) ) by A179, A181, A217, A222, A223, A224, A225, JORDAN1H:65;
A229: ( front_right_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 A179, A181, A217, A222, A223, A224, A225, JORDAN1H:72;
(len (F . k)) -' 1 <= len (F . k) by NAT_D:35;
then A230: (len (F . k)) -' 1 in dom (F . k) by A221, FINSEQ_3:27;
A231: ( front_right_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 A179, A181, A217, A222, A223, A224, A225, JORDAN1H:71;
A232: ( front_right_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 A179, A181, A217, A222, A223, A224, A225, JORDAN1H:70;
A233: ( front_right_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 A179, A181, A217, A222, A223, A224, A225, JORDAN1H:69;
A234: ( front_left_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 A179, A181, A217, A222, A223, A224, A225, JORDAN1H:68;
A235: 1 <= j2 by A224, MATRIX_1:39;
A236: left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C by A180, A221, A219;
then A237: ( i1 = i2 & j1 + 1 = j2 implies [(i1 -' 1),(j1 + 1)] in Indices (Gauge C,n) ) by A179, A181, A217, A222, A223, A224, A225, JORDAN1H:61;
A238: ( i1 = i2 & j1 = j2 + 1 implies [(i1 + 1),j2] in Indices (Gauge C,n) ) by A179, A181, A217, A222, A223, A224, A225, A236, JORDAN1H:64;
A239: ( i1 = i2 + 1 & j1 = j2 implies [i2,(j1 -' 1)] in Indices (Gauge C,n) ) by A179, A181, A217, A222, A223, A224, A225, A236, JORDAN1H:63;
A240: ( i1 + 1 = i2 & j1 = j2 implies [(i1 + 1),(j1 + 1)] in Indices (Gauge C,n) ) by A179, A181, A217, A222, A223, A224, A225, A236, JORDAN1H:62;
A241: 1 <= i2 by A224, MATRIX_1:39;
thus A242: F . (k + 1) is_sequence_on Gauge C,n :: thesis:

proof

per cases ;

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

then consider i, j being Element of NAT such that
A243: (F . k) ^ <*((Gauge C,n) * i,j)*> turns_left (len (F . k)) -' 1, Gauge C,n and
A244: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A156, A179, A181, A217, A236;
set f = (F . k) ^ <*((Gauge C,n) * i,j)*>;
A245: ((F . k) ^ <*((Gauge C,n) * i,j)*>) /. ((len (F . k)) + 1) = (Gauge C,n) * i,j by FINSEQ_4:82;
A246: ((F . k) ^ <*((Gauge C,n) * i,j)*>) /. (len (F . k)) = (Gauge C,n) * i2,j2 by A225, A218, FINSEQ_4:83;
A247: ((F . k) ^ <*((Gauge C,n) * i,j)*>) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 by A223, A230, FINSEQ_4:83;
thus F . (k + 1) is_sequence_on Gauge C,n :: thesis:

proof

per cases by A219, A222, A224, A220, A243, A247, A246, GOBRD13:def 7;

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

now

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A250: [i19,j19] in Indices (Gauge C,n) and
A251: [i29,j29] in Indices (Gauge C,n) and
A252: (F . k) /. (len (F . k)) = (Gauge C,n) * i19,j19 and
A253: (Gauge C,n) * (i2 -' 1),j2 = (Gauge C,n) * i29,j29 ; :: thesis:
A254: i2 -' 1 = i29 by A237, A248, A251, A253, GOBOARD1:21;
i2 = i19 by A224, A225, A250, A252, GOBOARD1:21;
then i19 - i29 = i2 - (i2 - 1) by A241, A254, XREAL_1:235;
then A255: abs (i19 - i29) = 1 by ABSVALUE:def 1;
A256: j2 = j29 by A237, A248, A251, A253, GOBOARD1:21;
j2 = j19 by A224, A225, A250, A252, GOBOARD1:21;
then abs (j29 - j19) = 0 by A256, ABSVALUE:def 1;
hence (abs (i29 - i19)) + (abs (j29 - j19)) = 1 by A255, UNIFORM1:13; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A179, A181, A217, A237, A244, A245, A248, A249, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A259: [i19,j19] in Indices (Gauge C,n) and
A260: [i29,j29] in Indices (Gauge C,n) and
A261: (F . k) /. (len (F . k)) = (Gauge C,n) * i19,j19 and
A262: (Gauge C,n) * i2,(j2 + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A263: i2 = i29 by A240, A257, A260, A262, GOBOARD1:21;
i2 = i19 by A224, A225, A259, A261, GOBOARD1:21;
then A264: abs (i29 - i19) = 0 by A263, ABSVALUE:def 1;
A265: j2 + 1 = j29 by A240, A257, A260, A262, GOBOARD1:21;
j2 = j19 by A224, A225, A259, A261, GOBOARD1:21;
hence (abs (i29 - i19)) + (abs (j29 - j19)) = 1 by A265, A264, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A179, A181, A217, A240, A244, A245, A257, A258, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A268: [i19,j19] in Indices (Gauge C,n) and
A269: [i29,j29] in Indices (Gauge C,n) and
A270: (F . k) /. (len (F . k)) = (Gauge C,n) * i19,j19 and
A271: (Gauge C,n) * i2,(j2 -' 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A272: j2 -' 1 = j29 by A239, A266, A269, A271, GOBOARD1:21;
j2 = j19 by A224, A225, A268, A270, GOBOARD1:21;
then j19 - j29 = j2 - (j2 - 1) by A235, A272, XREAL_1:235;
then A273: abs (j19 - j29) = 1 by ABSVALUE:def 1;
A274: i2 = i29 by A239, A266, A269, A271, GOBOARD1:21;
i2 = i19 by A224, A225, A268, A270, GOBOARD1:21;
then abs (i29 - i19) = 0 by A274, ABSVALUE:def 1;
hence (abs (i29 - i19)) + (abs (j29 - j19)) = 1 by A273, UNIFORM1:13; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A179, A181, A217, A239, A244, A245, A266, A267, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A277: [i19,j19] in Indices (Gauge C,n) and
A278: [i29,j29] in Indices (Gauge C,n) and
A279: (F . k) /. (len (F . k)) = (Gauge C,n) * i19,j19 and
A280: (Gauge C,n) * (i2 + 1),j2 = (Gauge C,n) * i29,j29 ; :: thesis:
A281: j2 = j29 by A238, A275, A278, A280, GOBOARD1:21;
j2 = j19 by A224, A225, A277, A279, GOBOARD1:21;
then A282: abs (j29 - j19) = 0 by A281, ABSVALUE:def 1;
A283: i2 + 1 = i29 by A238, A275, A278, A280, GOBOARD1:21;
i2 = i19 by A224, A225, A277, A279, GOBOARD1:21;
hence (abs (i29 - i19)) + (abs (j29 - j19)) = 1 by A283, A282, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A179, A181, A217, A238, A244, A245, A275, A276, CARD_1:47, JORDAN8:9; :: thesis:

end;

suppose A284: ( front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) misses C & 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
A285: (F . k) ^ <*((Gauge C,n) * i,j)*> goes_straight (len (F . k)) -' 1, Gauge C,n and
A286: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A156, A179, A181, A217, A236;
set f = (F . k) ^ <*((Gauge C,n) * i,j)*>;
A287: ((F . k) ^ <*((Gauge C,n) * i,j)*>) /. ((len (F . k)) + 1) = (Gauge C,n) * i,j by FINSEQ_4:82;
A288: ((F . k) ^ <*((Gauge C,n) * i,j)*>) /. (len (F . k)) = (Gauge C,n) * i2,j2 by A225, A218, FINSEQ_4:83;
A289: ((F . k) ^ <*((Gauge C,n) * i,j)*>) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 by A223, A230, FINSEQ_4:83;
thus F . (k + 1) is_sequence_on Gauge C,n :: thesis:

proof

per cases by A219, A222, A224, A220, A285, A289, A288, GOBRD13:def 8;

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

now

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A292: [i19,j19] in Indices (Gauge C,n) and
A293: [i29,j29] in Indices (Gauge C,n) and
A294: (F . k) /. (len (F . k)) = (Gauge C,n) * i19,j19 and
A295: (Gauge C,n) * i2,(j2 + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A296: i2 = i19 by A224, A225, A292, A294, GOBOARD1:21;
i2 = i29 by A228, A284, A290, A293, A295, GOBOARD1:21;
then A297: abs (i29 - i19) = 0 by A296, ABSVALUE:def 1;
A298: j2 = j19 by A224, A225, A292, A294, GOBOARD1:21;
j2 + 1 = j29 by A228, A284, A290, A293, A295, GOBOARD1:21;
hence (abs (i29 - i19)) + (abs (j29 - j19)) = 1 by A298, A297, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A179, A181, A217, A228, A284, A286, A287, A290, A291, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A301: [i19,j19] in Indices (Gauge C,n) and
A302: [i29,j29] in Indices (Gauge C,n) and
A303: (F . k) /. (len (F . k)) = (Gauge C,n) * i19,j19 and
A304: (Gauge C,n) * (i2 + 1),j2 = (Gauge C,n) * i29,j29 ; :: thesis:
A305: j2 = j19 by A224, A225, A301, A303, GOBOARD1:21;
j2 = j29 by A227, A284, A299, A302, A304, GOBOARD1:21;
then A306: abs (j29 - j19) = 0 by A305, ABSVALUE:def 1;
A307: i2 = i19 by A224, A225, A301, A303, GOBOARD1:21;
i2 + 1 = i29 by A227, A284, A299, A302, A304, GOBOARD1:21;
hence (abs (i29 - i19)) + (abs (j29 - j19)) = 1 by A307, A306, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A179, A181, A217, A227, A284, A286, A287, A299, A300, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A310: [i19,j19] in Indices (Gauge C,n) and
A311: [i29,j29] in Indices (Gauge C,n) and
A312: (F . k) /. (len (F . k)) = (Gauge C,n) * i19,j19 and
A313: (Gauge C,n) * (i2 -' 1),j2 = (Gauge C,n) * i29,j29 ; :: thesis:
A314: i2 = i19 by A224, A225, A310, A312, GOBOARD1:21;
i2 -' 1 = i29 by A226, A284, A308, A311, A313, GOBOARD1:21;
then i19 - i29 = i2 - (i2 - 1) by A241, A314, XREAL_1:235;
then A315: abs (i19 - i29) = 1 by ABSVALUE:def 1;
A316: j2 = j19 by A224, A225, A310, A312, GOBOARD1:21;
j2 = j29 by A226, A284, A308, A311, A313, GOBOARD1:21;
then abs (j29 - j19) = 0 by A316, ABSVALUE:def 1;
hence (abs (i29 - i19)) + (abs (j29 - j19)) = 1 by A315, UNIFORM1:13; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A179, A181, A217, A226, A284, A286, A287, A308, A309, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A319: [i19,j19] in Indices (Gauge C,n) and
A320: [i29,j29] in Indices (Gauge C,n) and
A321: (F . k) /. (len (F . k)) = (Gauge C,n) * i19,j19 and
A322: (Gauge C,n) * i2,(j2 -' 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A323: j2 = j19 by A224, A225, A319, A321, GOBOARD1:21;
j2 -' 1 = j29 by A234, A284, A317, A320, A322, GOBOARD1:21;
then j19 - j29 = j2 - (j2 - 1) by A235, A323, XREAL_1:235;
then A324: abs (j19 - j29) = 1 by ABSVALUE:def 1;
A325: i2 = i19 by A224, A225, A319, A321, GOBOARD1:21;
i2 = i29 by A234, A284, A317, A320, A322, GOBOARD1:21;
then abs (i29 - i19) = 0 by A325, ABSVALUE:def 1;
hence (abs (i29 - i19)) + (abs (j29 - j19)) = 1 by A324, UNIFORM1:13; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A179, A181, A217, A234, A284, A286, A287, A317, A318, CARD_1:47, JORDAN8:9; :: thesis:

end;

suppose A326: 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
A327: (F . k) ^ <*((Gauge C,n) * i,j)*> turns_right (len (F . k)) -' 1, Gauge C,n and
A328: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A156, A179, A181, A217, A236;
set f = (F . k) ^ <*((Gauge C,n) * i,j)*>;
A329: ((F . k) ^ <*((Gauge C,n) * i,j)*>) /. ((len (F . k)) + 1) = (Gauge C,n) * i,j by FINSEQ_4:82;
A330: ((F . k) ^ <*((Gauge C,n) * i,j)*>) /. (len (F . k)) = (Gauge C,n) * i2,j2 by A225, A218, FINSEQ_4:83;
A331: ((F . k) ^ <*((Gauge C,n) * i,j)*>) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 by A223, A230, FINSEQ_4:83;
thus F . (k + 1) is_sequence_on Gauge C,n :: thesis:

proof

per cases by A219, A222, A224, A220, A327, A331, A330, GOBRD13:def 6;

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

now

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A334: [i19,j19] in Indices (Gauge C,n) and
A335: [i29,j29] in Indices (Gauge C,n) and
A336: (F . k) /. (len (F . k)) = (Gauge C,n) * i19,j19 and
A337: (Gauge C,n) * (i2 + 1),j2 = (Gauge C,n) * i29,j29 ; :: thesis:
A338: j2 = j19 by A224, A225, A334, A336, GOBOARD1:21;
j2 = j29 by A233, A326, A332, A335, A337, GOBOARD1:21;
then A339: abs (j29 - j19) = 0 by A338, ABSVALUE:def 1;
A340: i2 = i19 by A224, A225, A334, A336, GOBOARD1:21;
i2 + 1 = i29 by A233, A326, A332, A335, A337, GOBOARD1:21;
hence (abs (i29 - i19)) + (abs (j29 - j19)) = 1 by A340, A339, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A179, A181, A217, A233, A326, A328, A329, A332, A333, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A343: [i19,j19] in Indices (Gauge C,n) and
A344: [i29,j29] in Indices (Gauge C,n) and
A345: (F . k) /. (len (F . k)) = (Gauge C,n) * i19,j19 and
A346: (Gauge C,n) * i2,(j2 -' 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A347: j2 = j19 by A224, A225, A343, A345, GOBOARD1:21;
j2 -' 1 = j29 by A232, A326, A341, A344, A346, GOBOARD1:21;
then j19 - j29 = j2 - (j2 - 1) by A235, A347, XREAL_1:235;
then A348: abs (j19 - j29) = 1 by ABSVALUE:def 1;
A349: i2 = i19 by A224, A225, A343, A345, GOBOARD1:21;
i2 = i29 by A232, A326, A341, A344, A346, GOBOARD1:21;
then abs (i29 - i19) = 0 by A349, ABSVALUE:def 1;
hence (abs (i29 - i19)) + (abs (j29 - j19)) = 1 by A348, UNIFORM1:13; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A179, A181, A217, A232, A326, A328, A329, A341, A342, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A352: [i19,j19] in Indices (Gauge C,n) and
A353: [i29,j29] in Indices (Gauge C,n) and
A354: (F . k) /. (len (F . k)) = (Gauge C,n) * i19,j19 and
A355: (Gauge C,n) * i2,(j2 + 1) = (Gauge C,n) * i29,j29 ; :: thesis:
A356: i2 = i19 by A224, A225, A352, A354, GOBOARD1:21;
i2 = i29 by A231, A326, A350, A353, A355, GOBOARD1:21;
then A357: abs (i29 - i19) = 0 by A356, ABSVALUE:def 1;
A358: j2 = j19 by A224, A225, A352, A354, GOBOARD1:21;
j2 + 1 = j29 by A231, A326, A350, A353, A355, GOBOARD1:21;
hence (abs (i29 - i19)) + (abs (j29 - j19)) = 1 by A358, A357, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A179, A181, A217, A231, A326, A328, A329, A350, A351, CARD_1:47, JORDAN8:9; :: thesis:

end;

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

now

let i19, j19, i29, j29 be Element of NAT ; :: thesis:
assume that
A361: [i19,j19] in Indices (Gauge C,n) and
A362: [i29,j29] in Indices (Gauge C,n) and
A363: (F . k) /. (len (F . k)) = (Gauge C,n) * i19,j19 and
A364: (Gauge C,n) * (i2 -' 1),j2 = (Gauge C,n) * i29,j29 ; :: thesis:
A365: i2 = i19 by A224, A225, A361, A363, GOBOARD1:21;
i2 -' 1 = i29 by A229, A326, A359, A362, A364, GOBOARD1:21;
then i19 - i29 = i2 - (i2 - 1) by A241, A365, XREAL_1:235;
then A366: abs (i19 - i29) = 1 by ABSVALUE:def 1;
A367: j2 = j19 by A224, A225, A361, A363, GOBOARD1:21;
j2 = j29 by A229, A326, A359, A362, A364, GOBOARD1:21;
then abs (j29 - j19) = 0 by A367, ABSVALUE:def 1;
hence (abs (i29 - i19)) + (abs (j29 - j19)) = 1 by A366, UNIFORM1:13; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge C,n by A179, A181, A217, A229, A326, A328, A329, A359, A360, CARD_1:47, JORDAN8:9; :: thesis:

end;

let m be Element of NAT ; :: thesis:
assume that
A368: 1 <= m and
A369: m + 1 <= len (F . (k + 1)) ; :: thesis:
A370: right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) misses C by A180, A221, A219;

now

per cases ;

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

A372: (j2 -' 1) + 1 = j2 by A235, XREAL_1:237;
A373: (i2 -' 1) + 1 = i2 by A241, XREAL_1:237;
thus ( right_cell (F . (k + 1)),m,(Gauge C,n) misses C & left_cell (F . (k + 1)),m,(Gauge C,n) meets C ) :: thesis:

proof

per cases ;

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

then A375: 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 A156, A179, A181, A217, A236;
then A376: (F . (k + 1)) /. (len (F . k)) = (Gauge C,n) * i2,j2 by A225, A218, FINSEQ_4:83;
A377: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 by A223, A230, A375, FINSEQ_4:83;

now

per cases by A219, A222, A224, A220, A375, A377, A376, GOBRD13:def 7;

suppose that A378: ( i1 = i2 & j1 + 1 = j2 ) and
A379: (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),(i1 -' 1),j2 by A179, A221, A219, A222, A223, A224, A225, A378, GOBRD13:35;
hence right_cell (F . (k + 1)),m,(Gauge C,n) misses C by A181, A182, A224, A237, A242, A368, A371, A373, A374, A376, A378, A379, GOBRD13:27; :: thesis:
A380: j2 -' 1 = j1 by A378, NAT_D:34;
cell (Gauge C,n),(i1 -' 1),j1 meets C by A179, A221, A219, A222, A223, A224, A225, A236, A378, GOBRD13:22;
hence left_cell (F . (k + 1)),m,(Gauge C,n) meets C by A181, A182, A224, A237, A242, A368, A371, A373, A376, A378, A379, A380, GOBRD13:26; :: thesis:

end;

suppose that A381: ( i1 + 1 = i2 & j1 = j2 ) and
A382: (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 by A179, A221, A219, A222, A223, A224, A225, A381, GOBRD13:37;
hence right_cell (F . (k + 1)),m,(Gauge C,n) misses C by A181, A182, A224, A240, A242, A368, A371, A374, A376, A381, A382, GOBRD13:23; :: thesis:
A383: (i1 + 1) -' 1 = i1 by NAT_D:34;
cell (Gauge C,n),i1,j1 meets C by A179, A221, A219, A222, A223, A224, A225, A236, A381, GOBRD13:24;
hence left_cell (F . (k + 1)),m,(Gauge C,n) meets C by A181, A182, A224, A240, A242, A368, A371, A376, A381, A382, A383, GOBRD13:22; :: thesis:

end;

suppose that A384: ( i1 = i2 + 1 & j1 = j2 ) and
A385: (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 -' 1),(j2 -' 1) by A179, A221, A219, A222, A223, A224, A225, A384, GOBRD13:39;
hence right_cell (F . (k + 1)),m,(Gauge C,n) misses C by A181, A182, A224, A239, A242, A368, A371, A372, A374, A376, A384, A385, GOBRD13:29; :: thesis:
cell (Gauge C,n),i2,(j2 -' 1) meets C by A179, A221, A219, A222, A223, A224, A225, A236, A384, GOBRD13:26;
hence left_cell (F . (k + 1)),m,(Gauge C,n) meets C by A181, A182, A224, A239, A242, A368, A371, A372, A376, A384, A385, GOBRD13:28; :: thesis:

end;

suppose that A386: ( i1 = i2 & j1 = j2 + 1 ) and
A387: (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 -' 1) by A179, A221, A219, A222, A223, A224, A225, A386, GOBRD13:41;
hence right_cell (F . (k + 1)),m,(Gauge C,n) misses C by A181, A182, A224, A238, A242, A368, A371, A374, A376, A386, A387, GOBRD13:25; :: thesis:
cell (Gauge C,n),i2,j2 meets C by A179, A221, A219, A222, A223, A224, A225, A236, A386, GOBRD13:28;
hence left_cell (F . (k + 1)),m,(Gauge C,n) meets C by A181, A182, A224, A238, A242, A368, A371, A376, A386, A387, GOBRD13:24; :: thesis:

end;

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

end;

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

then A389: 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 A156, A179, A181, A217, A236;
then A390: (F . (k + 1)) /. (len (F . k)) = (Gauge C,n) * i2,j2 by A225, A218, FINSEQ_4:83;
A391: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 by A223, A230, A389, FINSEQ_4:83;

now

per cases by A219, A222, A224, A220, A389, A391, A390, GOBRD13:def 8;

suppose that A392: ( i1 = i2 & j1 + 1 = j2 ) and
A393: (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),i1,j2 by A179, A221, A219, A222, A223, A224, A225, A392, GOBRD13:36;
hence right_cell (F . (k + 1)),m,(Gauge C,n) misses C by A181, A182, A224, A228, A242, A368, A371, A388, A390, A392, A393, GOBRD13:23; :: thesis:
front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),(i1 -' 1),j2 by A179, A221, A219, A222, A223, A224, A225, A392, GOBRD13:35;
hence left_cell (F . (k + 1)),m,(Gauge C,n) meets C by A181, A182, A224, A228, A242, A368, A371, A388, A390, A392, A393, GOBRD13:22; :: thesis:

end;

suppose that A394: ( i1 + 1 = i2 & j1 = j2 ) and
A395: (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,(j2 -' 1) by A179, A221, A219, A222, A223, A224, A225, A394, GOBRD13:38;
hence right_cell (F . (k + 1)),m,(Gauge C,n) misses C by A181, A182, A224, A227, A242, A368, A371, A388, A390, A394, A395, GOBRD13:25; :: thesis:
front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),i2,j2 by A179, A221, A219, A222, A223, A224, A225, A394, GOBRD13:37;
hence left_cell (F . (k + 1)),m,(Gauge C,n) meets C by A181, A182, A224, A227, A242, A368, A371, A388, A390, A394, A395, GOBRD13:24; :: thesis:

end;

suppose that A396: ( i1 = i2 + 1 & j1 = j2 ) and
A397: (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 by A179, A221, A219, A222, A223, A224, A225, A396, GOBRD13:40;
hence right_cell (F . (k + 1)),m,(Gauge C,n) misses C by A181, A182, A224, A226, A242, A368, A371, A373, A388, A390, A396, A397, GOBRD13:27; :: thesis:
front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),(i2 -' 1),(j2 -' 1) by A179, A221, A219, A222, A223, A224, A225, A396, GOBRD13:39;
hence left_cell (F . (k + 1)),m,(Gauge C,n) meets C by A181, A182, A224, A226, A242, A368, A371, A373, A388, A390, A396, A397, GOBRD13:26; :: thesis:

end;

suppose that A398: ( i1 = i2 & j1 = j2 + 1 ) and
A399: (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 -' 1) by A179, A221, A219, A222, A223, A224, A225, A398, GOBRD13:42;
hence right_cell (F . (k + 1)),m,(Gauge C,n) misses C by A181, A182, A224, A234, A242, A368, A371, A372, A388, A390, A398, A399, GOBRD13:29; :: thesis:
front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),i2,(j2 -' 1) by A179, A221, A219, A222, A223, A224, A225, A398, GOBRD13:41;
hence left_cell (F . (k + 1)),m,(Gauge C,n) meets C by A181, A182, A224, A234, A242, A368, A371, A372, A388, A390, A398, A399, GOBRD13:28; :: thesis:

end;

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

end;

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

then A401: 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 A156, A179, A181, A217, A236;
then A402: (F . (k + 1)) /. (len (F . k)) = (Gauge C,n) * i2,j2 by A225, A218, FINSEQ_4:83;
A403: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 by A223, A230, A401, FINSEQ_4:83;

now

per cases by A219, A222, A224, A220, A401, A403, A402, GOBRD13:def 6;

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

A406: j2 -' 1 = j1 by A404, NAT_D:34;
cell (Gauge C,n),i1,j1 misses C by A179, A221, A219, A222, A223, A224, A225, A370, A404, GOBRD13:23;
hence right_cell (F . (k + 1)),m,(Gauge C,n) misses C by A181, A182, A224, A233, A242, A368, A371, A400, A402, A404, A405, A406, GOBRD13:25; :: thesis:
front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),i2,j2 by A179, A221, A219, A222, A223, A224, A225, A404, GOBRD13:36;
hence left_cell (F . (k + 1)),m,(Gauge C,n) meets C by A181, A182, A224, A233, A242, A368, A371, A400, A402, A404, A405, GOBRD13:24; :: thesis:

end;

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

A409: i2 -' 1 = i1 by A407, NAT_D:34;
cell (Gauge C,n),i1,(j1 -' 1) misses C by A179, A221, A219, A222, A223, A224, A225, A370, A407, GOBRD13:25;
hence right_cell (F . (k + 1)),m,(Gauge C,n) misses C by A181, A182, A224, A232, A242, A368, A371, A372, A400, A402, A407, A408, A409, GOBRD13:29; :: thesis:
front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),i2,(j2 -' 1) by A179, A221, A219, A222, A223, A224, A225, A407, GOBRD13:38;
hence left_cell (F . (k + 1)),m,(Gauge C,n) meets C by A181, A182, A224, A232, A242, A368, A371, A372, A400, A402, A407, A408, GOBRD13:28; :: thesis:

end;

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

cell (Gauge C,n),i2,j2 misses C by A179, A221, A219, A222, A223, A224, A225, A370, A410, GOBRD13:27;
hence right_cell (F . (k + 1)),m,(Gauge C,n) misses C by A181, A182, A224, A231, A242, A368, A371, A400, A402, A410, A411, GOBRD13:23; :: thesis:
front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),(i2 -' 1),j2 by A179, A221, A219, A222, A223, A224, A225, A410, GOBRD13:40;
hence left_cell (F . (k + 1)),m,(Gauge C,n) meets C by A181, A182, A224, A231, A242, A368, A371, A400, A402, A410, A411, GOBRD13:22; :: thesis:

end;

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

cell (Gauge C,n),(i2 -' 1),j2 misses C by A179, A221, A219, A222, A223, A224, A225, A370, A412, GOBRD13:29;
hence right_cell (F . (k + 1)),m,(Gauge C,n) misses C by A181, A182, A224, A229, A242, A368, A371, A373, A400, A402, A412, A413, GOBRD13:27; :: thesis:
front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) = cell (Gauge C,n),(i2 -' 1),(j2 -' 1) by A179, A221, A219, A222, A223, A224, A225, A412, GOBRD13:42;
hence left_cell (F . (k + 1)),m,(Gauge C,n) meets C by A181, A182, A224, A229, A242, A368, A371, A373, A400, A402, A412, A413, GOBRD13:26; :: thesis:

end;

hence ( right_cell (F . (k + 1)),m,(Gauge C,n) misses C & left_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 A369, XXREAL_0:1;
then A414: m + 1 <= len (F . k) by A181, A182, NAT_1:13;
then consider i1, j1, i2, j2 being Element of NAT such that
A415: [i1,j1] in Indices (Gauge C,n) and
A416: (F . k) /. m = (Gauge C,n) * i1,j1 and
A417: [i2,j2] in Indices (Gauge C,n) and
A418: (F . k) /. (m + 1) = (Gauge C,n) * i2,j2 and
A419: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A179, A368, JORDAN8:6;
A420: right_cell (F . k),m,(Gauge C,n) misses C by A180, A368, A414;

A421: now

per cases ;

suppose ( front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) misses C & front_left_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_left (len (F . k)) -' 1, Gauge C,n and
A422: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A156, A179, A181, A217, A236;
take i = i; :: thesis:
take j = j; :: thesis:
thus F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A422; :: thesis:

end;

suppose ( front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) misses C & 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)*> goes_straight (len (F . k)) -' 1, Gauge C,n and
A423: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A156, A179, A181, A217, A236;
take i = i; :: thesis:
take j = j; :: thesis:
thus F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A423; :: thesis:

end;

suppose 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)*> turns_right (len (F . k)) -' 1, Gauge C,n and
A424: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A156, A179, A181, A217, A236;
take i = i; :: thesis:
take j = j; :: thesis:
thus F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A424; :: thesis:

end;

1 <= m + 1 by NAT_1:12;
then m + 1 in dom (F . k) by A414, FINSEQ_3:27;
then A425: (F . (k + 1)) /. (m + 1) = (Gauge C,n) * i2,j2 by A418, A421, FINSEQ_4:83;
A426: left_cell (F . k),m,(Gauge C,n) meets C by A180, A368, A414;
m <= len (F . k) by A414, NAT_1:13;
then m in dom (F . k) by A368, FINSEQ_3:27;
then A427: (F . (k + 1)) /. m = (Gauge C,n) * i1,j1 by A416, A421, FINSEQ_4:83;

now

per cases by A419;

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

then A429: right_cell (F . k),m,(Gauge C,n) = cell (Gauge C,n),i1,j1 by A179, A368, A414, A415, A416, A417, A418, GOBRD13:23;
left_cell (F . k),m,(Gauge C,n) = cell (Gauge C,n),(i1 -' 1),j1 by A179, A368, A414, A415, A416, A417, A418, A428, GOBRD13:22;
hence ( right_cell (F . (k + 1)),m,(Gauge C,n) misses C & left_cell (F . (k + 1)),m,(Gauge C,n) meets C ) by A242, A368, A369, A415, A417, A420, A426, A427, A425, A428, A429, GOBRD13:22, GOBRD13:23; :: thesis:

end;

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

then A431: right_cell (F . k),m,(Gauge C,n) = cell (Gauge C,n),i1,(j1 -' 1) by A179, A368, A414, A415, A416, A417, A418, GOBRD13:25;
left_cell (F . k),m,(Gauge C,n) = cell (Gauge C,n),i1,j1 by A179, A368, A414, A415, A416, A417, A418, A430, GOBRD13:24;
hence ( right_cell (F . (k + 1)),m,(Gauge C,n) misses C & left_cell (F . (k + 1)),m,(Gauge C,n) meets C ) by A242, A368, A369, A415, A417, A420, A426, A427, A425, A430, A431, GOBRD13:24, GOBRD13:25; :: thesis:

end;

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

then A433: right_cell (F . k),m,(Gauge C,n) = cell (Gauge C,n),i2,j2 by A179, A368, A414, A415, A416, A417, A418, GOBRD13:27;
left_cell (F . k),m,(Gauge C,n) = cell (Gauge C,n),i2,(j2 -' 1) by A179, A368, A414, A415, A416, A417, A418, A432, GOBRD13:26;
hence ( right_cell (F . (k + 1)),m,(Gauge C,n) misses C & left_cell (F . (k + 1)),m,(Gauge C,n) meets C ) by A242, A368, A369, A415, A417, A420, A426, A427, A425, A432, A433, GOBRD13:26, GOBRD13:27; :: thesis:

end;

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

then A435: right_cell (F . k),m,(Gauge C,n) = cell (Gauge C,n),(i1 -' 1),j2 by A179, A368, A414, A415, A416, A417, A418, GOBRD13:29;
left_cell (F . k),m,(Gauge C,n) = cell (Gauge C,n),i2,j2 by A179, A368, A414, A415, A416, A417, A418, A434, GOBRD13:28;
hence ( right_cell (F . (k + 1)),m,(Gauge C,n) misses C & left_cell (F . (k + 1)),m,(Gauge C,n) meets C ) by A242, A368, A369, A415, A417, A420, A426, A427, A425, A434, A435, GOBRD13:28, GOBRD13:29; :: thesis:

end;

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

end;

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

end;

A436: S₄[ 0 ]

proof

A437: 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 A155;
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 ) by A155;
hence F . 0 is_sequence_on Gauge C,n by A437, GOBOARD1:def 11; :: thesis:
let m be Element of NAT ; :: thesis:
assume that
1 <= m and
A438: m + 1 <= len (F . 0 ) ; :: thesis:
thus ( right_cell (F . 0 ),m,(Gauge C,n) misses C & left_cell (F . 0 ),m,(Gauge C,n) meets C ) by A155, A438, CARD_1:47; :: thesis:

end;

A439: for k being Element of NAT holds S₄[k] from NAT_1:sch 1(A436, A178);
A440: 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 & front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) misses C & front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) misses C holds
( 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
A441: k > 1 and
A442: [i1,j1] in Indices (Gauge C,n) and
A443: (F . k) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 and
A444: [i2,j2] in Indices (Gauge C,n) and
A445: (F . k) /. (len (F . k)) = (Gauge C,n) * i2,j2 ; :: thesis:
A446: len (F . k) = k by A176;
then A447: 1 <= (len (F . k)) -' 1 by A441, NAT_D:49;
(len (F . k)) -' 1 <= len (F . k) by NAT_D:35;
then A448: (len (F . k)) -' 1 in dom (F . k) by A447, FINSEQ_3:27;
A449: i1 + 1 > i1 by NAT_1:13;
A450: F . k is_sequence_on Gauge C,n by A439;
A451: j1 + 1 > j1 by NAT_1:13;
A452: len (F . k) in dom (F . k) by A441, A446, FINSEQ_3:27;
A453: i2 + 1 > i2 by NAT_1:13;
A454: j2 + 1 > j2 by NAT_1:13;
A455: ((len (F . k)) -' 1) + 1 = len (F . k) by A441, A446, XREAL_1:237;
then A456: ((len (F . k)) -' 1) + (1 + 1) = (len (F . k)) + 1 ;
A457: left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C by A439, A447, A455;

hereby :: thesis:

assume that
A458: front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) misses C and
A459: front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) misses C ; :: thesis:
consider i, j being Element of NAT such that
A460: (F . k) ^ <*((Gauge C,n) * i,j)*> turns_left (len (F . k)) -' 1, Gauge C,n and
A461: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A156, A441, A450, A446, A457, A458, A459;
thus F . (k + 1) turns_left (len (F . k)) -' 1, Gauge C,n by A460, A461; :: thesis:
A462: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge C,n) * i,j by A461, FINSEQ_4:82;
A463: (F . (k + 1)) /. (len (F . k)) = (Gauge C,n) * i2,j2 by A445, A452, A461, FINSEQ_4:83;
A464: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 by A443, A448, A461, 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 A442, A444, A455, A456, A451, A454, A460, A461, A463, A462, 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 A442, A444, A455, A456, A449, A453, A460, A461, A464, A463, A462, 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 A442, A444, A455, A456, A449, A453, A460, A461, A464, A463, A462, 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 A442, A444, A455, A456, A451, A454, A460, A461, A464, A463, A462, GOBRD13:def 7; :: thesis:

end;

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

proof

let m be Element of NAT ; :: thesis:
assume m <= 0 ; :: thesis:
then 0 = m ;
hence (F . 0 ) | m = F . m by A155; :: 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)) ) );
A466: S₁[ 0 ,F . 0 ,F . (0 + 1)] by A156;
A467: 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 & front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) misses C & front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C holds
( 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))*> ) ) )

proof

let k, i1, i2, j1, j2 be Element of NAT ; :: thesis:
assume that
A468: k > 1 and
A469: [i1,j1] in Indices (Gauge C,n) and
A470: (F . k) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 and
A471: [i2,j2] in Indices (Gauge C,n) and
A472: (F . k) /. (len (F . k)) = (Gauge C,n) * i2,j2 ; :: thesis:
A473: len (F . k) = k by A176;
then A474: 1 <= (len (F . k)) -' 1 by A468, NAT_D:49;
(len (F . k)) -' 1 <= len (F . k) by NAT_D:35;
then A475: (len (F . k)) -' 1 in dom (F . k) by A474, FINSEQ_3:27;
A476: i1 + 1 > i1 by NAT_1:13;
A477: F . k is_sequence_on Gauge C,n by A439;
A478: j1 + 1 > j1 by NAT_1:13;
A479: len (F . k) in dom (F . k) by A468, A473, FINSEQ_3:27;
A480: i2 + 1 > i2 by NAT_1:13;
A481: j2 + 1 > j2 by NAT_1:13;
A482: ((len (F . k)) -' 1) + 1 = len (F . k) by A468, A473, XREAL_1:237;
then A483: ((len (F . k)) -' 1) + (1 + 1) = (len (F . k)) + 1 ;
A484: left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C by A439, A474, A482;

hereby :: thesis:

assume that
A485: front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) misses C and
A486: front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C ; :: thesis:
consider i, j being Element of NAT such that
A487: (F . k) ^ <*((Gauge C,n) * i,j)*> goes_straight (len (F . k)) -' 1, Gauge C,n and
A488: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A156, A468, A477, A473, A484, A485, A486;
thus F . (k + 1) goes_straight (len (F . k)) -' 1, Gauge C,n by A487, A488; :: thesis:
A489: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge C,n) * i,j by A488, FINSEQ_4:82;
A490: (F . (k + 1)) /. (len (F . k)) = (Gauge C,n) * i2,j2 by A472, A479, A488, FINSEQ_4:83;
A491: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 by A470, A475, A488, 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 A469, A471, A482, A483, A478, A481, A487, A488, A490, A489, 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 A469, A471, A482, A483, A476, A480, A487, A488, A491, A490, A489, 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 A469, A471, A482, A483, A476, A480, A487, A488, A491, A490, A489, 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 A469, A471, A482, A483, A478, A481, A487, A488, A491, A490, A489, GOBRD13:def 8; :: thesis:

end;

A492: 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 & front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C holds
( 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)*> ) ) )

proof

let k, i1, i2, j1, j2 be Element of NAT ; :: thesis:
assume that
A493: k > 1 and
A494: [i1,j1] in Indices (Gauge C,n) and
A495: (F . k) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 and
A496: [i2,j2] in Indices (Gauge C,n) and
A497: (F . k) /. (len (F . k)) = (Gauge C,n) * i2,j2 ; :: thesis:
A498: len (F . k) = k by A176;
then A499: ((len (F . k)) -' 1) + 1 = len (F . k) by A493, XREAL_1:237;
then A500: ((len (F . k)) -' 1) + (1 + 1) = (len (F . k)) + 1 ;
A501: F . k is_sequence_on Gauge C,n by A439;
assume A502: front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C ; :: thesis:
A503: 1 <= (len (F . k)) -' 1 by A493, A498, NAT_D:49;
then left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C by A439, A499;
then consider i, j being Element of NAT such that
A504: (F . k) ^ <*((Gauge C,n) * i,j)*> turns_right (len (F . k)) -' 1, Gauge C,n and
A505: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i,j)*> by A156, A493, A501, A498, A502;
len (F . k) in dom (F . k) by A493, A498, FINSEQ_3:27;
then A506: (F . (k + 1)) /. (len (F . k)) = (Gauge C,n) * i2,j2 by A497, A505, FINSEQ_4:83;
(len (F . k)) -' 1 <= len (F . k) by NAT_D:35;
then (len (F . k)) -' 1 in dom (F . k) by A503, FINSEQ_3:27;
then A507: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 by A495, A505, FINSEQ_4:83;
thus F . (k + 1) turns_right (len (F . k)) -' 1, Gauge C,n by A504, A505; :: thesis:
A508: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge C,n) * i,j by A505, FINSEQ_4:82;
A509: j2 + 1 > j2 by NAT_1:13;
A510: i2 + 1 > i2 by NAT_1:13;
A511: j1 + 1 > j1 by NAT_1:13;
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 A494, A496, A499, A500, A509, A504, A505, A507, A506, A508, GOBRD13:def 6; :: thesis:
A512: i1 + 1 > i1 by NAT_1:13;
hence ( 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 A494, A496, A499, A500, A510, A504, A505, A507, A506, A508, 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 A494, A496, A499, A500, A512, A510, A504, A505, A507, A506, A508, 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 A494, A496, A499, A500, A511, A509, A504, A505, A507, A506, A508, GOBRD13:def 6; :: thesis:

end;

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

proof

let k be Element of NAT ; :: thesis:
assume A514: k > 1 ; :: thesis:
A515: F . k is_sequence_on Gauge C,n by A439;
A516: len (F . k) = k by A176;
then A517: ((len (F . k)) -' 1) + 1 = len (F . k) by A514, XREAL_1:237;
1 <= (len (F . k)) -' 1 by A514, A516, NAT_D:49;
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 A515, A517, JORDAN8:6;
hence ( ( front_right_cell (F . k),(k -' 1),(Gauge C,n) misses C & front_left_cell (F . k),(k -' 1),(Gauge C,n) misses C implies F . (k + 1) turns_left k -' 1, Gauge C,n ) & ( front_right_cell (F . k),(k -' 1),(Gauge C,n) misses C & front_left_cell (F . k),(k -' 1),(Gauge C,n) meets C implies F . (k + 1) goes_straight k -' 1, Gauge C,n ) & ( front_right_cell (F . k),(k -' 1),(Gauge C,n) meets C implies F . (k + 1) turns_right k -' 1, Gauge C,n ) ) by A440, A467, A492, A514, A516; :: thesis:

end;

A518: S₁[1,F . 1,F . (1 + 1)] by A156;
A519: 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:
A520: F . k is_sequence_on Gauge C,n by A439;
A521: len (F . k) = k by A176;

per cases by XXREAL_0:1;

suppose A522: k < 1 ; :: thesis:

take X-SpanStart C,n ; :: thesis:
take Y-SpanStart C,n ; :: thesis:
thus [(X-SpanStart C,n),(Y-SpanStart C,n)] in Indices (Gauge C,n) by A1, JORDAN11:8; :: thesis:
k = 0 by A522, NAT_1:14;
hence F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n))*> by A155, A466, FINSEQ_1:47; :: thesis:

end;

suppose A523: k = 1 ; :: thesis:

take (X-SpanStart C,n) -' 1 ; :: thesis:
take Y-SpanStart C,n ; :: thesis:
thus [((X-SpanStart C,n) -' 1),(Y-SpanStart C,n)] in Indices (Gauge C,n) by A1, JORDAN11:9; :: thesis:
thus F . (k + 1) = (F . k) ^ <*((Gauge C,n) * ((X-SpanStart C,n) -' 1),(Y-SpanStart C,n))*> by A466, A518, A523, FINSEQ_1:def 9; :: thesis:

end;

suppose A524: k > 1 ; :: thesis:

then A525: ((len (F . k)) -' 1) + 1 = len (F . k) by A521, XREAL_1:237;
1 <= (len (F . k)) -' 1 by A521, A524, NAT_D:49;
then consider i1, j1, i2, j2 being Element of NAT such that
A526: [i1,j1] in Indices (Gauge C,n) and
A527: (F . k) /. ((len (F . k)) -' 1) = (Gauge C,n) * i1,j1 and
A528: [i2,j2] in Indices (Gauge C,n) and
A529: (F . k) /. (len (F . k)) = (Gauge C,n) * i2,j2 and
A530: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A520, A525, JORDAN8:6;

now

per cases ;

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

now

per cases by A530;

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

then A533: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 -' 1),j2)*> by A440, A524, A526, A527, A528, A529, A531;
[(i2 -' 1),j2] in Indices (Gauge C,n) by A440, A524, A526, A527, A528, A529, A531, A532;
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)*> ) by A533; :: thesis:

end;

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

then A535: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 + 1))*> by A440, A524, A526, A527, A528, A529, A531;
[i2,(j2 + 1)] in Indices (Gauge C,n) by A440, A524, A526, A527, A528, A529, A531, A534;
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)*> ) by A535; :: thesis:

end;

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

then A537: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 -' 1))*> by A440, A524, A526, A527, A528, A529, A531;
[i2,(j2 -' 1)] in Indices (Gauge C,n) by A440, A524, A526, A527, A528, A529, A531, A536;
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)*> ) by A537; :: thesis:

end;

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

then A539: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 + 1),j2)*> by A440, A524, A526, A527, A528, A529, A531;
[(i2 + 1),j2] in Indices (Gauge C,n) by A440, A524, A526, A527, A528, A529, A531, A538;
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)*> ) by A539; :: 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 A540: ( front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) misses C & front_left_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C ) ; :: thesis:

now

per cases by A530;

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

then A542: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 + 1))*> by A467, A524, A526, A527, A528, A529, A540;
[i2,(j2 + 1)] in Indices (Gauge C,n) by A467, A524, A526, A527, A528, A529, A540, A541;
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)*> ) by A542; :: thesis:

end;

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

then A544: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 + 1),j2)*> by A467, A524, A526, A527, A528, A529, A540;
[(i2 + 1),j2] in Indices (Gauge C,n) by A467, A524, A526, A527, A528, A529, A540, A543;
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)*> ) by A544; :: thesis:

end;

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

then A546: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 -' 1),j2)*> by A467, A524, A526, A527, A528, A529, A540;
[(i2 -' 1),j2] in Indices (Gauge C,n) by A467, A524, A526, A527, A528, A529, A540, A545;
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)*> ) by A546; :: thesis:

end;

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

then A548: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 -' 1))*> by A467, A524, A526, A527, A528, A529, A540;
[i2,(j2 -' 1)] in Indices (Gauge C,n) by A467, A524, A526, A527, A528, A529, A540, A547;
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)*> ) by A548; :: 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 A549: front_right_cell (F . k),((len (F . k)) -' 1),(Gauge C,n) meets C ; :: thesis:

now

per cases by A530;

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

then A551: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 + 1),j2)*> by A492, A524, A526, A527, A528, A529, A549;
[(i2 + 1),j2] in Indices (Gauge C,n) by A492, A524, A526, A527, A528, A529, A549, A550;
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)*> ) by A551; :: thesis:

end;

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

then A553: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 -' 1))*> by A492, A524, A526, A527, A528, A529, A549;
[i2,(j2 -' 1)] in Indices (Gauge C,n) by A492, A524, A526, A527, A528, A529, A549, A552;
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)*> ) by A553; :: thesis:

end;

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

then A555: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 + 1))*> by A492, A524, A526, A527, A528, A529, A549;
[i2,(j2 + 1)] in Indices (Gauge C,n) by A492, A524, A526, A527, A528, A529, A549, A554;
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)*> ) by A555; :: thesis:

end;

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

then A557: F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 -' 1),j2)*> by A492, A524, A526, A527, A528, A529, A549;
[(i2 -' 1),j2] in Indices (Gauge C,n) by A492, A524, A526, A527, A528, A529, A549, A556;
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)*> ) by A557; :: 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;

A558: for k being Element of NAT st S₅[k] holds
S₅[k + 1]

proof

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

per cases by A560, XXREAL_0:1;

suppose m < k + 1 ; :: thesis:

then A561: m <= k by NAT_1:13;
A562: 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 A519;
len (F . k) = k by A176;
then (F . (k + 1)) | m = (F . k) | m by A561, A562, FINSEQ_5:25;
hence (F . (k + 1)) | m = F . m by A559, A561; :: thesis:

end;

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

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

end;

A564: for k being Element of NAT holds S₅[k] from NAT_1:sch 1(A465, A558);
A565: 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
A566: 1 <= j and
A567: j <= k ; :: thesis:
j <= len (F . k) by A176, A567;
then len ((F . k) | j) = j by FINSEQ_1:80;
then A568: j in dom ((F . k) | j) by A566, FINSEQ_3:27;
(F . k) | j = F . j by A564, A567;
hence (F . k) /. j = (F . j) /. j by A568, FINSEQ_4:85; :: thesis:

end;

defpred S₇[ Element of NAT ] means F . $1 is unfolded ;
A569: for k being Element of NAT st S₇[k] holds
S₇[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A570: F . k is unfolded ; :: thesis:
A571: F . k is_sequence_on Gauge C,n by A439;

per cases ;

suppose k <= 1 ; :: thesis:

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

end;

suppose A572: k > 1 ; :: thesis:

set m = k -' 1;
A573: (k -' 1) + 1 = k by A572, XREAL_1:237;
A574: len (F . k) = k by A176;
A575: 1 <= k -' 1 by A572, NAT_D:49;
then consider i1, j1, i2, j2 being Element of NAT such that
A576: [i1,j1] in Indices (Gauge C,n) and
A577: (F . k) /. (k -' 1) = (Gauge C,n) * i1,j1 and
A578: [i2,j2] in Indices (Gauge C,n) and
A579: (F . k) /. (len (F . k)) = (Gauge C,n) * i2,j2 and
A580: ( ( 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, A573, A574, JORDAN8:6;
A581: LSeg (F . k),(k -' 1) = LSeg ((Gauge C,n) * i1,j1),((Gauge C,n) * i2,j2) by A575, A573, A574, A577, A579, TOPREAL1:def 5;
A582: 1 <= j2 by A578, MATRIX_1:39;
then A583: (j2 -' 1) + 1 = j2 by XREAL_1:237;
A584: 1 <= j1 by A576, MATRIX_1:39;
A585: 1 <= i2 by A578, MATRIX_1:39;
then A586: (i2 -' 1) + 1 = i2 by XREAL_1:237;
A587: i1 <= len (Gauge C,n) by A576, MATRIX_1:39;
A588: j2 <= width (Gauge C,n) by A578, MATRIX_1:39;
A589: 1 <= i1 by A576, MATRIX_1:39;
A590: j1 <= width (Gauge C,n) by A576, MATRIX_1:39;
A591: i2 <= len (Gauge C,n) by A578, MATRIX_1:39;

now

per cases ;

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

now

per cases by A580;

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

then [(i2 -' 1),j2] in Indices (Gauge C,n) by A440, A572, A574, A576, A577, A578, A579, A592;
then 1 <= i2 -' 1 by MATRIX_1:39;
then A594: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * (i2 -' 1),j2)) = {((F . k) /. (len (F . k)))} by A579, A587, A584, A588, A586, A581, A593, GOBOARD7:18;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 -' 1),j2)*> by A440, A572, A574, A576, A577, A578, A579, A592, A593;
hence S₇[k + 1] by A570, A573, A574, A594, SPPOL_2:31; :: thesis:

end;

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

then [i2,(j2 + 1)] in Indices (Gauge C,n) by A440, A572, A574, A576, A577, A578, A579, A592;
then j2 + 1 <= width (Gauge C,n) by MATRIX_1:39;
then A596: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * i2,(j2 + 1))) = {((F . k) /. (len (F . k)))} by A579, A589, A584, A591, A581, A595, GOBOARD7:20;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 + 1))*> by A440, A572, A574, A576, A577, A578, A579, A592, A595;
hence S₇[k + 1] by A570, A573, A574, A596, SPPOL_2:31; :: thesis:

end;

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

then [i2,(j2 -' 1)] in Indices (Gauge C,n) by A440, A572, A574, A576, A577, A578, A579, A592;
then 1 <= j2 -' 1 by MATRIX_1:39;
then A598: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * i2,(j2 -' 1))) = {((F . k) /. (len (F . k)))} by A579, A587, A590, A585, A583, A581, A597, GOBOARD7:17;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 -' 1))*> by A440, A572, A574, A576, A577, A578, A579, A592, A597;
hence S₇[k + 1] by A570, A573, A574, A598, SPPOL_2:31; :: thesis:

end;

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

then [(i2 + 1),j2] in Indices (Gauge C,n) by A440, A572, A574, A576, A577, A578, A579, A592;
then i2 + 1 <= len (Gauge C,n) by MATRIX_1:39;
then A600: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * (i2 + 1),j2)) = {((F . k) /. (len (F . k)))} by A579, A589, A590, A582, A581, A599, GOBOARD7:19;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 + 1),j2)*> by A440, A572, A574, A576, A577, A578, A579, A592, A599;
hence S₇[k + 1] by A570, A573, A574, A600, SPPOL_2:31; :: thesis:

end;

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

end;

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

now

per cases by A580;

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

then [i2,(j2 + 1)] in Indices (Gauge C,n) by A467, A572, A574, A576, A577, A578, A579, A601;
then A603: j2 + 1 <= width (Gauge C,n) by MATRIX_1:39;
j2 + 1 = j1 + (1 + 1) by A602;
then A604: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * i2,(j2 + 1))) = {((F . k) /. (len (F . k)))} by A579, A589, A587, A584, A581, A602, A603, GOBOARD7:15;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 + 1))*> by A467, A572, A574, A576, A577, A578, A579, A601, A602;
hence S₇[k + 1] by A570, A573, A574, A604, SPPOL_2:31; :: thesis:

end;

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

then [(i2 + 1),j2] in Indices (Gauge C,n) by A467, A572, A574, A576, A577, A578, A579, A601;
then A606: i2 + 1 <= len (Gauge C,n) by MATRIX_1:39;
i2 + 1 = i1 + (1 + 1) by A605;
then A607: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * (i2 + 1),j2)) = {((F . k) /. (len (F . k)))} by A579, A589, A584, A590, A581, A605, A606, GOBOARD7:16;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 + 1),j2)*> by A467, A572, A574, A576, A577, A578, A579, A601, A605;
hence S₇[k + 1] by A570, A573, A574, A607, SPPOL_2:31; :: thesis:

end;

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

then [(i2 -' 1),j2] in Indices (Gauge C,n) by A467, A572, A574, A576, A577, A578, A579, A601;
then A609: 1 <= i2 -' 1 by MATRIX_1:39;
((i2 -' 1) + 1) + 1 = (i2 -' 1) + (1 + 1) ;
then A610: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * (i2 -' 1),j2)) = {((F . k) /. (len (F . k)))} by A579, A587, A584, A590, A586, A581, A608, A609, GOBOARD7:16;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 -' 1),j2)*> by A467, A572, A574, A576, A577, A578, A579, A601, A608;
hence S₇[k + 1] by A570, A573, A574, A610, SPPOL_2:31; :: thesis:

end;

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

then [i2,(j2 -' 1)] in Indices (Gauge C,n) by A467, A572, A574, A576, A577, A578, A579, A601;
then A612: 1 <= j2 -' 1 by MATRIX_1:39;
((j2 -' 1) + 1) + 1 = (j2 -' 1) + (1 + 1) ;
then A613: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * i2,(j2 -' 1))) = {((F . k) /. (len (F . k)))} by A579, A589, A587, A590, A583, A581, A611, A612, GOBOARD7:15;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 -' 1))*> by A467, A572, A574, A576, A577, A578, A579, A601, A611;
hence S₇[k + 1] by A570, A573, A574, A613, SPPOL_2:31; :: thesis:

end;

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

end;

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

now

per cases by A580;

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

then [(i2 + 1),j2] in Indices (Gauge C,n) by A492, A572, A574, A576, A577, A578, A579, A614;
then i2 + 1 <= len (Gauge C,n) by MATRIX_1:39;
then A616: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * (i2 + 1),j2)) = {((F . k) /. (len (F . k)))} by A579, A589, A584, A588, A581, A615, GOBOARD7:17;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 + 1),j2)*> by A492, A572, A574, A576, A577, A578, A579, A614, A615;
hence S₇[k + 1] by A570, A573, A574, A616, SPPOL_2:31; :: thesis:

end;

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

then [i2,(j2 -' 1)] in Indices (Gauge C,n) by A492, A572, A574, A576, A577, A578, A579, A614;
then 1 <= j2 -' 1 by MATRIX_1:39;
then A618: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * i2,(j2 -' 1))) = {((F . k) /. (len (F . k)))} by A579, A589, A590, A591, A583, A581, A617, GOBOARD7:18;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 -' 1))*> by A492, A572, A574, A576, A577, A578, A579, A614, A617;
hence S₇[k + 1] by A570, A573, A574, A618, SPPOL_2:31; :: thesis:

end;

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

then [i2,(j2 + 1)] in Indices (Gauge C,n) by A492, A572, A574, A576, A577, A578, A579, A614;
then j2 + 1 <= width (Gauge C,n) by MATRIX_1:39;
then A620: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * i2,(j2 + 1))) = {((F . k) /. (len (F . k)))} by A579, A587, A584, A585, A581, A619, GOBOARD7:19;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * i2,(j2 + 1))*> by A492, A572, A574, A576, A577, A578, A579, A614, A619;
hence S₇[k + 1] by A570, A573, A574, A620, SPPOL_2:31; :: thesis:

end;

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

then [(i2 -' 1),j2] in Indices (Gauge C,n) by A492, A572, A574, A576, A577, A578, A579, A614;
then 1 <= i2 -' 1 by MATRIX_1:39;
then A622: (LSeg (F . k),(k -' 1)) /\ (LSeg ((F . k) /. (len (F . k))),((Gauge C,n) * (i2 -' 1),j2)) = {((F . k) /. (len (F . k)))} by A579, A587, A590, A582, A586, A581, A621, GOBOARD7:20;
F . (k + 1) = (F . k) ^ <*((Gauge C,n) * (i2 -' 1),j2)*> by A492, A572, A574, A576, A577, A578, A579, A614, A621;
hence S₇[k + 1] by A570, A573, A574, A622, 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 A623: 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:
A624: for k being Element of NAT st S₈[k] holds
S₈[k + 1]

proof

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

now

let n, m be Element of NAT ; :: thesis:
assume that
A626: n in dom (F . (k + 1)) and
A627: m in dom (F . (k + 1)) and
A628: (F . (k + 1)) /. n = (F . (k + 1)) /. m ; :: thesis:
A629: 1 <= n by A626, FINSEQ_3:27;
A630: m <= len (F . (k + 1)) by A627, FINSEQ_3:27;
A631: 1 <= m by A627, FINSEQ_3:27;
A632: n <= len (F . (k + 1)) by A626, FINSEQ_3:27;
A633: 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 A519;
A634: len (F . k) = k by A176;
A635: len (F . (k + 1)) = k + 1 by A176;

per cases by A632, A630, A635, NAT_1:8;

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

then A637: m in dom (F . k) by A631, A634, FINSEQ_3:27;
then A638: (F . (k + 1)) /. m = (F . k) /. m by A633, FINSEQ_4:83;
A639: n in dom (F . k) by A629, A634, A636, FINSEQ_3:27;
then (F . (k + 1)) /. n = (F . k) /. n by A633, FINSEQ_4:83;
hence n = m by A625, A628, A639, A637, A638, PARTFUN2:17; :: thesis:

end;

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

hence n = m by A623, A627, A628, A635, NAT_1:12; :: thesis:

end;

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

hence n = m by A623, A626, A628, A635, 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;

A640: S₈[ 0 ] by A155;
A641: for k being Element of NAT holds S₈[k] from NAT_1:sch 1(A640, A624);
A642: 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 A641;
hence card (rng (F . k)) = len (F . k) by FINSEQ_4:77
.= k by A176 ;
:: thesis:

end;

reconsider k = ((len (Gauge C,n)) * (width (Gauge C,n))) + 1 as Element of NAT ;
A643: k > (len (Gauge C,n)) * (width (Gauge C,n)) by NAT_1:13;
F . k is_sequence_on Gauge C,n by A439;
then A644: card (rng (F . k)) <= card (Values (Gauge C,n)) by GOBRD13:9, NAT_1:44;
card (Values (Gauge C,n)) <= (len (Gauge C,n)) * (width (Gauge C,n)) by GOBRD13:8;
then card (rng (F . k)) <= (len (Gauge C,n)) * (width (Gauge C,n)) by A644, XXREAL_0:2;
hence contradiction by A642, A643; :: thesis:

end;

then A645: ex k being Nat st S₆[k] ;
consider k being Nat such that
A646: S₆[k] and
A647: for l being Nat st S₆[l] holds
k <= l from NAT_1:sch 5(A645);
reconsider k = k as Element of NAT by ORDINAL1:def 13;
consider m being Element of NAT such that
A648: m in dom (F . k) and
A649: m <> len (F . k) and
A650: (F . k) /. m = (F . k) /. (len (F . k)) by A646;
A651: 1 <= m by A648, FINSEQ_3:27;
reconsider f = F . k as non empty FinSequence of (TOP-REAL 2) by A646;
A652: f is_sequence_on Gauge C,n by A439;
A653: m <= len f by A648, FINSEQ_3:27;
then A654: m < len f by A649, XXREAL_0:1;
then 1 < len f by A651, XXREAL_0:2;
then A655: len f >= 1 + 1 by NAT_1:13;
then A656: k >= 2 by A176;
A657: S₇[ 0 ] by A155, CARD_1:47, SPPOL_2:27;
for k being Element of NAT holds S₇[k] from NAT_1:sch 1(A657, A569);
then reconsider f = f as non constant non empty special unfolded FinSequence of (TOP-REAL 2) by A652, A655, JORDAN8:7, JORDAN8:8;
set g = f /^ (m -' 1);
A658: m + 1 <= len f by A654, NAT_1:13;
A659: 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

proof

left_cell f,n,(Gauge C,n) meets C by A439, A662, A663;
then consider p being set such that
A673: p in left_cell f,n,(Gauge C,n) and
A674: p in C by XBOOLE_0:3;
reconsider p = p as Element of (TOP-REAL 2) by A673;

now

take p = p; :: thesis:

now

assume p in L~ h ; :: thesis:
then consider j being Element of NAT such that
A675: 1 <= j and
A676: j + 1 <= len f and
A677: p in LSeg f,j by A660, SPPOL_2:13;
p in (right_cell f,j,(Gauge C,n)) /\ (left_cell f,j,(Gauge C,n)) by A439, A675, A676, A677, GOBRD13:30;
then A678: p in right_cell f,j,(Gauge C,n) by XBOOLE_0:def 4;
right_cell f,j,(Gauge C,n) misses C by A439, A675, A676;
hence contradiction by A674, A678, XBOOLE_0:3; :: thesis:

end;

hence p in rc by A673, XBOOLE_0:def 5; :: thesis:
thus p in C by A674; :: thesis:

end;

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

end;

Int (left_cell f,n,(Gauge C,n)) is connected by A652, A662, A663, JORDAN9:12;
then rc is connected by A668, A670, A666, A671, CONNSP_1:19, XBOOLE_1:19;
then rc c= Comp by A661, A667, A669, GOBOARD9:6;
hence C meets Comp by A672, XBOOLE_1:63; :: thesis:

end;

A679: for i being Element of NAT st 1 <= i & i + 1 <= len f holds
left_cell f,i,(Gauge C,n) = Cl (Int (left_cell f,i,(Gauge C,n)))

proof

let i be Element of NAT ; :: thesis:
assume that
A680: 1 <= i and
A681: i + 1 <= len f ; :: thesis:
consider i1, j1, i2, j2 being Element of NAT such that
A682: [i1,j1] in Indices (Gauge C,n) and
A683: f /. i = (Gauge C,n) * i1,j1 and
A684: [i2,j2] in Indices (Gauge C,n) and
A685: f /. (i + 1) = (Gauge C,n) * i2,j2 and
A686: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A652, A680, A681, JORDAN8:6;
A687: i1 <= len (Gauge C,n) by A682, MATRIX_1:39;
A688: i2 <= len (Gauge C,n) by A684, MATRIX_1:39;
A689: i1 + 1 > i1 by NAT_1:13;
A690: j1 <= width (Gauge C,n) by A682, MATRIX_1:39;
A691: j1 + 1 > j1 by NAT_1:13;
A692: j2 <= width (Gauge C,n) by A684, MATRIX_1:39;
A693: i2 + 1 > i2 by NAT_1:13;
A694: j2 + 1 > j2 by NAT_1:13;

per cases by A686;

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

A696: i1 -' 1 <= len (Gauge C,n) by A687, NAT_D:44;
left_cell f,i,(Gauge C,n) = cell (Gauge C,n),(i1 -' 1),j1 by A652, A680, A681, A682, A683, A684, A685, A691, A694, A695, GOBRD13:def 3;
hence left_cell f,i,(Gauge C,n) = Cl (Int (left_cell f,i,(Gauge C,n))) by A690, A696, GOBRD11:35; :: thesis:

end;

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

then left_cell f,i,(Gauge C,n) = cell (Gauge C,n),i1,j1 by A652, A680, A681, A682, A683, A684, A685, A689, A693, GOBRD13:def 3;
hence left_cell f,i,(Gauge C,n) = Cl (Int (left_cell f,i,(Gauge C,n))) by A687, A690, GOBRD11:35; :: thesis:

end;

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

A698: j2 -' 1 <= width (Gauge C,n) by A692, NAT_D:44;
left_cell f,i,(Gauge C,n) = cell (Gauge C,n),i2,(j2 -' 1) by A652, A680, A681, A682, A683, A684, A685, A689, A693, A697, GOBRD13:def 3;
hence left_cell f,i,(Gauge C,n) = Cl (Int (left_cell f,i,(Gauge C,n))) by A688, A698, GOBRD11:35; :: thesis:

end;

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

then left_cell f,i,(Gauge C,n) = cell (Gauge C,n),i1,j2 by A652, A680, A681, A682, A683, A684, A685, A691, A694, GOBRD13:def 3;
hence left_cell f,i,(Gauge C,n) = Cl (Int (left_cell f,i,(Gauge C,n))) by A687, A692, GOBRD11:35; :: thesis:

end;

m -' 1 <= m by NAT_D:44;
then m -' 1 < m + 1 by NAT_1:13;
then A699: m -' 1 < len f by A658, XXREAL_0:2;
then A700: len (f /^ (m -' 1)) = (len f) - (m -' 1) by RFINSEQ:def 2;
then (m -' 1) - (m -' 1) < len (f /^ (m -' 1)) by A699, 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 A701: g /. (len g) = f /. ((m -' 1) + (len g)) by FINSEQ_5:30
.= f /. (len f) by A700 ;
(m + 1) - (m -' 1) <= len g by A658, A700, XREAL_1:11;
then A702: (m + 1) - (m - 1) <= len g by A651, XREAL_1:235;
then A703: ((1 + m) - m) + 1 <= len g ;
A704: g is_sequence_on Gauge C,n by A439, JORDAN8:5;
then A705: g is standard by JORDAN8:7;
A706: not g is constant

proof

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

end;

A709: len (F . k) = k by A176;
A710: 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
A711: 1 <= i and
A712: i < len g and
A713: 1 <= j and
A714: j < len g and
A715: g /. i = g /. j and
A716: i <> j ; :: thesis:
A717: i in dom g by A711, A712, FINSEQ_3:27;
then A718: g /. i = f /. ((m -' 1) + i) by FINSEQ_5:30;
A719: j in dom g by A713, A714, FINSEQ_3:27;
then A720: g /. j = f /. ((m -' 1) + j) by FINSEQ_5:30;

per cases by A716, XXREAL_0:1;

suppose A721: i < j ; :: thesis:

set l = (m -' 1) + j;
set m9 = (m -' 1) + i;
A722: (m -' 1) + i < (m -' 1) + j by A721, XREAL_1:8;
A723: len (F . ((m -' 1) + j)) = (m -' 1) + j by A176;
A724: (m -' 1) + j < k by A709, A700, A714, XREAL_1:22;
then A725: f | ((m -' 1) + j) = F . ((m -' 1) + j) by A564;
0 + j <= (m -' 1) + j by XREAL_1:8;
then A726: 1 <= (m -' 1) + j by A713, XXREAL_0:2;
then (m -' 1) + j in dom (F . ((m -' 1) + j)) by A723, FINSEQ_3:27;
then A727: (F . ((m -' 1) + j)) /. ((m -' 1) + j) = f /. ((m -' 1) + j) by A725, FINSEQ_4:85;
0 + i <= (m -' 1) + i by XREAL_1:8;
then 1 <= (m -' 1) + i by A711, XXREAL_0:2;
then A728: (m -' 1) + i in dom (F . ((m -' 1) + j)) by A722, A723, FINSEQ_3:27;
then (F . ((m -' 1) + j)) /. ((m -' 1) + i) = f /. ((m -' 1) + i) by A725, FINSEQ_4:85;
hence contradiction by A647, A715, A718, A719, A722, A724, A726, A723, A728, A727, FINSEQ_5:30; :: thesis:

end;

suppose A729: j < i ; :: thesis:

set l = (m -' 1) + i;
set m9 = (m -' 1) + j;
A730: (m -' 1) + j < (m -' 1) + i by A729, XREAL_1:8;
A731: len (F . ((m -' 1) + i)) = (m -' 1) + i by A176;
A732: (m -' 1) + i < k by A709, A700, A712, XREAL_1:22;
then A733: f | ((m -' 1) + i) = F . ((m -' 1) + i) by A564;
0 + i <= (m -' 1) + i by XREAL_1:8;
then A734: 1 <= (m -' 1) + i by A711, XXREAL_0:2;
then (m -' 1) + i in dom (F . ((m -' 1) + i)) by A731, FINSEQ_3:27;
then A735: (F . ((m -' 1) + i)) /. ((m -' 1) + i) = f /. ((m -' 1) + i) by A733, FINSEQ_4:85;
0 + j <= (m -' 1) + j by XREAL_1:8;
then 1 <= (m -' 1) + j by A713, XXREAL_0:2;
then A736: (m -' 1) + j in dom (F . ((m -' 1) + i)) by A730, A731, FINSEQ_3:27;
then (F . ((m -' 1) + i)) /. ((m -' 1) + j) = f /. ((m -' 1) + j) by A733, FINSEQ_4:85;
hence contradiction by A647, A715, A717, A720, A730, A732, A734, A731, A736, A735, FINSEQ_5:30; :: thesis:

end;

1 in dom g by FINSEQ_5:6;
then A737: g /. 1 = f /. ((m -' 1) + 1) by FINSEQ_5:30
.= f /. m by A651, XREAL_1:237 ;
A738: 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
A739: 1 < i and
A740: i < j and
A741: j <= len g and
A742: g /. i = g /. j ; :: thesis:
A743: 1 < j by A739, A740, XXREAL_0:2;
A744: i < len g by A740, A741, XXREAL_0:2;
then A745: 1 < len g by A739, XXREAL_0:2;

per cases ;

suppose j <> len g ; :: thesis:

then j < len g by A741, XXREAL_0:1;
hence contradiction by A710, A739, A740, A742, A743, A744; :: thesis:

end;

suppose j = len g ; :: thesis:

hence contradiction by A650, A737, A701, A710, A739, A740, A742, A745; :: thesis:

end;

A746: 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
A747: 1 <= i and
A748: i < j and
A749: j < len g and
A750: g /. i = g /. j ; :: thesis:
A751: i < len g by A748, A749, XXREAL_0:2;
1 < j by A747, A748, XXREAL_0:2;
hence contradiction by A710, A747, A748, A749, A750, A751; :: 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
A752: i + 1 < j and
A753: ( ( i > 1 & j < len g ) or j + 1 < len g ) ; :: thesis:
A754: 1 < j by A752, NAT_1:12;
A755: 1 <= i + 1 by NAT_1:12;
A756: j <= j + 1 by NAT_1:12;
then A757: i + 1 < j + 1 by A752, XXREAL_0:2;
i < j by A752, NAT_1:13;
then A758: i < j + 1 by A756, XXREAL_0:2;

per cases by A753, NAT_1:14;

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

then A760: i + 1 < len g by A752, XXREAL_0:2;
then A761: LSeg g,i = LSeg (g /. i),(g /. (i + 1)) by A759, TOPREAL1:def 5;
A762: i < len g by A760, NAT_1:13;
consider i1, j1, i2, j2 being Element of NAT such that
A763: [i1,j1] in Indices (Gauge C,n) and
A764: g /. i = (Gauge C,n) * i1,j1 and
A765: [i2,j2] in Indices (Gauge C,n) and
A766: g /. (i + 1) = (Gauge C,n) * i2,j2 and
A767: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A704, A759, A760, JORDAN8:6;
A768: 1 <= i1 by A763, MATRIX_1:39;
A769: j2 <= width (Gauge C,n) by A765, MATRIX_1:39;
A770: 1 <= i2 by A765, MATRIX_1:39;
A771: i1 <= len (Gauge C,n) by A763, MATRIX_1:39;
A772: 1 <= j2 by A765, MATRIX_1:39;
A773: j1 <= width (Gauge C,n) by A763, MATRIX_1:39;
A774: i2 <= len (Gauge C,n) by A765, MATRIX_1:39;
A775: 1 <= j1 by A763, MATRIX_1:39;
A776: 1 < i + 1 by A759, NAT_1:13;
A777: j + 1 <= len g by A759, NAT_1:13;
then A778: LSeg g,j = LSeg (g /. j),(g /. (j + 1)) by A754, TOPREAL1:def 5;
consider i19, j19, i29, j29 being Element of NAT such that
A779: [i19,j19] in Indices (Gauge C,n) and
A780: g /. j = (Gauge C,n) * i19,j19 and
A781: [i29,j29] in Indices (Gauge C,n) and
A782: g /. (j + 1) = (Gauge C,n) * i29,j29 and
A783: ( ( i19 = i29 & j19 + 1 = j29 ) or ( i19 + 1 = i29 & j19 = j29 ) or ( i19 = i29 + 1 & j19 = j29 ) or ( i19 = i29 & j19 = j29 + 1 ) ) by A704, A754, A777, JORDAN8:6;
A784: 1 <= i19 by A779, MATRIX_1:39;
A785: j29 <= width (Gauge C,n) by A781, MATRIX_1:39;
A786: j19 <= width (Gauge C,n) by A779, MATRIX_1:39;
A787: 1 <= j29 by A781, MATRIX_1:39;
A788: 1 <= j19 by A779, MATRIX_1:39;
A789: i29 <= len (Gauge C,n) by A781, MATRIX_1:39;
A790: i19 <= len (Gauge C,n) by A779, MATRIX_1:39;
assume (LSeg g,i) /\ (LSeg g,j) <> {} ; :: according to XBOOLE_0:def 7 :: thesis:
then A791: LSeg g,i meets LSeg g,j by XBOOLE_0:def 7;
A792: 1 <= i29 by A781, MATRIX_1:39;

now

per cases by A767, A783;

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

then A794: i1 = i19 by A761, A764, A766, A768, A771, A775, A769, A778, A780, A782, A784, A790, A788, A785, A791, GOBOARD7:21;

now

per cases by A761, A764, A766, A768, A771, A775, A769, A778, A780, A782, A784, A790, A788, A785, A791, A793, GOBOARD7:24;

suppose j1 = j19 ; :: thesis:

hence contradiction by A710, A752, A756, A754, A759, A762, A764, A780, A794; :: thesis:

end;

suppose j1 = j19 + 1 ; :: thesis:

hence contradiction by A738, A758, A759, A764, A777, A782, A793, A794; :: thesis:

end;

suppose j1 + 1 = j19 ; :: thesis:

hence contradiction by A710, A752, A755, A754, A759, A760, A766, A780, A793, A794; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A761, A764, A766, A768, A771, A775, A769, A778, A780, A782, A784, A788, A786, A789, A791, A795, GOBOARD7:23;

suppose ( i1 = i19 & j1 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A759, A762, A764, A780; :: thesis:

end;

suppose ( i1 = i19 & j1 + 1 = j19 ) ; :: thesis:

hence contradiction by A738, A752, A759, A776, A766, A780, A795; :: thesis:

end;

suppose ( i1 = i19 + 1 & j1 = j19 ) ; :: thesis:

hence contradiction by A738, A758, A759, A764, A777, A782, A795; :: thesis:

end;

suppose ( i1 = i19 + 1 & j1 + 1 = j19 ) ; :: thesis:

hence contradiction by A738, A757, A776, A766, A777, A782, A795; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A761, A764, A766, A768, A771, A775, A769, A778, A780, A782, A790, A788, A786, A792, A791, A796, GOBOARD7:23;

suppose ( i1 = i29 & j19 = j1 ) ; :: thesis:

hence contradiction by A738, A758, A759, A764, A777, A782, A796; :: thesis:

end;

suppose ( i1 = i29 & j1 + 1 = j19 ) ; :: thesis:

hence contradiction by A738, A757, A776, A766, A777, A782, A796; :: thesis:

end;

suppose ( i1 = i29 + 1 & j19 = j1 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A759, A762, A764, A780, A796; :: thesis:

end;

suppose ( i1 = i29 + 1 & j1 + 1 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A755, A754, A759, A760, A766, A780, A796; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A798: i1 = i19 by A761, A764, A766, A768, A771, A775, A769, A778, A780, A782, A784, A790, A786, A787, A791, GOBOARD7:21;

now

per cases by A761, A764, A766, A768, A771, A775, A769, A778, A780, A782, A784, A790, A786, A787, A791, A797, GOBOARD7:24;

suppose j1 = j29 ; :: thesis:

hence contradiction by A710, A752, A755, A754, A759, A760, A766, A780, A797, A798; :: thesis:

end;

suppose j1 = j29 + 1 ; :: thesis:

hence contradiction by A710, A752, A756, A754, A759, A762, A764, A780, A797, A798; :: thesis:

end;

suppose j1 + 1 = j29 ; :: thesis:

hence contradiction by A738, A757, A776, A766, A777, A782, A797, A798; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A761, A764, A766, A768, A775, A773, A774, A778, A780, A782, A784, A790, A788, A785, A791, A799, GOBOARD7:23;

suppose ( i19 = i1 & j1 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A759, A762, A764, A780; :: thesis:

end;

suppose ( i19 = i1 & j19 + 1 = j1 ) ; :: thesis:

hence contradiction by A738, A758, A759, A764, A777, A782, A799; :: thesis:

end;

suppose ( i19 = i1 + 1 & j1 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A755, A754, A759, A760, A766, A780, A799; :: thesis:

end;

suppose ( i19 = i1 + 1 & j19 + 1 = j1 ) ; :: thesis:

hence contradiction by A738, A757, A776, A766, A777, A782, A799; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A801: j1 = j19 by A761, A764, A766, A768, A775, A773, A774, A778, A780, A782, A784, A788, A786, A789, A791, GOBOARD7:22;

now

per cases by A761, A764, A766, A768, A775, A773, A774, A778, A780, A782, A784, A788, A786, A789, A791, A800, GOBOARD7:25;

suppose i1 = i19 ; :: thesis:

hence contradiction by A710, A752, A756, A754, A759, A762, A764, A780, A801; :: thesis:

end;

suppose i1 = i19 + 1 ; :: thesis:

hence contradiction by A738, A758, A759, A764, A777, A782, A800, A801; :: thesis:

end;

suppose i1 + 1 = i19 ; :: thesis:

hence contradiction by A710, A752, A755, A754, A759, A760, A766, A780, A800, A801; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A803: j1 = j19 by A761, A764, A766, A768, A775, A773, A774, A778, A780, A782, A790, A788, A786, A792, A791, GOBOARD7:22;

now

per cases by A761, A764, A766, A768, A775, A773, A774, A778, A780, A782, A790, A788, A786, A792, A791, A802, GOBOARD7:25;

suppose i1 = i29 ; :: thesis:

hence contradiction by A738, A758, A759, A764, A777, A782, A802, A803; :: thesis:

end;

suppose i1 = i29 + 1 ; :: thesis:

hence contradiction by A710, A752, A756, A754, A759, A762, A764, A780, A802, A803; :: thesis:

end;

suppose i1 + 1 = i29 ; :: thesis:

hence contradiction by A738, A757, A776, A766, A777, A782, A802, A803; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A761, A764, A766, A768, A775, A773, A774, A778, A780, A782, A784, A790, A786, A787, A791, A804, GOBOARD7:23;

suppose ( i19 = i1 & j1 = j29 ) ; :: thesis:

hence contradiction by A738, A758, A759, A764, A777, A782, A804; :: thesis:

end;

suppose ( i19 = i1 & j29 + 1 = j1 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A759, A762, A764, A780, A804; :: thesis:

end;

suppose ( i19 = i1 + 1 & j1 = j29 ) ; :: thesis:

hence contradiction by A738, A757, A776, A766, A777, A782, A804; :: thesis:

end;

suppose ( i19 = i1 + 1 & j29 + 1 = j1 ) ; :: thesis:

hence contradiction by A710, A752, A755, A754, A759, A760, A766, A780, A804; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A761, A764, A766, A771, A775, A773, A770, A778, A780, A782, A784, A790, A788, A785, A791, A805, GOBOARD7:23;

suppose ( i19 = i2 & j19 = j1 ) ; :: thesis:

hence contradiction by A710, A752, A755, A754, A759, A760, A766, A780, A805; :: thesis:

end;

suppose ( i19 = i2 & j19 + 1 = j1 ) ; :: thesis:

hence contradiction by A738, A757, A776, A766, A777, A782, A805; :: thesis:

end;

suppose ( i19 = i2 + 1 & j19 = j1 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A759, A762, A764, A780, A805; :: thesis:

end;

suppose ( i19 = i2 + 1 & j19 + 1 = j1 ) ; :: thesis:

hence contradiction by A738, A758, A759, A764, A777, A782, A805; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A807: j1 = j19 by A761, A764, A766, A771, A775, A773, A770, A778, A780, A782, A784, A788, A786, A789, A791, GOBOARD7:22;

now

per cases by A761, A764, A766, A771, A775, A773, A770, A778, A780, A782, A784, A788, A786, A789, A791, A806, GOBOARD7:25;

suppose i2 = i19 ; :: thesis:

hence contradiction by A710, A752, A755, A754, A759, A760, A766, A780, A806, A807; :: thesis:

end;

suppose i2 = i19 + 1 ; :: thesis:

hence contradiction by A738, A757, A776, A766, A777, A782, A806, A807; :: thesis:

end;

suppose i2 + 1 = i19 ; :: thesis:

hence contradiction by A710, A752, A756, A754, A759, A762, A764, A780, A806, A807; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A809: j1 = j19 by A761, A764, A766, A771, A775, A773, A770, A778, A780, A782, A790, A788, A786, A792, A791, GOBOARD7:22;

now

per cases by A761, A764, A766, A771, A775, A773, A770, A778, A780, A782, A790, A788, A786, A792, A791, A808, GOBOARD7:25;

suppose i2 = i29 ; :: thesis:

hence contradiction by A738, A757, A776, A766, A777, A782, A808, A809; :: thesis:

end;

suppose i2 = i29 + 1 ; :: thesis:

hence contradiction by A710, A752, A755, A754, A759, A760, A766, A780, A808, A809; :: thesis:

end;

suppose i2 + 1 = i29 ; :: thesis:

hence contradiction by A738, A758, A759, A764, A777, A782, A808, A809; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A761, A764, A766, A771, A775, A773, A770, A778, A780, A782, A784, A790, A786, A787, A791, A810, GOBOARD7:23;

suppose ( i19 = i2 & j29 = j1 ) ; :: thesis:

hence contradiction by A738, A757, A776, A766, A777, A782, A810; :: thesis:

end;

suppose ( i19 = i2 & j29 + 1 = j1 ) ; :: thesis:

hence contradiction by A710, A752, A755, A754, A759, A760, A766, A780, A810; :: thesis:

end;

suppose ( i19 = i2 + 1 & j29 = j1 ) ; :: thesis:

hence contradiction by A738, A758, A759, A764, A777, A782, A810; :: thesis:

end;

suppose ( i19 = i2 + 1 & j29 + 1 = j1 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A759, A762, A764, A780, A810; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A812: i1 = i19 by A761, A764, A766, A768, A771, A773, A772, A778, A780, A782, A784, A790, A788, A785, A791, GOBOARD7:21;

now

per cases by A761, A764, A766, A768, A771, A773, A772, A778, A780, A782, A784, A790, A788, A785, A791, A811, GOBOARD7:24;

suppose j2 = j19 ; :: thesis:

hence contradiction by A710, A752, A755, A754, A759, A760, A766, A780, A811, A812; :: thesis:

end;

suppose j2 = j19 + 1 ; :: thesis:

hence contradiction by A738, A757, A776, A766, A777, A782, A811, A812; :: thesis:

end;

suppose j2 + 1 = j19 ; :: thesis:

hence contradiction by A710, A752, A756, A754, A759, A762, A764, A780, A811, A812; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A761, A764, A766, A768, A771, A773, A772, A778, A780, A782, A784, A788, A786, A789, A791, A813, GOBOARD7:23;

suppose ( i1 = i19 & j2 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A755, A754, A759, A760, A766, A780, A813; :: thesis:

end;

suppose ( i1 = i19 & j2 + 1 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A759, A762, A764, A780, A813; :: thesis:

end;

suppose ( i1 = i19 + 1 & j2 = j19 ) ; :: thesis:

hence contradiction by A738, A757, A776, A766, A777, A782, A813; :: thesis:

end;

suppose ( i1 = i19 + 1 & j2 + 1 = j19 ) ; :: thesis:

hence contradiction by A738, A758, A759, A764, A777, A782, A813; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A761, A764, A766, A768, A771, A773, A772, A778, A780, A782, A790, A788, A786, A792, A791, A814, GOBOARD7:23;

suppose ( i1 = i29 & j2 = j19 ) ; :: thesis:

hence contradiction by A738, A757, A776, A766, A777, A782, A814; :: thesis:

end;

suppose ( i1 = i29 & j2 + 1 = j19 ) ; :: thesis:

hence contradiction by A738, A758, A759, A764, A777, A782, A814; :: thesis:

end;

suppose ( i1 = i29 + 1 & j2 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A755, A754, A759, A760, A766, A780, A814; :: thesis:

end;

suppose ( i1 = i29 + 1 & j2 + 1 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A759, A762, A764, A780, A814; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A816: i1 = i19 by A761, A764, A766, A768, A771, A773, A772, A778, A780, A782, A784, A790, A786, A787, A791, GOBOARD7:21;

now

per cases by A761, A764, A766, A768, A771, A773, A772, A778, A780, A782, A784, A790, A786, A787, A791, A815, GOBOARD7:24;

suppose j2 = j29 ; :: thesis:

hence contradiction by A738, A757, A776, A766, A777, A782, A815, A816; :: thesis:

end;

suppose j2 = j29 + 1 ; :: thesis:

hence contradiction by A710, A752, A755, A754, A759, A760, A766, A780, A815, A816; :: thesis:

end;

suppose j2 + 1 = j29 ; :: thesis:

hence contradiction by A738, A758, A759, A764, A777, A782, A815, A816; :: thesis:

end;

hence contradiction ; :: 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) /\ (LSeg g,j) = {} ; :: according to XBOOLE_0:def 7 :: thesis:

end;

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

then consider i19, j19, i29, j29 being Element of NAT such that
A818: [i19,j19] in Indices (Gauge C,n) and
A819: g /. j = (Gauge C,n) * i19,j19 and
A820: [i29,j29] in Indices (Gauge C,n) and
A821: g /. (j + 1) = (Gauge C,n) * i29,j29 and
A822: ( ( i19 = i29 & j19 + 1 = j29 ) or ( i19 + 1 = i29 & j19 = j29 ) or ( i19 = i29 + 1 & j19 = j29 ) or ( i19 = i29 & j19 = j29 + 1 ) ) by A704, A754, JORDAN8:6;
A823: 1 <= i19 by A818, MATRIX_1:39;
A824: j29 <= width (Gauge C,n) by A820, MATRIX_1:39;
A825: 1 <= i29 by A820, MATRIX_1:39;
A826: i19 <= len (Gauge C,n) by A818, MATRIX_1:39;
A827: 1 <= j29 by A820, MATRIX_1:39;
A828: j19 <= width (Gauge C,n) by A818, MATRIX_1:39;
A829: i29 <= len (Gauge C,n) by A820, MATRIX_1:39;
A830: 1 <= j19 by A818, MATRIX_1:39;
assume (LSeg g,i) /\ (LSeg g,j) <> {} ; :: according to XBOOLE_0:def 7 :: thesis:
then A831: LSeg g,i meets LSeg g,j by XBOOLE_0:def 7;
A832: 1 < i + 1 by A817, NAT_1:13;
A833: j < len g by A817, NAT_1:12;
A834: i + 1 < len g by A757, A817, XXREAL_0:2;
then A835: LSeg g,i = LSeg (g /. i),(g /. (i + 1)) by A817, TOPREAL1:def 5;
A836: i < len g by A834, NAT_1:13;
consider i1, j1, i2, j2 being Element of NAT such that
A837: [i1,j1] in Indices (Gauge C,n) and
A838: g /. i = (Gauge C,n) * i1,j1 and
A839: [i2,j2] in Indices (Gauge C,n) and
A840: g /. (i + 1) = (Gauge C,n) * i2,j2 and
A841: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A704, A817, A834, JORDAN8:6;
A842: 1 <= i1 by A837, MATRIX_1:39;
A843: j2 <= width (Gauge C,n) by A839, MATRIX_1:39;
A844: j1 <= width (Gauge C,n) by A837, MATRIX_1:39;
A845: 1 <= j2 by A839, MATRIX_1:39;
A846: 1 <= j1 by A837, MATRIX_1:39;
A847: i2 <= len (Gauge C,n) by A839, MATRIX_1:39;
A848: i1 <= len (Gauge C,n) by A837, MATRIX_1:39;
A849: LSeg g,j = LSeg (g /. j),(g /. (j + 1)) by A754, A817, TOPREAL1:def 5;
A850: 1 <= i2 by A839, MATRIX_1:39;

now

per cases by A841, A822;

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

then A852: i1 = i19 by A835, A838, A840, A842, A848, A846, A843, A849, A819, A821, A823, A826, A830, A824, A831, GOBOARD7:21;

now

per cases by A835, A838, A840, A842, A848, A846, A843, A849, A819, A821, A823, A826, A830, A824, A831, A851, GOBOARD7:24;

suppose j1 = j19 ; :: thesis:

hence contradiction by A710, A752, A756, A754, A817, A836, A833, A838, A819, A852; :: thesis:

end;

suppose j1 = j19 + 1 ; :: thesis:

hence contradiction by A746, A758, A817, A838, A821, A851, A852; :: thesis:

end;

suppose j1 + 1 = j19 ; :: thesis:

hence contradiction by A710, A752, A755, A754, A834, A833, A840, A819, A851, A852; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A835, A838, A840, A842, A848, A846, A843, A849, A819, A821, A823, A830, A828, A829, A831, A853, GOBOARD7:23;

suppose ( i1 = i19 & j1 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A817, A836, A833, A838, A819; :: thesis:

end;

suppose ( i1 = i19 & j1 + 1 = j19 ) ; :: thesis:

hence contradiction by A738, A752, A832, A833, A840, A819, A853; :: thesis:

end;

suppose ( i1 = i19 + 1 & j1 = j19 ) ; :: thesis:

hence contradiction by A746, A758, A817, A838, A821, A853; :: thesis:

end;

suppose ( i1 = i19 + 1 & j1 + 1 = j19 ) ; :: thesis:

hence contradiction by A738, A757, A817, A832, A840, A821, A853; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A835, A838, A840, A842, A848, A846, A843, A849, A819, A821, A826, A830, A828, A825, A831, A854, GOBOARD7:23;

suppose ( i1 = i29 & j19 = j1 ) ; :: thesis:

hence contradiction by A746, A758, A817, A838, A821, A854; :: thesis:

end;

suppose ( i1 = i29 & j1 + 1 = j19 ) ; :: thesis:

hence contradiction by A738, A757, A817, A832, A840, A821, A854; :: thesis:

end;

suppose ( i1 = i29 + 1 & j19 = j1 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A817, A836, A833, A838, A819, A854; :: thesis:

end;

suppose ( i1 = i29 + 1 & j1 + 1 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A755, A754, A834, A833, A840, A819, A854; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A856: i1 = i19 by A835, A838, A840, A842, A848, A846, A843, A849, A819, A821, A823, A826, A828, A827, A831, GOBOARD7:21;

now

per cases by A835, A838, A840, A842, A848, A846, A843, A849, A819, A821, A823, A826, A828, A827, A831, A855, GOBOARD7:24;

suppose j1 = j29 ; :: thesis:

hence contradiction by A710, A752, A755, A754, A834, A833, A840, A819, A855, A856; :: thesis:

end;

suppose j1 = j29 + 1 ; :: thesis:

hence contradiction by A710, A752, A756, A754, A817, A836, A833, A838, A819, A855, A856; :: thesis:

end;

suppose j1 + 1 = j29 ; :: thesis:

hence contradiction by A738, A757, A817, A832, A840, A821, A855, A856; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A835, A838, A840, A842, A846, A844, A847, A849, A819, A821, A823, A826, A830, A824, A831, A857, GOBOARD7:23;

suppose ( i19 = i1 & j1 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A817, A836, A833, A838, A819; :: thesis:

end;

suppose ( i19 = i1 & j19 + 1 = j1 ) ; :: thesis:

hence contradiction by A746, A758, A817, A838, A821, A857; :: thesis:

end;

suppose ( i19 = i1 + 1 & j1 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A755, A754, A834, A833, A840, A819, A857; :: thesis:

end;

suppose ( i19 = i1 + 1 & j19 + 1 = j1 ) ; :: thesis:

hence contradiction by A738, A757, A817, A832, A840, A821, A857; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A859: j1 = j19 by A835, A838, A840, A842, A846, A844, A847, A849, A819, A821, A823, A830, A828, A829, A831, GOBOARD7:22;

now

per cases by A835, A838, A840, A842, A846, A844, A847, A849, A819, A821, A823, A830, A828, A829, A831, A858, GOBOARD7:25;

suppose i1 = i19 ; :: thesis:

hence contradiction by A710, A752, A756, A754, A817, A836, A833, A838, A819, A859; :: thesis:

end;

suppose i1 = i19 + 1 ; :: thesis:

hence contradiction by A746, A758, A817, A838, A821, A858, A859; :: thesis:

end;

suppose i1 + 1 = i19 ; :: thesis:

hence contradiction by A710, A752, A755, A754, A834, A833, A840, A819, A858, A859; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A861: j1 = j19 by A835, A838, A840, A842, A846, A844, A847, A849, A819, A821, A826, A830, A828, A825, A831, GOBOARD7:22;

now

per cases by A835, A838, A840, A842, A846, A844, A847, A849, A819, A821, A826, A830, A828, A825, A831, A860, GOBOARD7:25;

suppose i1 = i29 ; :: thesis:

hence contradiction by A746, A758, A817, A838, A821, A860, A861; :: thesis:

end;

suppose i1 = i29 + 1 ; :: thesis:

hence contradiction by A710, A752, A756, A754, A817, A836, A833, A838, A819, A860, A861; :: thesis:

end;

suppose i1 + 1 = i29 ; :: thesis:

hence contradiction by A738, A757, A817, A832, A840, A821, A860, A861; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A835, A838, A840, A842, A846, A844, A847, A849, A819, A821, A823, A826, A828, A827, A831, A862, GOBOARD7:23;

suppose ( i19 = i1 & j1 = j29 ) ; :: thesis:

hence contradiction by A746, A758, A817, A838, A821, A862; :: thesis:

end;

suppose ( i19 = i1 & j29 + 1 = j1 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A817, A836, A833, A838, A819, A862; :: thesis:

end;

suppose ( i19 = i1 + 1 & j1 = j29 ) ; :: thesis:

hence contradiction by A738, A757, A817, A832, A840, A821, A862; :: thesis:

end;

suppose ( i19 = i1 + 1 & j29 + 1 = j1 ) ; :: thesis:

hence contradiction by A710, A752, A755, A754, A834, A833, A840, A819, A862; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A835, A838, A840, A848, A846, A844, A850, A849, A819, A821, A823, A826, A830, A824, A831, A863, GOBOARD7:23;

suppose ( i19 = i2 & j19 = j1 ) ; :: thesis:

hence contradiction by A710, A752, A755, A754, A834, A833, A840, A819, A863; :: thesis:

end;

suppose ( i19 = i2 & j19 + 1 = j1 ) ; :: thesis:

hence contradiction by A738, A757, A817, A832, A840, A821, A863; :: thesis:

end;

suppose ( i19 = i2 + 1 & j19 = j1 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A817, A836, A833, A838, A819, A863; :: thesis:

end;

suppose ( i19 = i2 + 1 & j19 + 1 = j1 ) ; :: thesis:

hence contradiction by A746, A758, A817, A838, A821, A863; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A865: j1 = j19 by A835, A838, A840, A848, A846, A844, A850, A849, A819, A821, A823, A830, A828, A829, A831, GOBOARD7:22;

now

per cases by A835, A838, A840, A848, A846, A844, A850, A849, A819, A821, A823, A830, A828, A829, A831, A864, GOBOARD7:25;

suppose i2 = i19 ; :: thesis:

hence contradiction by A710, A752, A755, A754, A834, A833, A840, A819, A864, A865; :: thesis:

end;

suppose i2 = i19 + 1 ; :: thesis:

hence contradiction by A738, A757, A817, A832, A840, A821, A864, A865; :: thesis:

end;

suppose i2 + 1 = i19 ; :: thesis:

hence contradiction by A710, A752, A756, A754, A817, A836, A833, A838, A819, A864, A865; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A867: j1 = j19 by A835, A838, A840, A848, A846, A844, A850, A849, A819, A821, A826, A830, A828, A825, A831, GOBOARD7:22;

now

per cases by A835, A838, A840, A848, A846, A844, A850, A849, A819, A821, A826, A830, A828, A825, A831, A866, GOBOARD7:25;

suppose i2 = i29 ; :: thesis:

hence contradiction by A738, A757, A817, A832, A840, A821, A866, A867; :: thesis:

end;

suppose i2 = i29 + 1 ; :: thesis:

hence contradiction by A710, A752, A755, A754, A834, A833, A840, A819, A866, A867; :: thesis:

end;

suppose i2 + 1 = i29 ; :: thesis:

hence contradiction by A746, A758, A817, A838, A821, A866, A867; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A835, A838, A840, A848, A846, A844, A850, A849, A819, A821, A823, A826, A828, A827, A831, A868, GOBOARD7:23;

suppose ( i19 = i2 & j29 = j1 ) ; :: thesis:

hence contradiction by A738, A757, A817, A832, A840, A821, A868; :: thesis:

end;

suppose ( i19 = i2 & j29 + 1 = j1 ) ; :: thesis:

hence contradiction by A710, A752, A755, A754, A834, A833, A840, A819, A868; :: thesis:

end;

suppose ( i19 = i2 + 1 & j29 = j1 ) ; :: thesis:

hence contradiction by A746, A758, A817, A838, A821, A868; :: thesis:

end;

suppose ( i19 = i2 + 1 & j29 + 1 = j1 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A817, A836, A833, A838, A819, A868; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A870: i1 = i19 by A835, A838, A840, A842, A848, A844, A845, A849, A819, A821, A823, A826, A830, A824, A831, GOBOARD7:21;

now

per cases by A835, A838, A840, A842, A848, A844, A845, A849, A819, A821, A823, A826, A830, A824, A831, A869, GOBOARD7:24;

suppose j2 = j19 ; :: thesis:

hence contradiction by A710, A752, A755, A754, A834, A833, A840, A819, A869, A870; :: thesis:

end;

suppose j2 = j19 + 1 ; :: thesis:

hence contradiction by A738, A757, A817, A832, A840, A821, A869, A870; :: thesis:

end;

suppose j2 + 1 = j19 ; :: thesis:

hence contradiction by A710, A752, A756, A754, A817, A836, A833, A838, A819, A869, A870; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A835, A838, A840, A842, A848, A844, A845, A849, A819, A821, A823, A830, A828, A829, A831, A871, GOBOARD7:23;

suppose ( i1 = i19 & j2 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A755, A754, A834, A833, A840, A819, A871; :: thesis:

end;

suppose ( i1 = i19 & j2 + 1 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A817, A836, A833, A838, A819, A871; :: thesis:

end;

suppose ( i1 = i19 + 1 & j2 = j19 ) ; :: thesis:

hence contradiction by A738, A757, A817, A832, A840, A821, A871; :: thesis:

end;

suppose ( i1 = i19 + 1 & j2 + 1 = j19 ) ; :: thesis:

hence contradiction by A746, A758, A817, A838, A821, A871; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A835, A838, A840, A842, A848, A844, A845, A849, A819, A821, A826, A830, A828, A825, A831, A872, GOBOARD7:23;

suppose ( i1 = i29 & j2 = j19 ) ; :: thesis:

hence contradiction by A738, A757, A817, A832, A840, A821, A872; :: thesis:

end;

suppose ( i1 = i29 & j2 + 1 = j19 ) ; :: thesis:

hence contradiction by A746, A758, A817, A838, A821, A872; :: thesis:

end;

suppose ( i1 = i29 + 1 & j2 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A755, A754, A834, A833, A840, A819, A872; :: thesis:

end;

suppose ( i1 = i29 + 1 & j2 + 1 = j19 ) ; :: thesis:

hence contradiction by A710, A752, A756, A754, A817, A836, A833, A838, A819, A872; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A874: i1 = i19 by A835, A838, A840, A842, A848, A844, A845, A849, A819, A821, A823, A826, A828, A827, A831, GOBOARD7:21;

now

per cases by A835, A838, A840, A842, A848, A844, A845, A849, A819, A821, A823, A826, A828, A827, A831, A873, GOBOARD7:24;

suppose j2 = j29 ; :: thesis:

hence contradiction by A738, A757, A817, A832, A840, A821, A873, A874; :: thesis:

end;

suppose j2 = j29 + 1 ; :: thesis:

hence contradiction by A710, A752, A755, A754, A834, A833, A840, A819, A873, A874; :: thesis:

end;

suppose j2 + 1 = j29 ; :: thesis:

hence contradiction by A746, A758, A817, A838, A821, A873, A874; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then reconsider g = g as non constant standard special_circular_sequence by A650, A737, A701, A704, A706, FINSEQ_6:def 1, JORDAN8:7;
reconsider Lg9 = (L~ g) ` as Subset of (TOP-REAL 2) ;
A875: C c= Lg9

proof

let c be set ; :: according to TARSKI:def 3 :: thesis:
assume that
A876: c in C and
A877: not c in Lg9 ; :: thesis:
reconsider c = c as Point of (TOP-REAL 2) by A876;
consider i being Element of NAT such that
A878: 1 <= i and
A879: i + 1 <= len g and
A880: c in LSeg (g /. i),(g /. (i + 1)) by A877, SPPOL_2:14, SUBSET_1:50;
A881: 1 <= i + (m -' 1) by A878, NAT_1:12;
i + 1 in dom g by A878, A879, GOBOARD2:3;
then A882: g /. (i + 1) = f /. ((i + 1) + (m -' 1)) by FINSEQ_5:30;
(i + 1) + (m -' 1) = (i + (m -' 1)) + 1 ;
then A883: (i + (m -' 1)) + 1 <= (len g) + (m -' 1) by A879, XREAL_1:8;
i in dom g by A878, A879, GOBOARD2:3;
then g /. i = f /. (i + (m -' 1)) by FINSEQ_5:30;
then c in LSeg f,(i + (m -' 1)) by A700, A880, A882, A881, A883, TOPREAL1:def 5;
then c in (right_cell f,(i + (m -' 1)),(Gauge C,n)) /\ (left_cell f,(i + (m -' 1)),(Gauge C,n)) by A439, A700, A881, A883, GOBRD13:30;
then c in right_cell f,(i + (m -' 1)),(Gauge C,n) by XBOOLE_0:def 4;
then right_cell f,(i + (m -' 1)),(Gauge C,n) meets C by A876, XBOOLE_0:3;
hence contradiction by A439, A700, A881, A883; :: thesis:

end;

A884: LeftComp g is_a_component_of (L~ g) ` by GOBOARD9:def 1;
L~ g is closed by SPPOL_1:49;
then (L~ g) ` is open by TOPS_1:29;
then A885: (L~ g) ` = Int ((L~ g) ` ) by TOPS_1:55;
A886: C meets LeftComp g

proof

left_cell f,m,(Gauge C,n) meets C by A439, A651, A658;
then consider p being set such that
A887: p in left_cell f,m,(Gauge C,n) and
A888: p in C by XBOOLE_0:3;
reconsider p = p as Element of (TOP-REAL 2) by A887;

now

reconsider u = p as Element of (Euclid 2) by TOPREAL3:13;
take p = p; :: thesis:
thus p in C by A888; :: thesis:
A889: Int (left_cell g,1) c= LeftComp g by A703, GOBOARD9:24;
Int (left_cell g,1,(Gauge C,n)) c= Int (left_cell g,1) by A704, A703, GOBRD13:34, TOPS_1:48;
then Int (left_cell g,1,(Gauge C,n)) c= LeftComp g by A889, XBOOLE_1:1;
then Int (left_cell f,((m -' 1) + 1),(Gauge C,n)) c= LeftComp g by A652, A699, A703, GOBRD13:33;
then A890: Int (left_cell f,m,(Gauge C,n)) c= LeftComp g by A651, XREAL_1:237;
consider r being real number such that
A891: r > 0 and
A892: Ball u,r c= (L~ g) ` by A875, A885, A888, GOBOARD6:8;
reconsider r = r as Real by XREAL_0:def 1;
reconsider B = Ball u,r as non empty Subset of (TOP-REAL 2) by A4, A891, TBSP_1:16, TOPMETR:16;
A893: B is open by GOBOARD6:6;
A894: left_cell f,m,(Gauge C,n) = Cl (Int (left_cell f,m,(Gauge C,n))) by A651, A658, A679;
p in Ball u,r by A891, TBSP_1:16;
then A895: Int (left_cell f,m,(Gauge C,n)) meets B by A887, A894, A893, TOPS_1:39;
A896: p in B by A891, TBSP_1:16;
B is connected by SPRECT_3:17;
then B c= LeftComp g by A884, A892, A890, A895, GOBOARD9:6;
hence p in LeftComp g by A896; :: thesis:

end;

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

end;

A897: L~ g c= L~ f by JORDAN3:75;
A898: RightComp g is_a_component_of (L~ g) ` by GOBOARD9:def 2;
m = 1

proof

A899: for n being Element of NAT st 1 <= n holds
(n -' 1) + 2 = n + 1

proof

let n be Element of NAT ; :: thesis:
assume 1 <= n ; :: thesis:
hence (n -' 1) + 2 = (n + 2) -' 1 by NAT_D:38
.= ((n + 1) + 1) - 1 by NAT_D:37
.= n + 1 ;
:: thesis:

end;

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

proof

A902: 2 <= len (Gauge C,n) by A2, NAT_1:12;
let n be Element of NAT ; :: thesis:
assume that
A903: 1 <= n and
A904: n <= m -' 1 ; :: thesis:
set p = f /. n;
A905: n <= len f by A699, A904, XXREAL_0:2;
then A906: f /. n in Values (Gauge C,n) by A439, A903, JORDAN9:8;
assume f /. n in L~ g ; :: thesis:
then consider j being Element of NAT such that
A907: (m -' 1) + 1 <= j and
A908: j + 1 <= len f and
A909: f /. n in LSeg f,j by A699, JORDAN9:9;
A910: j + 1 <= k by A176, A908;
A911: j < k by A709, A908, NAT_1:13;
A912: n < (m -' 1) + 1 by A904, NAT_1:13;
then A913: n < j by A907, XXREAL_0:2;
A914: (m -' 1) + 1 = m by A651, XREAL_1:237;
then A915: 1 < j by A900, A907, XXREAL_0:2;

per cases by A6, A439, A908, A909, A915, A902, A906, JORDAN9:25;

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

A917: n <> len (F . j) by A176, A907, A912;
n <= len (F . j) by A176, A913;
then A918: n in dom (F . j) by A903, FINSEQ_3:27;
(F . j) /. n = (F . n) /. n by A565, A903, A913
.= f /. n by A709, A565, A903, A905
.= (F . j) /. j by A565, A915, A911, A916
.= (F . j) /. (len (F . j)) by A176 ;
hence contradiction by A647, A915, A911, A918, A917; :: thesis:

end;

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

now

per cases by A910, XXREAL_0:1;

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

A921: n <> len (F . m) by A176, A912, A914;
n <= len (F . m) by A176, A912, A914;
then A922: n in dom (F . m) by A903, FINSEQ_3:27;
(F . m) /. n = (F . n) /. n by A565, A903, A912, A914
.= f /. n by A709, A565, A903, A905
.= (F . m) /. m by A650, A709, A651, A653, A565, A919, A920
.= (F . m) /. (len (F . m)) by A176 ;
hence contradiction by A647, A709, A651, A654, A922, A921; :: thesis:

end;

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

set l = j + 1;
A924: 1 <= j + 1 by NAT_1:11;
A925: n < n + 1 by XREAL_1:31;
A926: n + 1 < j + 1 by A913, XREAL_1:8;
then A927: n <> len (F . (j + 1)) by A176, A925;
A928: n < j + 1 by A925, A926, XXREAL_0:2;
then n <= len (F . (j + 1)) by A176;
then A929: n in dom (F . (j + 1)) by A903, FINSEQ_3:27;
(F . (j + 1)) /. n = (F . n) /. n by A565, A903, A928
.= f /. n by A709, A565, A903, A905
.= (F . (j + 1)) /. (j + 1) by A565, A919, A923, A924
.= (F . (j + 1)) /. (len (F . (j + 1))) by A176 ;
hence contradiction by A647, A923, A929, A927, NAT_1:11; :: thesis:

end;

hence contradiction ; :: thesis:

end;

C meets LeftComp (Rev g)

proof

1 <= len g by A703, XREAL_1:147;
then A930: ((len g) -' 1) + 2 = (len g) + 1 by A899;
A931: 1 - 1 < m - 1 by A900, XREAL_1:11;
A932: (m -' 1) + 2 = m + 1 by A651, A899;
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;
A933: (1 + 1) - 1 <= (len g) - 1 by A702, XREAL_1:11;
(1 + 1) -' 1 <= (len g) -' 1 by A702, NAT_D:42;
then A934: 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 A935: m -' 1 <> len (F . ((m -' 1) + ((len g) -' 1))) by A176;
A936: 1 + 1 <= len (Rev g) by A702, FINSEQ_5:def 3;
then (1 + 1) -' 1 <= (len (Rev g)) -' 1 by NAT_D:42;
then A937: 1 <= (len (Rev g)) -' 1 by NAT_D:34;
A938: Rev g is_sequence_on Gauge C,n by A704, JORDAN9:7;
then consider p1, p2, q1, q2 being Element of NAT such that
A939: [p1,p2] in Indices (Gauge C,n) and
A940: (Rev g) /. 1 = (Gauge C,n) * p1,p2 and
A941: [q1,q2] in Indices (Gauge C,n) and
A942: (Rev g) /. 2 = (Gauge C,n) * q1,q2 and
A943: ( ( p1 = q1 & p2 + 1 = q2 ) or ( p1 + 1 = q1 & p2 = q2 ) or ( p1 = q1 + 1 & p2 = q2 ) or ( p1 = q1 & p2 = q2 + 1 ) ) by A936, JORDAN8:6;
A944: 1 <= p1 by A939, MATRIX_1:39;
A945: p2 <= width (Gauge C,n) by A939, MATRIX_1:39;
A946: p1 <= len (Gauge C,n) by A939, MATRIX_1:39;
A947: 1 <= p2 by A939, MATRIX_1:39;
A948: (Rev g) /. 1 = f /. m by A650, A701, FINSEQ_5:68;
(len g) -' 1 <= len g by NAT_D:44;
then A949: (len g) -' 1 in dom g by A934, FINSEQ_3:27;
then A950: (Rev g) /. 2 = g /. ((len g) -' 1) by A930, FINSEQ_5:69
.= f /. ((m -' 1) + ((len g) -' 1)) by A949, FINSEQ_5:30 ;
1 < len (Rev g) by A936, NAT_1:13;
then A951: ((len (Rev g)) -' 1) + 1 = len (Rev g) by XREAL_1:237;
A952: (m -' 1) + ((len g) -' 1) = (m + ((len g) -' 1)) -' 1 by A651, NAT_D:38
.= (((len g) -' 1) + m) - 1 by A934, NAT_D:37
.= (((len g) - 1) + m) - 1 by A933, XREAL_0:def 2
.= (((k - (m - 1)) - 1) + m) - 1 by A709, A700, A931, XREAL_0:def 2
.= k - 1 ;
then A953: (Rev g) /. 1 = f /. (((m -' 1) + ((len g) -' 1)) + 1) by A709, A701, FINSEQ_5:68;
A954: (m -' 1) + 1 = m by A651, XREAL_1:237;
then A955: 1 <= m -' 1 by A900, NAT_1:13;
then A956: left_cell f,(m -' 1),(Gauge C,n) meets C by A439, A653, A954;
m -' 1 <= (m -' 1) + ((len g) -' 1) by NAT_1:11;
then m -' 1 <= len (F . ((m -' 1) + ((len g) -' 1))) by A176;
then A957: m -' 1 in dom (F . ((m -' 1) + ((len g) -' 1))) by A955, FINSEQ_3:27;
not f /. (m -' 1) in L~ g by A901, A955;
then A958: not f /. (m -' 1) in L~ (Rev g) by SPPOL_2:22;
A959: k = ((m -' 1) + ((len g) -' 1)) + 1 by A952;
then A960: (m -' 1) + ((len g) -' 1) < k by XREAL_1:31;
(len g) -' 1 <= (m -' 1) + ((len g) -' 1) by NAT_1:11;
then A961: 1 <= (m -' 1) + ((len g) -' 1) by A934, XXREAL_0:2;
then A962: left_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) meets C by A439, A709, A959;

per cases by A943;

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

consider a1, a2, p91, p92 being Element of NAT such that
A964: [a1,a2] in Indices (Gauge C,n) and
A965: f /. (m -' 1) = (Gauge C,n) * a1,a2 and
A966: [p91,p92] in Indices (Gauge C,n) and
A967: (Rev g) /. 1 = (Gauge C,n) * p91,p92 and
A968: ( ( a1 = p91 & a2 + 1 = p92 ) or ( a1 + 1 = p91 & a2 = p92 ) or ( a1 = p91 + 1 & a2 = p92 ) or ( a1 = p91 & a2 = p92 + 1 ) ) by A652, A653, A948, A954, A955, JORDAN8:6;
A969: 1 <= a2 by A964, MATRIX_1:39;
thus C meets LeftComp (Rev g) :: thesis:

proof

per cases by A968;

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

A971: m -' 1 <= m by A954, NAT_1:11;
A972: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A709, A699, A565, A955
.= (F . m) /. (m -' 1) by A565, A955, A971 ;
A973: 2 in dom g by A702, FINSEQ_3:27;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A930, FINSEQ_5:def 3;
then A974: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A973, FINSEQ_5:69
.= f /. (m + 1) by A932, A973, FINSEQ_5:30 ;
A975: L~ (Rev g) c= L~ f by A897, SPPOL_2:22;
A976: (Rev g) /. 1 = g /. 1 by A650, A737, A701, FINSEQ_5:68
.= (Rev g) /. (len g) by FINSEQ_5:68
.= (Rev g) /. (len (Rev g)) by FINSEQ_5:def 3 ;
A977: (F . k) | (m + 1) = F . (m + 1) by A564, A709, A658;
A978: a1 = p1 by A939, A940, A966, A967, A970, GOBOARD1:21;
A979: f /. ((m -' 1) + 1) = (F . m) /. m by A709, A651, A653, A565, A954;
A980: (m -' 1) + 1 <= len (F . m) by A176, A954;
set rc = (left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g));
A981: a2 + 1 > a2 by NAT_1:13;
A982: a2 + 1 = p2 by A939, A940, A966, A967, A970, GOBOARD1:21;
then A983: p2 -' 1 = a2 by NAT_D:34;
left_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) = cell (Gauge C,n),p1,p2 by A439, A709, A952, A961, A950, A953, A939, A940, A941, A942, A963, GOBRD13:28
.= front_right_cell (F . m),(m -' 1),(Gauge C,n) by A439, A948, A954, A955, A939, A940, A964, A965, A978, A982, A980, A972, A979, GOBRD13:36 ;
then F . (m + 1) turns_right m -' 1, Gauge C,n by A513, A900, A962;
then A984: f turns_right m -' 1, Gauge C,n by A955, A932, A977, GOBRD13:44;
A985: p2 + 1 > a2 + 1 by A982, NAT_1:13;
then A986: [(p1 + 1),p2] in Indices (Gauge C,n) by A948, A954, A939, A940, A964, A965, A981, A984, GOBRD13:def 6;
then A987: p1 + 1 <= len (Gauge C,n) by MATRIX_1:39;
f /. (m + 1) = (Gauge C,n) * (p1 + 1),p2 by A948, A954, A932, A939, A940, A964, A965, A985, A981, A984, GOBRD13:def 6;
then left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) = cell (Gauge C,n),p1,a2 by A938, A937, A951, A939, A940, A986, A983, A974, A976, GOBRD13:26;
then f /. (m -' 1) in left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) by A944, A945, A965, A969, A978, A982, A987, JORDAN9:22;
then A988: f /. (m -' 1) in (left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g)) by A958, XBOOLE_0:def 5;
A989: LeftComp (Rev g) is_a_component_of (L~ (Rev g)) ` by GOBOARD9:def 1;
(left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g)) c= LeftComp (Rev g) by A938, A937, A951, JORDAN9:29;
hence C meets LeftComp (Rev g) by A653, A659, A954, A955, A958, A988, A975, A989; :: thesis:

end;

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

then a1 + 1 = p1 by A939, A940, A966, A967, GOBOARD1:21;
then A991: q1 -' 1 = a1 by A963, NAT_D:34;
a2 = p2 by A939, A940, A966, A967, A990, GOBOARD1:21;
then right_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) = cell (Gauge C,n),a1,a2 by A439, A709, A952, A961, A950, A953, A939, A940, A941, A942, A963, A991, GOBRD13:29
.= left_cell f,(m -' 1),(Gauge C,n) by A439, A653, A948, A954, A955, A964, A965, A966, A967, A990, GOBRD13:24 ;
hence C meets LeftComp (Rev g) by A439, A709, A959, A961, A956; :: thesis:

end;

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

then A993: a2 = p2 by A939, A940, A966, A967, GOBOARD1:21;
a1 = p1 + 1 by A939, A940, A966, A967, A992, GOBOARD1:21;
then right_cell f,(m -' 1),(Gauge C,n) = cell (Gauge C,n),p1,p2 by A650, A652, A653, A701, A954, A955, A939, A940, A964, A965, A993, FINSEQ_5:68, GOBRD13:27
.= left_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) by A439, A709, A952, A961, A950, A953, A939, A940, A941, A942, A963, GOBRD13:28 ;
hence C meets LeftComp (Rev g) by A439, A653, A954, A955, A962; :: thesis:

end;

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

then A995: a2 = q2 by A939, A940, A963, A966, A967, GOBOARD1:21;
A996: a1 = q1 by A939, A940, A963, A966, A967, A994, GOBOARD1:21;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A565, A955, NAT_1:11
.= (Rev g) /. 2 by A709, A699, A565, A955, A942, A965, A996, A995
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A565, A960, A961, A950
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A176 ;
hence C meets LeftComp (Rev g) by A647, A960, A961, A957, A935; :: thesis:

end;

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

consider a1, a2, p91, p92 being Element of NAT such that
A998: [a1,a2] in Indices (Gauge C,n) and
A999: f /. (m -' 1) = (Gauge C,n) * a1,a2 and
A1000: [p91,p92] in Indices (Gauge C,n) and
A1001: (Rev g) /. 1 = (Gauge C,n) * p91,p92 and
A1002: ( ( a1 = p91 & a2 + 1 = p92 ) or ( a1 + 1 = p91 & a2 = p92 ) or ( a1 = p91 + 1 & a2 = p92 ) or ( a1 = p91 & a2 = p92 + 1 ) ) by A652, A653, A948, A954, A955, JORDAN8:6;
A1003: 1 <= a2 by A998, MATRIX_1:39;
A1004: a2 <= width (Gauge C,n) by A998, MATRIX_1:39;
A1005: 1 <= a1 by A998, MATRIX_1:39;
thus C meets LeftComp (Rev g) :: thesis:

proof

per cases by A1002;

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

then a2 + 1 = p2 by A939, A940, A1000, A1001, GOBOARD1:21;
then A1007: q2 -' 1 = a2 by A997, NAT_D:34;
A1008: a1 = p1 by A939, A940, A1000, A1001, A1006, GOBOARD1:21;
right_cell f,(m -' 1),(Gauge C,n) = cell (Gauge C,n),a1,a2 by A439, A653, A948, A954, A955, A998, A999, A1000, A1001, A1006, GOBRD13:23
.= left_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) by A439, A709, A952, A961, A950, A953, A939, A940, A941, A942, A997, A1008, A1007, GOBRD13:26 ;
hence C meets LeftComp (Rev g) by A439, A653, A954, A955, A962; :: thesis:

end;

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

A1010: m -' 1 <= m by A954, NAT_1:11;
A1011: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A709, A699, A565, A955
.= (F . m) /. (m -' 1) by A565, A955, A1010 ;
A1012: 2 in dom g by A702, FINSEQ_3:27;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A930, FINSEQ_5:def 3;
then A1013: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A1012, FINSEQ_5:69
.= f /. (m + 1) by A932, A1012, FINSEQ_5:30 ;
A1014: L~ (Rev g) c= L~ f by A897, SPPOL_2:22;
A1015: (F . k) | (m + 1) = F . (m + 1) by A564, A709, A658;
A1016: (m -' 1) + 1 <= len (F . m) by A176, A954;
A1017: a2 = p2 by A939, A940, A1000, A1001, A1009, GOBOARD1:21;
A1018: (Rev g) /. 1 = g /. 1 by A650, A737, A701, FINSEQ_5:68
.= (Rev g) /. (len g) by FINSEQ_5:68
.= (Rev g) /. (len (Rev g)) by FINSEQ_5:def 3 ;
set rc = (left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g));
A1019: p1 < p1 + 1 by XREAL_1:31;
A1020: f /. ((m -' 1) + 1) = (F . m) /. m by A709, A651, A653, A565, A954;
A1021: (a2 -' 1) + 1 = a2 by A1003, XREAL_1:237;
A1022: a1 + 1 = p1 by A939, A940, A1000, A1001, A1009, GOBOARD1:21;
then A1023: a1 = p1 -' 1 by NAT_D:34;
left_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) = cell (Gauge C,n),p1,(p2 -' 1) by A439, A709, A952, A961, A950, A953, A939, A940, A941, A942, A997, GOBRD13:26
.= front_right_cell (F . m),(m -' 1),(Gauge C,n) by A439, A948, A954, A955, A939, A940, A998, A999, A1022, A1017, A1016, A1011, A1020, GOBRD13:38 ;
then F . (m + 1) turns_right m -' 1, Gauge C,n by A513, A900, A962;
then A1024: f turns_right m -' 1, Gauge C,n by A955, A932, A1015, GOBRD13:44;
A1025: a1 < a1 + 1 by XREAL_1:31;
then A1026: [p1,(p2 -' 1)] in Indices (Gauge C,n) by A948, A954, A939, A940, A998, A999, A1022, A1019, A1024, GOBRD13:def 6;
then A1027: 1 <= a2 -' 1 by A1017, MATRIX_1:39;
f /. (m + 1) = (Gauge C,n) * p1,(p2 -' 1) by A948, A954, A932, A939, A940, A998, A999, A1022, A1025, A1019, A1024, GOBRD13:def 6;
then left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) = cell (Gauge C,n),a1,(a2 -' 1) by A938, A937, A951, A939, A940, A1017, A1026, A1023, A1013, A1021, A1018, GOBRD13:22;
then f /. (m -' 1) in left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) by A946, A999, A1005, A1004, A1022, A1021, A1027, JORDAN9:22;
then A1028: f /. (m -' 1) in (left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g)) by A958, XBOOLE_0:def 5;
A1029: LeftComp (Rev g) is_a_component_of (L~ (Rev g)) ` by GOBOARD9:def 1;
(left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g)) c= LeftComp (Rev g) by A938, A937, A951, JORDAN9:29;
hence C meets LeftComp (Rev g) by A653, A659, A954, A955, A958, A1028, A1014, A1029; :: thesis:

end;

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

then A1031: a2 = q2 by A939, A940, A997, A1000, A1001, GOBOARD1:21;
A1032: a1 = q1 by A939, A940, A997, A1000, A1001, A1030, GOBOARD1:21;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A565, A955, NAT_1:11
.= (Rev g) /. 2 by A709, A699, A565, A955, A942, A999, A1032, A1031
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A565, A960, A961, A950
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A176 ;
hence C meets LeftComp (Rev g) by A647, A960, A961, A957, A935; :: thesis:

end;

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

then A1034: a2 = p2 + 1 by A939, A940, A1000, A1001, GOBOARD1:21;
A1035: a1 = p1 by A939, A940, A1000, A1001, A1033, GOBOARD1:21;
right_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) = cell (Gauge C,n),p1,p2 by A439, A709, A952, A961, A950, A953, A939, A940, A941, A942, A997, GOBRD13:27
.= left_cell f,(m -' 1),(Gauge C,n) by A650, A652, A653, A701, A954, A955, A939, A940, A998, A999, A1035, A1034, FINSEQ_5:68, GOBRD13:28 ;
hence C meets LeftComp (Rev g) by A439, A709, A959, A961, A956; :: thesis:

end;

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

consider a1, a2, p91, p92 being Element of NAT such that
A1037: [a1,a2] in Indices (Gauge C,n) and
A1038: f /. (m -' 1) = (Gauge C,n) * a1,a2 and
A1039: [p91,p92] in Indices (Gauge C,n) and
A1040: (Rev g) /. 1 = (Gauge C,n) * p91,p92 and
A1041: ( ( a1 = p91 & a2 + 1 = p92 ) or ( a1 + 1 = p91 & a2 = p92 ) or ( a1 = p91 + 1 & a2 = p92 ) or ( a1 = p91 & a2 = p92 + 1 ) ) by A652, A653, A948, A954, A955, JORDAN8:6;
A1042: a1 <= len (Gauge C,n) by A1037, MATRIX_1:39;
thus C meets LeftComp (Rev g) :: thesis:

proof

per cases by A1041;

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

then a2 + 1 = p2 by A939, A940, A1039, A1040, GOBOARD1:21;
then A1044: q2 -' 1 = a2 by A1036, NAT_D:34;
a1 = p1 by A939, A940, A1039, A1040, A1043, GOBOARD1:21;
then A1045: q1 = a1 -' 1 by A1036, NAT_D:34;
right_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) = cell (Gauge C,n),q1,(q2 -' 1) by A439, A709, A952, A961, A950, A953, A939, A940, A941, A942, A1036, GOBRD13:25
.= left_cell f,(m -' 1),(Gauge C,n) by A439, A653, A948, A954, A955, A1037, A1038, A1039, A1040, A1043, A1045, A1044, GOBRD13:22 ;
hence C meets LeftComp (Rev g) by A439, A709, A959, A961, A956; :: thesis:

end;

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

then A1047: a2 = p2 by A939, A940, A1039, A1040, GOBOARD1:21;
A1048: a1 + 1 = p1 by A939, A940, A1039, A1040, A1046, GOBOARD1:21;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A565, A955, NAT_1:11
.= (Rev g) /. 2 by A709, A699, A565, A955, A942, A1036, A1038, A1048, A1047
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A565, A960, A961, A950
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A176 ;
hence C meets LeftComp (Rev g) by A647, A960, A961, A957, A935; :: thesis:

end;

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

A1050: m -' 1 <= m by A954, NAT_1:11;
A1051: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A709, A699, A565, A955
.= (F . m) /. (m -' 1) by A565, A955, A1050 ;
A1052: 2 in dom g by A702, FINSEQ_3:27;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A930, FINSEQ_5:def 3;
then A1053: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A1052, FINSEQ_5:69
.= f /. (m + 1) by A932, A1052, FINSEQ_5:30 ;
A1054: L~ (Rev g) c= L~ f by A897, SPPOL_2:22;
set rc = (left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g));
A1055: LeftComp (Rev g) is_a_component_of (L~ (Rev g)) ` by GOBOARD9:def 1;
A1056: p1 -' 1 = q1 by A1036, NAT_D:34;
A1057: (F . k) | (m + 1) = F . (m + 1) by A564, A709, A658;
A1058: a1 = p1 + 1 by A939, A940, A1039, A1040, A1049, GOBOARD1:21;
A1059: f /. ((m -' 1) + 1) = (F . m) /. m by A709, A651, A653, A565, A954;
A1060: (m -' 1) + 1 <= len (F . m) by A176, A954;
A1061: a2 = p2 by A939, A940, A1039, A1040, A1049, GOBOARD1:21;
left_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) = cell (Gauge C,n),q1,q2 by A439, A709, A952, A961, A950, A953, A939, A940, A941, A942, A1036, GOBRD13:24
.= front_right_cell (F . m),(m -' 1),(Gauge C,n) by A439, A948, A954, A955, A939, A940, A1036, A1037, A1038, A1058, A1061, A1056, A1060, A1051, A1059, GOBRD13:40 ;
then F . (m + 1) turns_right m -' 1, Gauge C,n by A513, A900, A962;
then A1062: f turns_right m -' 1, Gauge C,n by A955, A932, A1057, GOBRD13:44;
p1 + 1 > p1 by XREAL_1:31;
then A1063: a1 + 1 > p1 by A1058, NAT_1:13;
then A1064: [p1,(p2 + 1)] in Indices (Gauge C,n) by A948, A954, A939, A940, A1037, A1038, A1061, A1062, GOBRD13:def 6;
then A1065: p2 + 1 <= width (Gauge C,n) by MATRIX_1:39;
a2 + 1 > p2 by A1061, NAT_1:13;
then A1066: f /. (m + 1) = (Gauge C,n) * p1,(p2 + 1) by A948, A954, A932, A939, A940, A1037, A1038, A1061, A1063, A1062, GOBRD13:def 6;
(Rev g) /. 1 = g /. 1 by A650, A737, A701, FINSEQ_5:68
.= (Rev g) /. (len g) by FINSEQ_5:68
.= (Rev g) /. (len (Rev g)) by FINSEQ_5:def 3 ;
then left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) = cell (Gauge C,n),p1,p2 by A938, A937, A951, A939, A940, A1066, A1064, A1053, GOBRD13:28;
then f /. (m -' 1) in left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) by A944, A947, A1038, A1042, A1058, A1061, A1065, JORDAN9:22;
then A1067: f /. (m -' 1) in (left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g)) by A958, XBOOLE_0:def 5;
(left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g)) c= LeftComp (Rev g) by A938, A937, A951, JORDAN9:29;
hence C meets LeftComp (Rev g) by A653, A659, A954, A955, A958, A1067, A1054, A1055; :: thesis:

end;

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

then a1 = p1 by A939, A940, A1039, A1040, GOBOARD1:21;
then A1069: q1 = a1 -' 1 by A1036, NAT_D:34;
a2 = p2 + 1 by A939, A940, A1039, A1040, A1068, GOBOARD1:21;
then right_cell f,(m -' 1),(Gauge C,n) = cell (Gauge C,n),q1,q2 by A650, A652, A653, A701, A954, A955, A1036, A1037, A1038, A1039, A1040, A1068, A1069, FINSEQ_5:68, GOBRD13:29
.= left_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) by A439, A709, A952, A961, A950, A953, A939, A940, A941, A942, A1036, GOBRD13:24 ;
hence C meets LeftComp (Rev g) by A439, A653, A954, A955, A962; :: thesis:

end;

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

consider a1, a2, p91, p92 being Element of NAT such that
A1071: [a1,a2] in Indices (Gauge C,n) and
A1072: f /. (m -' 1) = (Gauge C,n) * a1,a2 and
A1073: [p91,p92] in Indices (Gauge C,n) and
A1074: (Rev g) /. 1 = (Gauge C,n) * p91,p92 and
A1075: ( ( a1 = p91 & a2 + 1 = p92 ) or ( a1 + 1 = p91 & a2 = p92 ) or ( a1 = p91 + 1 & a2 = p92 ) or ( a1 = p91 & a2 = p92 + 1 ) ) by A652, A653, A948, A954, A955, JORDAN8:6;
A1076: a2 <= width (Gauge C,n) by A1071, MATRIX_1:39;
thus C meets LeftComp (Rev g) :: thesis:

proof

per cases by A1075;

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

then A1078: a2 + 1 = p2 by A939, A940, A1073, A1074, GOBOARD1:21;
A1079: a1 = p1 by A939, A940, A1073, A1074, A1077, GOBOARD1:21;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A565, A955, NAT_1:11
.= (Rev g) /. 2 by A709, A699, A565, A955, A942, A1070, A1072, A1079, A1078
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A565, A960, A961, A950
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A176 ;
hence C meets LeftComp (Rev g) by A647, A960, A961, A957, A935; :: thesis:

end;

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

then a2 = p2 by A939, A940, A1073, A1074, GOBOARD1:21;
then A1081: a2 -' 1 = q2 by A1070, NAT_D:34;
a1 + 1 = p1 by A939, A940, A1073, A1074, A1080, GOBOARD1:21;
then A1082: a1 = q1 -' 1 by A1070, NAT_D:34;
right_cell f,(m -' 1),(Gauge C,n) = cell (Gauge C,n),a1,(a2 -' 1) by A439, A653, A948, A954, A955, A1071, A1072, A1073, A1074, A1080, GOBRD13:25
.= left_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) by A439, A709, A952, A961, A950, A953, A939, A940, A941, A942, A1070, A1082, A1081, GOBRD13:22 ;
hence C meets LeftComp (Rev g) by A439, A653, A954, A955, A962; :: thesis:

end;

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

then a2 = p2 by A939, A940, A1073, A1074, GOBOARD1:21;
then A1084: a2 -' 1 = q2 by A1070, NAT_D:34;
A1085: a1 = p1 + 1 by A939, A940, A1073, A1074, A1083, GOBOARD1:21;
right_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) = cell (Gauge C,n),q1,q2 by A439, A709, A952, A961, A950, A953, A939, A940, A941, A942, A1070, GOBRD13:23
.= left_cell f,(m -' 1),(Gauge C,n) by A650, A652, A653, A701, A954, A955, A1070, A1071, A1072, A1073, A1074, A1083, A1085, A1084, FINSEQ_5:68, GOBRD13:26 ;
hence C meets LeftComp (Rev g) by A439, A709, A959, A961, A956; :: thesis:

end;

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

then A1087: a2 = p2 + 1 by A939, A940, A1073, A1074, GOBOARD1:21;
A1088: f /. ((m -' 1) + 1) = (F . m) /. m by A709, A651, A653, A565, A954;
A1089: 2 in dom g by A702, FINSEQ_3:27;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A930, FINSEQ_5:def 3;
then A1090: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A1089, FINSEQ_5:69
.= f /. (m + 1) by A932, A1089, FINSEQ_5:30 ;
A1091: (p1 -' 1) + 1 = p1 by A944, XREAL_1:237;
A1092: m -' 1 <= m by A954, NAT_1:11;
A1093: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A709, A699, A565, A955
.= (F . m) /. (m -' 1) by A565, A955, A1092 ;
A1094: p2 -' 1 = q2 by A1070, NAT_D:34;
set rc = (left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g));
A1095: p2 + 1 > p2 by NAT_1:13;
A1096: (Rev g) /. 1 = g /. 1 by A650, A737, A701, FINSEQ_5:68
.= (Rev g) /. (len g) by FINSEQ_5:68
.= (Rev g) /. (len (Rev g)) by FINSEQ_5:def 3 ;
A1097: (m -' 1) + 1 <= len (F . m) by A176, A954;
A1098: (F . k) | (m + 1) = F . (m + 1) by A564, A709, A658;
A1099: L~ (Rev g) c= L~ f by A897, SPPOL_2:22;
A1100: a1 = p1 by A939, A940, A1073, A1074, A1086, GOBOARD1:21;
left_cell f,((m -' 1) + ((len g) -' 1)),(Gauge C,n) = cell (Gauge C,n),(q1 -' 1),q2 by A439, A709, A952, A961, A950, A953, A939, A940, A941, A942, A1070, GOBRD13:22
.= front_right_cell (F . m),(m -' 1),(Gauge C,n) by A439, A948, A954, A955, A939, A940, A1070, A1071, A1072, A1100, A1087, A1094, A1097, A1093, A1088, GOBRD13:42 ;
then F . (m + 1) turns_right m -' 1, Gauge C,n by A513, A900, A962;
then A1101: f turns_right m -' 1, Gauge C,n by A955, A932, A1098, GOBRD13:44;
A1102: a2 + 1 > p2 + 1 by A1087, NAT_1:13;
then A1103: [(p1 -' 1),p2] in Indices (Gauge C,n) by A948, A954, A939, A940, A1071, A1072, A1095, A1101, GOBRD13:def 6;
then A1104: 1 <= p1 -' 1 by MATRIX_1:39;
f /. (m + 1) = (Gauge C,n) * (p1 -' 1),p2 by A948, A954, A932, A939, A940, A1071, A1072, A1102, A1095, A1101, GOBRD13:def 6;
then left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) = cell (Gauge C,n),(p1 -' 1),p2 by A938, A937, A951, A939, A940, A1103, A1090, A1096, A1091, GOBRD13:24;
then f /. (m -' 1) in left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n) by A946, A947, A1072, A1076, A1100, A1087, A1104, A1091, JORDAN9:22;
then A1105: f /. (m -' 1) in (left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g)) by A958, XBOOLE_0:def 5;
A1106: LeftComp (Rev g) is_a_component_of (L~ (Rev g)) ` by GOBOARD9:def 1;
(left_cell (Rev g),((len (Rev g)) -' 1),(Gauge C,n)) \ (L~ (Rev g)) c= LeftComp (Rev g) by A938, A937, A951, JORDAN9:29;
hence C meets LeftComp (Rev g) by A653, A659, A954, A955, A958, A1105, A1099, A1106; :: thesis:

end;

then C meets RightComp g by GOBOARD9:26;
hence contradiction by A875, A884, A898, A886, JORDAN9:3, SPRECT_4:7; :: thesis:

end;

then A1107: g = f /^ 0 by XREAL_1:234
.= f by FINSEQ_5:31 ;
then reconsider f = f as non constant standard special_circular_sequence ;
F . (0 + 1) = <*((Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n))*> by A156;
then A1108: (Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n) = (F . 1) /. 1 by FINSEQ_4:25
.= f /. 1 by A646, A565 ;
F . (1 + 1) = <*((Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n)),((Gauge C,n) * ((X-SpanStart C,n) -' 1),(Y-SpanStart C,n))*> by A156;
then A1109: (Gauge C,n) * ((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) = (F . 2) /. 2 by FINSEQ_4:26
.= f /. 2 by A656, A565 ;
A1110: 2 < X-SpanStart C,n by JORDAN1H:58;
f is clockwise_oriented

proof

LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
then C c= LeftComp f by A875, A886, A1107, GOBOARD9:6;
then RightComp f misses C by GOBRD14:24, XBOOLE_1:63;
then A1111: RightComp f c= C ` by SUBSET_1:43;
A1112: L~ f is Bounded by JORDAN2C:73;
UBD (L~ f) is_outside_component_of L~ f by JORDAN2C:73, JORDAN2C:76;
then UBD (L~ f) is_a_component_of (L~ f) ` by JORDAN2C:def 4;
then A1113: ( UBD (L~ f) = RightComp f or UBD (L~ f) = LeftComp f ) by JORDAN1H:30;
A1114: ((X-SpanStart C,n) -' 1) + 1 = X-SpanStart C,n by A1110, XREAL_1:237, XXREAL_0:2;
set W = { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } ;
A1115: Int (right_cell f,1,(Gauge C,n)) c= right_cell f,1,(Gauge C,n) by TOPS_1:44;
A1116: BDD C = union { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } by JORDAN2C:def 5;
A1117: Int (right_cell f,1,(Gauge C,n)) <> {} by A652, A655, JORDAN9:11;
A1118: [((X-SpanStart C,n) -' 1),(Y-SpanStart C,n)] in Indices (Gauge C,n) by A1, JORDAN11:9;
cell (Gauge C,n),((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) c= BDD C by A1, JORDAN11:6;
then right_cell f,1,(Gauge C,n) c= BDD C by A5, A439, A655, A1108, A1109, A1114, A1118, GOBRD13:27;
then A1119: Int (right_cell f,1,(Gauge C,n)) c= BDD C by A1115, XBOOLE_1:1;
Int (right_cell f,1,(Gauge C,n)) c= RightComp f by A652, A655, JORDAN1H:31;
then BDD C meets RightComp f by A1119, A1117, XBOOLE_1:68;
then consider e being set such that
A1120: e in { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } and
A1121: RightComp f meets e by A1116, ZFMISC_1:98;
consider B being Subset of (TOP-REAL 2) such that
A1122: e = B and
A1123: B is_inside_component_of C by A1120;
A1124: B is Bounded by A1123, JORDAN2C:def 3;
B is_a_component_of C ` by A1123, JORDAN2C:def 3;
then RightComp f is Bounded by A1121, A1122, A1111, A1124, GOBOARD9:6, JORDAN2C:16;
hence f is clockwise_oriented by A1113, A1112, JORDAN1H:47, JORDAN1H:49; :: 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 A439; :: thesis:
thus f /. 1 = (Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n) by A1108; :: thesis:
thus f /. 2 = (Gauge C,n) * ((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) by A1109; :: thesis:
let m be Element of NAT ; :: thesis:
assume that
A1125: 1 <= m and
A1126: m + 2 <= len f ; :: thesis:
A1127: F . ((m + 1) + 1) = f | ((m + 1) + 1) by A564, A709, A1126;
A1128: m + 1 < m + 2 by XREAL_1:8;
then A1129: f | (m + 1) = F . (m + 1) by A564, A709, A1126, XXREAL_0:2;
A1130: m + 1 <= len f by A1126, A1128, XXREAL_0:2;
then A1131: front_right_cell (F . (m + 1)),m,(Gauge C,n) = front_right_cell f,m,(Gauge C,n) by A652, A1125, A1129, GOBRD13:43;
A1132: m + 1 > 1 by A1125, NAT_1:13;
A1133: m = (m + 1) -' 1 by NAT_D:34;
A1134: front_left_cell (F . (m + 1)),m,(Gauge C,n) = front_left_cell f,m,(Gauge C,n) by A652, A1125, A1130, A1129, GOBRD13:43;

hereby :: thesis:

assume that
A1135: front_right_cell f,m,(Gauge C,n) misses C and
A1136: front_left_cell f,m,(Gauge C,n) misses C ; :: thesis:
F . ((m + 1) + 1) turns_left m, Gauge C,n by A513, A1133, A1132, A1131, A1134, A1135, A1136;
hence f turns_left m, Gauge C,n by A1125, A1126, A1127, GOBRD13:45; :: thesis:

end;

hereby :: thesis:

assume that
A1137: front_right_cell f,m,(Gauge C,n) misses C and
A1138: front_left_cell f,m,(Gauge C,n) meets C ; :: thesis:
F . ((m + 1) + 1) goes_straight m, Gauge C,n by A513, A1133, A1132, A1131, A1134, A1137, A1138;
hence f goes_straight m, Gauge C,n by A1125, A1126, A1127, GOBRD13:46; :: thesis:

end;

assume front_right_cell f,m,(Gauge C,n) meets C ; :: thesis:
then F . ((m + 1) + 1) turns_right m, Gauge C,n by A513, A1133, A1132, A1131;
hence f turns_right m, Gauge C,n by A1125, A1126, A1127, GOBRD13:44; :: thesis: