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

let k be Nat; :: thesis:
let x be set ; :: thesis:

per cases by NAT_1:25;

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:235;
then A15: ((len f) -' 1) + (1 + 1) = (len f) + 1 ;
A16: ((len f) -' 1) + 1 in dom f by A10, A12, A14, FINSEQ_3:25;
A17: 1 <= (len f) -' 1 by A10, A12, NAT_D:49;
then consider i1, j1, i2, j2 being 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:3;
A23: i1 <= len (Gauge (C,n)) by A18, MATRIX_0:32;
A24: 1 <= j2 + 1 by NAT_1:12;
A25: 1 <= i2 by A20, MATRIX_0:32;
A26: j1 <= width (Gauge (C,n)) by A18, MATRIX_0:32;
A27: 1 <= i2 + 1 by NAT_1:12;
A28: 1 <= j2 by A20, MATRIX_0:32;
(len f) -' 1 <= len f by NAT_D:35;
then A29: (len f) -' 1 in dom f by A17, FINSEQ_3:25;
A30: j2 <= width (Gauge (C,n)) by A20, MATRIX_0:32;
then A31: j2 -' 1 <= width (Gauge (C,n)) by NAT_D:44;
A32: i2 <= len (Gauge (C,n)) by A20, MATRIX_0:32;
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 :: thesis:

take i = i2 -' 1; :: thesis:
take j = j2; :: thesis:

now :: thesis:

A36: now :: thesis:

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:21;
then cell ((Gauge (C,n)),0,j1) meets C by XREAL_1:232;
hence contradiction by A6, A26, JORDAN8:18; :: thesis:

end;

let i19, j19, i29, j29 be 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:68;
A42: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A16, A40, FINSEQ_4:68;
then A43: j2 = j29 by A20, A21, A38, GOBOARD1:5;
i2 = i29 by A20, A21, A38, A42, GOBOARD1:5;
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:67, GOBOARD1:5, MATRIX_0:30; :: 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 :: thesis:

take i = i2; :: thesis:
take j = j2 + 1; :: thesis:

now :: thesis:

A45: now :: thesis:

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:6;
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:23;
hence contradiction by A23, JORDAN8:15; :: thesis:

end;

let i19, j19, i29, j29 be 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:68;
A52: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A16, A50, FINSEQ_4:68;
then A53: j2 = j29 by A20, A21, A48, GOBOARD1:5;
i2 = i29 by A20, A21, A48, A52, GOBOARD1:5;
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:67, GOBOARD1:5, MATRIX_0:30; :: 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 :: thesis:

take i = i2; :: thesis:
take j = j2 -' 1; :: thesis:

now :: thesis:

A55: now :: thesis:

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:25;
then cell ((Gauge (C,n)),i2,0) meets C by XREAL_1:232;
hence contradiction by A32, JORDAN8:17; :: thesis:

end;

let i19, j19, i29, j29 be 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:68;
A61: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A16, A59, FINSEQ_4:68;
then A62: j2 = j29 by A20, A21, A57, GOBOARD1:5;
i2 = i29 by A20, A21, A57, A61, GOBOARD1:5;
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:67, GOBOARD1:5, MATRIX_0:30; :: 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 :: thesis:

take i = i2 + 1; :: thesis:
take j = j2; :: thesis:

now :: thesis:

A64: now :: thesis:

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:6;
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:27;
hence contradiction by A6, A30, JORDAN8:16; :: thesis:

end;

let i19, j19, i29, j29 be 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:68;
A71: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A16, A69, FINSEQ_4:68;
then A72: j2 = j29 by A20, A21, A67, GOBOARD1:5;
i2 = i29 by A20, A21, A67, A71, GOBOARD1:5;
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:67, GOBOARD1:5, MATRIX_0:30; :: 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 :: thesis:

take i = i2; :: thesis:
take j = j2 + 1; :: thesis:

now :: thesis:

A75: now :: thesis:

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:6;
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:34;
hence contradiction by A23, JORDAN8:15, NAT_D:44; :: thesis:

end;

let i19, j19, i29, j29 be 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:68;
A82: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A16, A80, FINSEQ_4:68;
then A83: j2 = j29 by A20, A21, A78, GOBOARD1:5;
i2 = i29 by A20, A21, A78, A82, GOBOARD1:5;
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:67, GOBOARD1:5, MATRIX_0:30; :: 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 :: thesis:

take i = i2 + 1; :: thesis:
take j = j2; :: thesis:

now :: thesis:

A85: now :: thesis:

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:6;
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:36;
hence contradiction by A6, A26, JORDAN8:16; :: thesis:

end;

let i19, j19, i29, j29 be 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:68;
A92: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A16, A90, FINSEQ_4:68;
then A93: j2 = j29 by A20, A21, A88, GOBOARD1:5;
i2 = i29 by A20, A21, A88, A92, GOBOARD1:5;
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:67, GOBOARD1:5, MATRIX_0:30; :: 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 :: thesis:

take i = i2 -' 1; :: thesis:
take j = j2; :: thesis:

now :: thesis:

A95: now :: thesis:

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:38;
then cell ((Gauge (C,n)),0,(j1 -' 1)) meets C by XREAL_1:232;
hence contradiction by A6, A26, JORDAN8:18, NAT_D:44; :: thesis:

end;

let i19, j19, i29, j29 be 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:68;
A101: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A16, A99, FINSEQ_4:68;
then A102: j2 = j29 by A20, A21, A97, GOBOARD1:5;
i2 = i29 by A20, A21, A97, A101, GOBOARD1:5;
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:67, GOBOARD1:5, MATRIX_0:30; :: 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 :: thesis:

take i = i2; :: thesis:
take j = j2 -' 1; :: thesis:

now :: thesis:

A104: now :: thesis:

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

end;

let i19, j19, i29, j29 be 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:68;
A110: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A16, A108, FINSEQ_4:68;
then A111: j2 = j29 by A20, A21, A106, GOBOARD1:5;
i2 = i29 by A20, A21, A106, A110, GOBOARD1:5;
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:67, GOBOARD1:5, MATRIX_0:30; :: 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 :: thesis:

take i = i2 + 1; :: thesis:
take j = j2; :: thesis:

now :: thesis:

A114: now :: thesis:

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:6;
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:35;
hence contradiction by A6, A30, JORDAN8:16; :: thesis:

end;

let i19, j19, i29, j29 be 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:68;
A121: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A16, A119, FINSEQ_4:68;
then A122: j2 = j29 by A20, A21, A117, GOBOARD1:5;
i2 = i29 by A20, A21, A117, A121, GOBOARD1:5;
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:67, GOBOARD1:5, MATRIX_0:30; :: 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 :: thesis:

take i = i2; :: thesis:
take j = j2 -' 1; :: thesis:

now :: thesis:

A124: now :: thesis:

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:37;
then cell ((Gauge (C,n)),i2,0) meets C by XREAL_1:232;
hence contradiction by A32, JORDAN8:17; :: thesis:

end;

let i19, j19, i29, j29 be 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:68;
A130: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A16, A128, FINSEQ_4:68;
then A131: j2 = j29 by A20, A21, A126, GOBOARD1:5;
i2 = i29 by A20, A21, A126, A130, GOBOARD1:5;
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:67, GOBOARD1:5, MATRIX_0:30; :: 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 :: thesis:

take i = i2; :: thesis:
take j = j2 + 1; :: thesis:

now :: thesis:

A133: now :: thesis:

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:6;
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:39;
hence contradiction by A32, JORDAN8:15, NAT_D:44; :: thesis:

end;

let i19, j19, i29, j29 be 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:68;
A140: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A16, A138, FINSEQ_4:68;
then A141: j2 = j29 by A20, A21, A136, GOBOARD1:5;
i2 = i29 by A20, A21, A136, A140, GOBOARD1:5;
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:67, GOBOARD1:5, MATRIX_0:30; :: 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 :: thesis:

take i = i2 -' 1; :: thesis:
take j = j2; :: thesis:

now :: thesis:

A143: now :: thesis:

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:41;
then cell ((Gauge (C,n)),0,(j2 -' 1)) meets C by XREAL_1:232;
hence contradiction by A6, A30, JORDAN8:18, NAT_D:44; :: thesis:

end;

let i19, j19, i29, j29 be 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:68;
A149: f /. (((len f) -' 1) + 1) = (Gauge (C,n)) * (i29,j29) by A16, A147, FINSEQ_4:68;
then A150: j2 = j29 by A20, A21, A145, GOBOARD1:5;
i2 = i29 by A20, A21, A145, A149, GOBOARD1:5;
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:67, GOBOARD1:5, MATRIX_0:30; :: 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 Nat holds S₁[k,F . k,F . (k + 1)] from RECDEF_1:sch 1(A7);
defpred S₂[ Nat] means F . $1 is FinSequence of (TOP-REAL 2);
A157: {} = <*> the carrier of (TOP-REAL 2) ;
A158: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

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

per cases by NAT_1:25;

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:

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

per cases ;

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

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 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 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 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 A166: len f <> k ; :: thesis:

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

end;

A167: S₂[ 0 ] by A155, A157;
A168: for k being Nat holds S₂[k] from NAT_1:sch 2(A167, A158);
rng F c= the carrier of (TOP-REAL 2) *

proof

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

end;

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

proof

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

per cases by NAT_1:25;

suppose k = 0 ; :: thesis:

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

end;

suppose k = 1 ; :: thesis:

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

end;

suppose A172: k > 1 ; :: thesis:

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

proof

per cases ;

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

then A174: ( front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C implies ex i, j being Nat st
( (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_right (len (F . k)) -' 1, Gauge (C,n) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) ) by A156, A170, A172;
A175: ( 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 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, A170, A172, A173;
( 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 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, A170, A172, A173;
hence S₃[k + 1] by A170, A175, A174, FINSEQ_2:16; :: 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, A170, A172;
hence S₃[k + 1] by A170, FINSEQ_2:16; :: thesis:

end;

defpred S₄[ Nat] means ( F . $1 is_sequence_on Gauge (C,n) & ( for m being Nat st 1 <= m & m + 1 <= len (F . $1) holds
( right_cell ((F . $1),m,(Gauge (C,n))) misses C & left_cell ((F . $1),m,(Gauge (C,n))) meets C ) ) );
A176: S₃[ 0 ] by A155, CARD_1:27;
A177: for k being Nat holds S₃[k] from NAT_1:sch 2(A176, A169);
A178: 1 <= X-SpanStart (C,n) by JORDAN1H:49, XXREAL_0:2;
A179: for k being Nat st S₄[k] holds
S₄[k + 1]

proof

let k be Nat; :: thesis:
assume that
A180: F . k is_sequence_on Gauge (C,n) and
A181: for m being 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:
A182: len (F . k) = k by A177;
A183: len (F . (k + 1)) = k + 1 by A177;

per cases by NAT_1:25;

suppose A184: k = 0 ; :: thesis:

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

A186: now :: thesis:

let l be Nat; :: thesis:
assume A187: l in dom (F . (k + 1)) ; :: thesis:
then A188: 1 <= l by FINSEQ_3:25;
l <= 1 by A183, A184, A187, FINSEQ_3:25;
then l = 1 by A188, XXREAL_0:1;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & (F . (k + 1)) /. l = (Gauge (C,n)) * (i,j) ) by A5, A185, FINSEQ_4:16; :: thesis:

end;

now :: thesis:

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

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A186, GOBOARD1:def 9; :: thesis:
let m be Nat; :: thesis:
assume that
A192: 1 <= m and
A193: m + 1 <= len (F . (k + 1)) ; :: thesis:
1 <= m + 1 by NAT_1:12;
then m + 1 = 0 + 1 by A183, A184, A193, 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 A192; :: thesis:

end;

suppose A194: k = 1 ; :: thesis:

A195: (X-SpanStart (C,n)) -' 1 < X-SpanStart (C,n) by A178, JORDAN5B:1;
A196: X-SpanStart (C,n) <= (X-SpanStart (C,n)) + 1 by NAT_1:11;
A197: [(X-SpanStart (C,n)),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A1, JORDAN11:8;
A198: 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, A194;
then A199: (F . (k + 1)) /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) by FINSEQ_4:17;
A200: [((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A1, JORDAN11:9;
A201: (F . (k + 1)) /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A198, FINSEQ_4:17;

A202: now :: thesis:

let l be Nat; :: thesis:
assume that
A203: l in dom (F . (k + 1)) and
A204: l + 1 in dom (F . (k + 1)) ; :: thesis:
let i1, j1, i2, j2 be Nat; :: thesis:
assume that
A205: [i1,j1] in Indices (Gauge (C,n)) and
A206: [i2,j2] in Indices (Gauge (C,n)) and
A207: (F . (k + 1)) /. l = (Gauge (C,n)) * (i1,j1) and
A208: (F . (k + 1)) /. (l + 1) = (Gauge (C,n)) * (i2,j2) ; :: thesis:
l <= 2 by A183, A194, A203, FINSEQ_3:25;
then A209: not not l = 0 & ... & not l = 2 ;
then A210: i2 = (X-SpanStart (C,n)) -' 1 by A183, A194, A201, A200, A203, A204, A206, A208, FINSEQ_3:25, GOBOARD1:5;
A211: j1 = Y-SpanStart (C,n) by A199, A201, A197, A200, A203, A209, A205, A207, FINSEQ_3:25, GOBOARD1:5;
j2 = Y-SpanStart (C,n) by A183, A194, A199, A201, A197, A200, A204, A209, A206, A208, FINSEQ_3:25, GOBOARD1:5;
then A212: |.(j1 - j2).| = 0 by A211, ABSVALUE:def 1;
i1 = X-SpanStart (C,n) by A183, A194, A199, A197, A203, A204, A209, A205, A207, FINSEQ_3:25, GOBOARD1:5;
then i2 + 1 = i1 by A3, A210, NAT_D:43, NAT_D:55;
hence |.(i1 - i2).| + |.(j1 - j2).| = 1 by A212, ABSVALUE:def 1; :: thesis:

end;

now :: thesis:

let l be Nat; :: thesis:
assume A213: l in dom (F . (k + 1)) ; :: thesis:
then l <= 2 by A183, A194, FINSEQ_3:25;
then not not l = 0 & ... & not l = 2 ;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & (F . (k + 1)) /. l = (Gauge (C,n)) * (i,j) ) by A199, A201, A197, A200, A213, FINSEQ_3:25; :: thesis:

end;

hence A214: F . (k + 1) is_sequence_on Gauge (C,n) by A202, GOBOARD1:def 9; :: thesis:
let m be Nat; :: thesis:
assume that
A215: 1 <= m and
A216: m + 1 <= len (F . (k + 1)) ; :: thesis:
1 + 1 <= m + 1 by A215, XREAL_1:6;
then A217: m + 1 = 1 + 1 by A183, A194, A216, 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 A199, A201, A197, A200, A214, A216, A195, A196, 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 A199, A201, A197, A200, A214, A216, A217, A195, A196, GOBRD13:def 3;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A1, JORDAN11:10; :: thesis:

end;

suppose A218: k > 1 ; :: thesis:

then A219: len (F . k) in dom (F . k) by A182, FINSEQ_3:25;
A220: ((len (F . k)) -' 1) + 1 = len (F . k) by A182, A218, XREAL_1:235;
then A221: ((len (F . k)) -' 1) + (1 + 1) = (len (F . k)) + 1 ;
A222: 1 <= (len (F . k)) -' 1 by A182, A218, NAT_D:49;
then consider i1, j1, i2, j2 being Nat such that
A223: [i1,j1] in Indices (Gauge (C,n)) and
A224: (F . k) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) and
A225: [i2,j2] in Indices (Gauge (C,n)) and
A226: (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 A180, A220, JORDAN8:3;
A227: ( 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 A180, A182, A218, A223, A224, A225, A226, JORDAN1H:58;
(i1 + 1) + 1 = i1 + 2 ;
then A228: ( 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 A180, A182, A218, A223, A224, A225, A226, JORDAN1H:57;
(j1 + 1) + 1 = j1 + 2 ;
then A229: ( 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 A180, A182, A218, A223, A224, A225, A226, JORDAN1H:56;
A230: ( 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 A180, A182, A218, A223, A224, A225, A226, JORDAN1H:63;
(len (F . k)) -' 1 <= len (F . k) by NAT_D:35;
then A231: (len (F . k)) -' 1 in dom (F . k) by A222, FINSEQ_3:25;
A232: ( 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 A180, A182, A218, A223, A224, A225, A226, JORDAN1H:62;
A233: ( 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 A180, A182, A218, A223, A224, A225, A226, JORDAN1H:61;
A234: ( 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 A180, A182, A218, A223, A224, A225, A226, JORDAN1H:60;
A235: ( 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 A180, A182, A218, A223, A224, A225, A226, JORDAN1H:59;
A236: 1 <= j2 by A225, MATRIX_0:32;
A237: left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C by A181, A222, A220;
then A238: ( i1 = i2 & j1 + 1 = j2 implies [(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n)) ) by A180, A182, A218, A223, A224, A225, A226, JORDAN1H:52;
A239: ( i1 = i2 & j1 = j2 + 1 implies [(i1 + 1),j2] in Indices (Gauge (C,n)) ) by A180, A182, A218, A223, A224, A225, A226, A237, JORDAN1H:55;
A240: ( i1 = i2 + 1 & j1 = j2 implies [i2,(j1 -' 1)] in Indices (Gauge (C,n)) ) by A180, A182, A218, A223, A224, A225, A226, A237, JORDAN1H:54;
A241: ( i1 + 1 = i2 & j1 = j2 implies [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) ) by A180, A182, A218, A223, A224, A225, A226, A237, JORDAN1H:53;
A242: 1 <= i2 by A225, MATRIX_0:32;
thus A243: 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 Nat such that
A244: (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_left (len (F . k)) -' 1, Gauge (C,n) and
A245: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A156, A180, A182, A218, A237;
set f = (F . k) ^ <*((Gauge (C,n)) * (i,j))*>;
A246: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i,j) by FINSEQ_4:67;
A247: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) by A226, A219, FINSEQ_4:68;
A248: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) by A224, A231, FINSEQ_4:68;
thus F . (k + 1) is_sequence_on Gauge (C,n) :: thesis:

proof

per cases by A220, A223, A225, A221, A244, A248, A247, GOBRD13:def 7;

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

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A251: [i19,j19] in Indices (Gauge (C,n)) and
A252: [i29,j29] in Indices (Gauge (C,n)) and
A253: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) and
A254: (Gauge (C,n)) * ((i2 -' 1),j2) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A255: i2 -' 1 = i29 by A238, A249, A252, A254, GOBOARD1:5;
i2 = i19 by A225, A226, A251, A253, GOBOARD1:5;
then i19 - i29 = i2 - (i2 - 1) by A242, A255, XREAL_1:233;
then A256: |.(i19 - i29).| = 1 by ABSVALUE:def 1;
A257: j2 = j29 by A238, A249, A252, A254, GOBOARD1:5;
j2 = j19 by A225, A226, A251, A253, GOBOARD1:5;
then |.(j29 - j19).| = 0 by A257, ABSVALUE:def 1;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A256, UNIFORM1:11; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A180, A182, A218, A238, A245, A246, A249, A250, CARD_1:27, JORDAN8:6; :: thesis:

end;

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

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A260: [i19,j19] in Indices (Gauge (C,n)) and
A261: [i29,j29] in Indices (Gauge (C,n)) and
A262: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) and
A263: (Gauge (C,n)) * (i2,(j2 + 1)) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A264: i2 = i29 by A241, A258, A261, A263, GOBOARD1:5;
i2 = i19 by A225, A226, A260, A262, GOBOARD1:5;
then A265: |.(i29 - i19).| = 0 by A264, ABSVALUE:def 1;
A266: j2 + 1 = j29 by A241, A258, A261, A263, GOBOARD1:5;
j2 = j19 by A225, A226, A260, A262, GOBOARD1:5;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A266, A265, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A180, A182, A218, A241, A245, A246, A258, A259, CARD_1:27, JORDAN8:6; :: thesis:

end;

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

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A269: [i19,j19] in Indices (Gauge (C,n)) and
A270: [i29,j29] in Indices (Gauge (C,n)) and
A271: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) and
A272: (Gauge (C,n)) * (i2,(j2 -' 1)) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A273: j2 -' 1 = j29 by A240, A267, A270, A272, GOBOARD1:5;
j2 = j19 by A225, A226, A269, A271, GOBOARD1:5;
then j19 - j29 = j2 - (j2 - 1) by A236, A273, XREAL_1:233;
then A274: |.(j19 - j29).| = 1 by ABSVALUE:def 1;
A275: i2 = i29 by A240, A267, A270, A272, GOBOARD1:5;
i2 = i19 by A225, A226, A269, A271, GOBOARD1:5;
then |.(i29 - i19).| = 0 by A275, ABSVALUE:def 1;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A274, UNIFORM1:11; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A180, A182, A218, A240, A245, A246, A267, A268, CARD_1:27, JORDAN8:6; :: thesis:

end;

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

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A278: [i19,j19] in Indices (Gauge (C,n)) and
A279: [i29,j29] in Indices (Gauge (C,n)) and
A280: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) and
A281: (Gauge (C,n)) * ((i2 + 1),j2) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A282: j2 = j29 by A239, A276, A279, A281, GOBOARD1:5;
j2 = j19 by A225, A226, A278, A280, GOBOARD1:5;
then A283: |.(j29 - j19).| = 0 by A282, ABSVALUE:def 1;
A284: i2 + 1 = i29 by A239, A276, A279, A281, GOBOARD1:5;
i2 = i19 by A225, A226, A278, A280, GOBOARD1:5;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A284, A283, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A180, A182, A218, A239, A245, A246, A276, A277, CARD_1:27, JORDAN8:6; :: thesis:

end;

suppose A285: ( 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 Nat such that
A286: (F . k) ^ <*((Gauge (C,n)) * (i,j))*> goes_straight (len (F . k)) -' 1, Gauge (C,n) and
A287: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A156, A180, A182, A218, A237;
set f = (F . k) ^ <*((Gauge (C,n)) * (i,j))*>;
A288: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i,j) by FINSEQ_4:67;
A289: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) by A226, A219, FINSEQ_4:68;
A290: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) by A224, A231, FINSEQ_4:68;
thus F . (k + 1) is_sequence_on Gauge (C,n) :: thesis:

proof

per cases by A220, A223, A225, A221, A286, A290, A289, GOBRD13:def 8;

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

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A293: [i19,j19] in Indices (Gauge (C,n)) and
A294: [i29,j29] in Indices (Gauge (C,n)) and
A295: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) and
A296: (Gauge (C,n)) * (i2,(j2 + 1)) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A297: i2 = i19 by A225, A226, A293, A295, GOBOARD1:5;
i2 = i29 by A229, A285, A291, A294, A296, GOBOARD1:5;
then A298: |.(i29 - i19).| = 0 by A297, ABSVALUE:def 1;
A299: j2 = j19 by A225, A226, A293, A295, GOBOARD1:5;
j2 + 1 = j29 by A229, A285, A291, A294, A296, GOBOARD1:5;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A299, A298, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A180, A182, A218, A229, A285, A287, A288, A291, A292, CARD_1:27, JORDAN8:6; :: thesis:

end;

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

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A302: [i19,j19] in Indices (Gauge (C,n)) and
A303: [i29,j29] in Indices (Gauge (C,n)) and
A304: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) and
A305: (Gauge (C,n)) * ((i2 + 1),j2) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A306: j2 = j19 by A225, A226, A302, A304, GOBOARD1:5;
j2 = j29 by A228, A285, A300, A303, A305, GOBOARD1:5;
then A307: |.(j29 - j19).| = 0 by A306, ABSVALUE:def 1;
A308: i2 = i19 by A225, A226, A302, A304, GOBOARD1:5;
i2 + 1 = i29 by A228, A285, A300, A303, A305, GOBOARD1:5;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A308, A307, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A180, A182, A218, A228, A285, A287, A288, A300, A301, CARD_1:27, JORDAN8:6; :: thesis:

end;

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

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A311: [i19,j19] in Indices (Gauge (C,n)) and
A312: [i29,j29] in Indices (Gauge (C,n)) and
A313: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) and
A314: (Gauge (C,n)) * ((i2 -' 1),j2) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A315: i2 = i19 by A225, A226, A311, A313, GOBOARD1:5;
i2 -' 1 = i29 by A227, A285, A309, A312, A314, GOBOARD1:5;
then i19 - i29 = i2 - (i2 - 1) by A242, A315, XREAL_1:233;
then A316: |.(i19 - i29).| = 1 by ABSVALUE:def 1;
A317: j2 = j19 by A225, A226, A311, A313, GOBOARD1:5;
j2 = j29 by A227, A285, A309, A312, A314, GOBOARD1:5;
then |.(j29 - j19).| = 0 by A317, ABSVALUE:def 1;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A316, UNIFORM1:11; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A180, A182, A218, A227, A285, A287, A288, A309, A310, CARD_1:27, JORDAN8:6; :: thesis:

end;

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

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A320: [i19,j19] in Indices (Gauge (C,n)) and
A321: [i29,j29] in Indices (Gauge (C,n)) and
A322: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) and
A323: (Gauge (C,n)) * (i2,(j2 -' 1)) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A324: j2 = j19 by A225, A226, A320, A322, GOBOARD1:5;
j2 -' 1 = j29 by A235, A285, A318, A321, A323, GOBOARD1:5;
then j19 - j29 = j2 - (j2 - 1) by A236, A324, XREAL_1:233;
then A325: |.(j19 - j29).| = 1 by ABSVALUE:def 1;
A326: i2 = i19 by A225, A226, A320, A322, GOBOARD1:5;
i2 = i29 by A235, A285, A318, A321, A323, GOBOARD1:5;
then |.(i29 - i19).| = 0 by A326, ABSVALUE:def 1;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A325, UNIFORM1:11; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A180, A182, A218, A235, A285, A287, A288, A318, A319, CARD_1:27, JORDAN8:6; :: thesis:

end;

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

then consider i, j being Nat such that
A328: (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_right (len (F . k)) -' 1, Gauge (C,n) and
A329: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A156, A180, A182, A218, A237;
set f = (F . k) ^ <*((Gauge (C,n)) * (i,j))*>;
A330: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i,j) by FINSEQ_4:67;
A331: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) by A226, A219, FINSEQ_4:68;
A332: ((F . k) ^ <*((Gauge (C,n)) * (i,j))*>) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) by A224, A231, FINSEQ_4:68;
thus F . (k + 1) is_sequence_on Gauge (C,n) :: thesis:

proof

per cases by A220, A223, A225, A221, A328, A332, A331, GOBRD13:def 6;

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

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A335: [i19,j19] in Indices (Gauge (C,n)) and
A336: [i29,j29] in Indices (Gauge (C,n)) and
A337: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) and
A338: (Gauge (C,n)) * ((i2 + 1),j2) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A339: j2 = j19 by A225, A226, A335, A337, GOBOARD1:5;
j2 = j29 by A234, A327, A333, A336, A338, GOBOARD1:5;
then A340: |.(j29 - j19).| = 0 by A339, ABSVALUE:def 1;
A341: i2 = i19 by A225, A226, A335, A337, GOBOARD1:5;
i2 + 1 = i29 by A234, A327, A333, A336, A338, GOBOARD1:5;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A341, A340, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A180, A182, A218, A234, A327, A329, A330, A333, A334, CARD_1:27, JORDAN8:6; :: thesis:

end;

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

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A344: [i19,j19] in Indices (Gauge (C,n)) and
A345: [i29,j29] in Indices (Gauge (C,n)) and
A346: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) and
A347: (Gauge (C,n)) * (i2,(j2 -' 1)) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A348: j2 = j19 by A225, A226, A344, A346, GOBOARD1:5;
j2 -' 1 = j29 by A233, A327, A342, A345, A347, GOBOARD1:5;
then j19 - j29 = j2 - (j2 - 1) by A236, A348, XREAL_1:233;
then A349: |.(j19 - j29).| = 1 by ABSVALUE:def 1;
A350: i2 = i19 by A225, A226, A344, A346, GOBOARD1:5;
i2 = i29 by A233, A327, A342, A345, A347, GOBOARD1:5;
then |.(i29 - i19).| = 0 by A350, ABSVALUE:def 1;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A349, UNIFORM1:11; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A180, A182, A218, A233, A327, A329, A330, A342, A343, CARD_1:27, JORDAN8:6; :: thesis:

end;

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

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A353: [i19,j19] in Indices (Gauge (C,n)) and
A354: [i29,j29] in Indices (Gauge (C,n)) and
A355: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) and
A356: (Gauge (C,n)) * (i2,(j2 + 1)) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A357: i2 = i19 by A225, A226, A353, A355, GOBOARD1:5;
i2 = i29 by A232, A327, A351, A354, A356, GOBOARD1:5;
then A358: |.(i29 - i19).| = 0 by A357, ABSVALUE:def 1;
A359: j2 = j19 by A225, A226, A353, A355, GOBOARD1:5;
j2 + 1 = j29 by A232, A327, A351, A354, A356, GOBOARD1:5;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A359, A358, ABSVALUE:def 1; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A180, A182, A218, A232, A327, A329, A330, A351, A352, CARD_1:27, JORDAN8:6; :: thesis:

end;

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

now :: thesis:

let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A362: [i19,j19] in Indices (Gauge (C,n)) and
A363: [i29,j29] in Indices (Gauge (C,n)) and
A364: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i19,j19) and
A365: (Gauge (C,n)) * ((i2 -' 1),j2) = (Gauge (C,n)) * (i29,j29) ; :: thesis:
A366: i2 = i19 by A225, A226, A362, A364, GOBOARD1:5;
i2 -' 1 = i29 by A230, A327, A360, A363, A365, GOBOARD1:5;
then i19 - i29 = i2 - (i2 - 1) by A242, A366, XREAL_1:233;
then A367: |.(i19 - i29).| = 1 by ABSVALUE:def 1;
A368: j2 = j19 by A225, A226, A362, A364, GOBOARD1:5;
j2 = j29 by A230, A327, A360, A363, A365, GOBOARD1:5;
then |.(j29 - j19).| = 0 by A368, ABSVALUE:def 1;
hence |.(i29 - i19).| + |.(j29 - j19).| = 1 by A367, UNIFORM1:11; :: thesis:

end;

hence F . (k + 1) is_sequence_on Gauge (C,n) by A180, A182, A218, A230, A327, A329, A330, A360, A361, CARD_1:27, JORDAN8:6; :: thesis:

end;

let m be Nat; :: thesis:
assume that
A369: 1 <= m and
A370: m + 1 <= len (F . (k + 1)) ; :: thesis:
A371: right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C by A181, A222, A220;

now :: thesis:

per cases ;

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

A373: (j2 -' 1) + 1 = j2 by A236, XREAL_1:235;
A374: (i2 -' 1) + 1 = i2 by A242, XREAL_1:235;
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 A375: ( 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 A376: ex i, j being Nat st
( (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_left (len (F . k)) -' 1, Gauge (C,n) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A156, A180, A182, A218, A237;
then A377: (F . (k + 1)) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) by A226, A219, FINSEQ_4:68;
A378: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) by A224, A231, A376, FINSEQ_4:68;

now :: thesis:

per cases by A220, A223, A225, A221, A376, A378, A377, GOBRD13:def 7;

suppose that A379: ( i1 = i2 & j1 + 1 = j2 ) and
A380: (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 A180, A222, A220, A223, A224, A225, A226, A379, GOBRD13:34;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A182, A183, A225, A238, A243, A369, A372, A374, A375, A377, A379, A380, GOBRD13:26; :: thesis:
A381: j2 -' 1 = j1 by A379, NAT_D:34;
cell ((Gauge (C,n)),(i1 -' 1),j1) meets C by A180, A222, A220, A223, A224, A225, A226, A237, A379, GOBRD13:21;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A182, A183, A225, A238, A243, A369, A372, A374, A377, A379, A380, A381, GOBRD13:25; :: thesis:

end;

suppose that A382: ( i1 + 1 = i2 & j1 = j2 ) and
A383: (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 A180, A222, A220, A223, A224, A225, A226, A382, GOBRD13:36;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A182, A183, A225, A241, A243, A369, A372, A375, A377, A382, A383, GOBRD13:22; :: thesis:
A384: (i1 + 1) -' 1 = i1 by NAT_D:34;
cell ((Gauge (C,n)),i1,j1) meets C by A180, A222, A220, A223, A224, A225, A226, A237, A382, GOBRD13:23;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A182, A183, A225, A241, A243, A369, A372, A377, A382, A383, A384, GOBRD13:21; :: thesis:

end;

suppose that A385: ( i1 = i2 + 1 & j1 = j2 ) and
A386: (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 A180, A222, A220, A223, A224, A225, A226, A385, GOBRD13:38;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A182, A183, A225, A240, A243, A369, A372, A373, A375, A377, A385, A386, GOBRD13:28; :: thesis:
cell ((Gauge (C,n)),i2,(j2 -' 1)) meets C by A180, A222, A220, A223, A224, A225, A226, A237, A385, GOBRD13:25;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A182, A183, A225, A240, A243, A369, A372, A373, A377, A385, A386, GOBRD13:27; :: thesis:

end;

suppose that A387: ( i1 = i2 & j1 = j2 + 1 ) and
A388: (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 A180, A222, A220, A223, A224, A225, A226, A387, GOBRD13:40;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A182, A183, A225, A239, A243, A369, A372, A375, A377, A387, A388, GOBRD13:24; :: thesis:
cell ((Gauge (C,n)),i2,j2) meets C by A180, A222, A220, A223, A224, A225, A226, A237, A387, GOBRD13:27;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A182, A183, A225, A239, A243, A369, A372, A377, A387, A388, GOBRD13:23; :: 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 A389: ( 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 A390: ex i, j being Nat st
( (F . k) ^ <*((Gauge (C,n)) * (i,j))*> goes_straight (len (F . k)) -' 1, Gauge (C,n) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A156, A180, A182, A218, A237;
then A391: (F . (k + 1)) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) by A226, A219, FINSEQ_4:68;
A392: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) by A224, A231, A390, FINSEQ_4:68;

now :: thesis:

per cases by A220, A223, A225, A221, A390, A392, A391, GOBRD13:def 8;

suppose that A393: ( i1 = i2 & j1 + 1 = j2 ) and
A394: (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 A180, A222, A220, A223, A224, A225, A226, A393, GOBRD13:35;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A182, A183, A225, A229, A243, A369, A372, A389, A391, A393, A394, GOBRD13:22; :: thesis:
front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j2) by A180, A222, A220, A223, A224, A225, A226, A393, GOBRD13:34;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A182, A183, A225, A229, A243, A369, A372, A389, A391, A393, A394, GOBRD13:21; :: thesis:

end;

suppose that A395: ( i1 + 1 = i2 & j1 = j2 ) and
A396: (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 A180, A222, A220, A223, A224, A225, A226, A395, GOBRD13:37;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A182, A183, A225, A228, A243, A369, A372, A389, A391, A395, A396, GOBRD13:24; :: thesis:
front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) by A180, A222, A220, A223, A224, A225, A226, A395, GOBRD13:36;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A182, A183, A225, A228, A243, A369, A372, A389, A391, A395, A396, GOBRD13:23; :: thesis:

end;

suppose that A397: ( i1 = i2 + 1 & j1 = j2 ) and
A398: (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 A180, A222, A220, A223, A224, A225, A226, A397, GOBRD13:39;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A182, A183, A225, A227, A243, A369, A372, A374, A389, A391, A397, A398, GOBRD13:26; :: thesis:
front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) by A180, A222, A220, A223, A224, A225, A226, A397, GOBRD13:38;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A182, A183, A225, A227, A243, A369, A372, A374, A389, A391, A397, A398, GOBRD13:25; :: thesis:

end;

suppose that A399: ( i1 = i2 & j1 = j2 + 1 ) and
A400: (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 A180, A222, A220, A223, A224, A225, A226, A399, GOBRD13:41;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A182, A183, A225, A235, A243, A369, A372, A373, A389, A391, A399, A400, GOBRD13:28; :: thesis:
front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A180, A222, A220, A223, A224, A225, A226, A399, GOBRD13:40;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A182, A183, A225, A235, A243, A369, A372, A373, A389, A391, A399, A400, GOBRD13:27; :: 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 A401: front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ; :: thesis:

then A402: ex i, j being Nat st
( (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_right (len (F . k)) -' 1, Gauge (C,n) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A156, A180, A182, A218, A237;
then A403: (F . (k + 1)) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) by A226, A219, FINSEQ_4:68;
A404: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) by A224, A231, A402, FINSEQ_4:68;

now :: thesis:

per cases by A220, A223, A225, A221, A402, A404, A403, GOBRD13:def 6;

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

A407: j2 -' 1 = j1 by A405, NAT_D:34;
cell ((Gauge (C,n)),i1,j1) misses C by A180, A222, A220, A223, A224, A225, A226, A371, A405, GOBRD13:22;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A182, A183, A225, A234, A243, A369, A372, A401, A403, A405, A406, A407, GOBRD13:24; :: thesis:
front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) by A180, A222, A220, A223, A224, A225, A226, A405, GOBRD13:35;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A182, A183, A225, A234, A243, A369, A372, A401, A403, A405, A406, GOBRD13:23; :: thesis:

end;

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

A410: i2 -' 1 = i1 by A408, NAT_D:34;
cell ((Gauge (C,n)),i1,(j1 -' 1)) misses C by A180, A222, A220, A223, A224, A225, A226, A371, A408, GOBRD13:24;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A182, A183, A225, A233, A243, A369, A372, A373, A401, A403, A408, A409, A410, GOBRD13:28; :: thesis:
front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A180, A222, A220, A223, A224, A225, A226, A408, GOBRD13:37;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A182, A183, A225, A233, A243, A369, A372, A373, A401, A403, A408, A409, GOBRD13:27; :: thesis:

end;

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

cell ((Gauge (C,n)),i2,j2) misses C by A180, A222, A220, A223, A224, A225, A226, A371, A411, GOBRD13:26;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A182, A183, A225, A232, A243, A369, A372, A401, A403, A411, A412, GOBRD13:22; :: thesis:
front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),j2) by A180, A222, A220, A223, A224, A225, A226, A411, GOBRD13:39;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A182, A183, A225, A232, A243, A369, A372, A401, A403, A411, A412, GOBRD13:21; :: thesis:

end;

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

cell ((Gauge (C,n)),(i2 -' 1),j2) misses C by A180, A222, A220, A223, A224, A225, A226, A371, A413, GOBRD13:28;
hence right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C by A182, A183, A225, A230, A243, A369, A372, A374, A401, A403, A413, A414, GOBRD13:26; :: thesis:
front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) by A180, A222, A220, A223, A224, A225, A226, A413, GOBRD13:41;
hence left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C by A182, A183, A225, A230, A243, A369, A372, A374, A401, A403, A413, A414, GOBRD13:25; :: 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 A370, XXREAL_0:1;
then A415: m + 1 <= len (F . k) by A182, A183, NAT_1:13;
then consider i1, j1, i2, j2 being Nat such that
A416: [i1,j1] in Indices (Gauge (C,n)) and
A417: (F . k) /. m = (Gauge (C,n)) * (i1,j1) and
A418: [i2,j2] in Indices (Gauge (C,n)) and
A419: (F . k) /. (m + 1) = (Gauge (C,n)) * (i2,j2) and
A420: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A180, A369, JORDAN8:3;
A421: right_cell ((F . k),m,(Gauge (C,n))) misses C by A181, A369, A415;

A422: now :: thesis:

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 Nat such that
(F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_left (len (F . k)) -' 1, Gauge (C,n) and
A423: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A156, A180, A182, A218, A237;
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))) misses C & front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ) ; :: thesis:

then consider i, j being Nat such that
(F . k) ^ <*((Gauge (C,n)) * (i,j))*> goes_straight (len (F . k)) -' 1, Gauge (C,n) and
A424: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A156, A180, A182, A218, A237;
take i = i; :: thesis:
take j = j; :: thesis:
thus F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A424; :: thesis:

end;

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

then consider i, j being Nat such that
(F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_right (len (F . k)) -' 1, Gauge (C,n) and
A425: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A156, A180, A182, A218, A237;
take i = i; :: thesis:
take j = j; :: thesis:
thus F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A425; :: thesis:

end;

1 <= m + 1 by NAT_1:12;
then m + 1 in dom (F . k) by A415, FINSEQ_3:25;
then A426: (F . (k + 1)) /. (m + 1) = (Gauge (C,n)) * (i2,j2) by A419, A422, FINSEQ_4:68;
A427: left_cell ((F . k),m,(Gauge (C,n))) meets C by A181, A369, A415;
m <= len (F . k) by A415, NAT_1:13;
then m in dom (F . k) by A369, FINSEQ_3:25;
then A428: (F . (k + 1)) /. m = (Gauge (C,n)) * (i1,j1) by A417, A422, FINSEQ_4:68;

now :: thesis:

per cases by A420;

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

then A430: right_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) by A180, A369, A415, A416, A417, A418, A419, GOBRD13:22;
left_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j1) by A180, A369, A415, A416, A417, A418, A419, A429, GOBRD13:21;
hence ( right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) by A243, A369, A370, A416, A418, A421, A427, A428, A426, A429, A430, GOBRD13:21, GOBRD13:22; :: thesis:

end;

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

then A432: right_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,(j1 -' 1)) by A180, A369, A415, A416, A417, A418, A419, GOBRD13:24;
left_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) by A180, A369, A415, A416, A417, A418, A419, A431, GOBRD13:23;
hence ( right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) by A243, A369, A370, A416, A418, A421, A427, A428, A426, A431, A432, GOBRD13:23, GOBRD13:24; :: thesis:

end;

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

then A434: right_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) by A180, A369, A415, A416, A417, A418, A419, GOBRD13:26;
left_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A180, A369, A415, A416, A417, A418, A419, A433, GOBRD13:25;
hence ( right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) by A243, A369, A370, A416, A418, A421, A427, A428, A426, A433, A434, GOBRD13:25, GOBRD13:26; :: thesis:

end;

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

then A436: right_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j2) by A180, A369, A415, A416, A417, A418, A419, GOBRD13:28;
left_cell ((F . k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) by A180, A369, A415, A416, A417, A418, A419, A435, GOBRD13:27;
hence ( right_cell ((F . (k + 1)),m,(Gauge (C,n))) misses C & left_cell ((F . (k + 1)),m,(Gauge (C,n))) meets C ) by A243, A369, A370, A416, A418, A421, A427, A428, A426, A435, A436, GOBRD13:27, 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;

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;

A437: S₄[ 0 ]

proof

A438: for n being Nat st n in dom (F . 0) & n + 1 in dom (F . 0) holds
for m, k, i, j being Nat st [m,k] in Indices (Gauge (C,n)) & [i,j] in Indices (Gauge (C,n)) & (F . 0) /. n = (Gauge (C,n)) * (m,k) & (F . 0) /. (n + 1) = (Gauge (C,n)) * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 by A155;
for n being Nat st n in dom (F . 0) holds
ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & (F . 0) /. n = (Gauge (C,n)) * (i,j) ) by A155;
hence F . 0 is_sequence_on Gauge (C,n) by A438, GOBOARD1:def 9; :: thesis:
let m be Nat; :: thesis:
assume that
1 <= m and
A439: 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, A439, CARD_1:27; :: thesis:

end;

A440: for k being Nat holds S₄[k] from NAT_1:sch 2(A437, A179);
A441: for k, i1, i2, j1, j2 being Nat st k > 1 & [i1,j1] in Indices (Gauge (C,n)) & (F . k) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) & [i2,j2] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) & 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 Nat; :: thesis:
assume that
A442: k > 1 and
A443: [i1,j1] in Indices (Gauge (C,n)) and
A444: (F . k) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) and
A445: [i2,j2] in Indices (Gauge (C,n)) and
A446: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) ; :: thesis:
A447: len (F . k) = k by A177;
then A448: 1 <= (len (F . k)) -' 1 by A442, NAT_D:49;
(len (F . k)) -' 1 <= len (F . k) by NAT_D:35;
then A449: (len (F . k)) -' 1 in dom (F . k) by A448, FINSEQ_3:25;
A450: i1 + 1 > i1 by NAT_1:13;
A451: F . k is_sequence_on Gauge (C,n) by A440;
A452: j1 + 1 > j1 by NAT_1:13;
A453: len (F . k) in dom (F . k) by A442, A447, FINSEQ_3:25;
A454: i2 + 1 > i2 by NAT_1:13;
A455: j2 + 1 > j2 by NAT_1:13;
A456: ((len (F . k)) -' 1) + 1 = len (F . k) by A442, A447, XREAL_1:235;
then A457: ((len (F . k)) -' 1) + (1 + 1) = (len (F . k)) + 1 ;
A458: left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C by A440, A448, A456;

hereby :: thesis:

assume that
A459: front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C and
A460: front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C ; :: thesis:
consider i, j being Nat such that
A461: (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_left (len (F . k)) -' 1, Gauge (C,n) and
A462: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A156, A442, A451, A447, A458, A459, A460;
thus F . (k + 1) turns_left (len (F . k)) -' 1, Gauge (C,n) by A461, A462; :: thesis:
A463: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i,j) by A462, FINSEQ_4:67;
A464: (F . (k + 1)) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) by A446, A453, A462, FINSEQ_4:68;
A465: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) by A444, A449, A462, FINSEQ_4:68;
hence ( i1 = i2 & j1 + 1 = j2 implies ( [(i2 -' 1),j2] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> ) ) by A443, A445, A456, A457, A452, A455, A461, A462, A464, A463, 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 A443, A445, A456, A457, A450, A454, A461, A462, A465, A464, A463, 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 A443, A445, A456, A457, A450, A454, A461, A462, A465, A464, A463, 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 A443, A445, A456, A457, A452, A455, A461, A462, A465, A464, A463, GOBRD13:def 7; :: thesis:

end;

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

proof

let m be 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 Nat st
( w = $1 & $1 >= 1 & ex m being Nat st
( m in dom (F . w) & m <> len (F . w) & (F . w) /. m = (F . w) /. (len (F . w)) ) );
A467: S₁[ 0 ,F . 0,F . (0 + 1)] by A156;
A468: for k, i1, i2, j1, j2 being Nat st k > 1 & [i1,j1] in Indices (Gauge (C,n)) & (F . k) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) & [i2,j2] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) & 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 Nat; :: thesis:
assume that
A469: k > 1 and
A470: [i1,j1] in Indices (Gauge (C,n)) and
A471: (F . k) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) and
A472: [i2,j2] in Indices (Gauge (C,n)) and
A473: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) ; :: thesis:
A474: len (F . k) = k by A177;
then A475: 1 <= (len (F . k)) -' 1 by A469, NAT_D:49;
(len (F . k)) -' 1 <= len (F . k) by NAT_D:35;
then A476: (len (F . k)) -' 1 in dom (F . k) by A475, FINSEQ_3:25;
A477: i1 + 1 > i1 by NAT_1:13;
A478: F . k is_sequence_on Gauge (C,n) by A440;
A479: j1 + 1 > j1 by NAT_1:13;
A480: len (F . k) in dom (F . k) by A469, A474, FINSEQ_3:25;
A481: i2 + 1 > i2 by NAT_1:13;
A482: j2 + 1 > j2 by NAT_1:13;
A483: ((len (F . k)) -' 1) + 1 = len (F . k) by A469, A474, XREAL_1:235;
then A484: ((len (F . k)) -' 1) + (1 + 1) = (len (F . k)) + 1 ;
A485: left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C by A440, A475, A483;

hereby :: thesis:

assume that
A486: front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) misses C and
A487: front_left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ; :: thesis:
consider i, j being Nat such that
A488: (F . k) ^ <*((Gauge (C,n)) * (i,j))*> goes_straight (len (F . k)) -' 1, Gauge (C,n) and
A489: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A156, A469, A478, A474, A485, A486, A487;
thus F . (k + 1) goes_straight (len (F . k)) -' 1, Gauge (C,n) by A488, A489; :: thesis:
A490: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i,j) by A489, FINSEQ_4:67;
A491: (F . (k + 1)) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) by A473, A480, A489, FINSEQ_4:68;
A492: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) by A471, A476, A489, FINSEQ_4:68;
hence ( i1 = i2 & j1 + 1 = j2 implies ( [i2,(j2 + 1)] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> ) ) by A470, A472, A483, A484, A479, A482, A488, A489, A491, A490, 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 A470, A472, A483, A484, A477, A481, A488, A489, A492, A491, A490, 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 A470, A472, A483, A484, A477, A481, A488, A489, A492, A491, A490, 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 A470, A472, A483, A484, A479, A482, A488, A489, A492, A491, A490, GOBRD13:def 8; :: thesis:

end;

A493: for k, i1, i2, j1, j2 being Nat st k > 1 & [i1,j1] in Indices (Gauge (C,n)) & (F . k) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) & [i2,j2] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) & 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 Nat; :: thesis:
assume that
A494: k > 1 and
A495: [i1,j1] in Indices (Gauge (C,n)) and
A496: (F . k) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) and
A497: [i2,j2] in Indices (Gauge (C,n)) and
A498: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) ; :: thesis:
A499: len (F . k) = k by A177;
then A500: ((len (F . k)) -' 1) + 1 = len (F . k) by A494, XREAL_1:235;
then A501: ((len (F . k)) -' 1) + (1 + 1) = (len (F . k)) + 1 ;
A502: F . k is_sequence_on Gauge (C,n) by A440;
assume A503: front_right_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C ; :: thesis:
A504: 1 <= (len (F . k)) -' 1 by A494, A499, NAT_D:49;
then left_cell ((F . k),((len (F . k)) -' 1),(Gauge (C,n))) meets C by A440, A500;
then consider i, j being Nat such that
A505: (F . k) ^ <*((Gauge (C,n)) * (i,j))*> turns_right (len (F . k)) -' 1, Gauge (C,n) and
A506: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> by A156, A494, A502, A499, A503;
len (F . k) in dom (F . k) by A494, A499, FINSEQ_3:25;
then A507: (F . (k + 1)) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) by A498, A506, FINSEQ_4:68;
(len (F . k)) -' 1 <= len (F . k) by NAT_D:35;
then (len (F . k)) -' 1 in dom (F . k) by A504, FINSEQ_3:25;
then A508: (F . (k + 1)) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) by A496, A506, FINSEQ_4:68;
thus F . (k + 1) turns_right (len (F . k)) -' 1, Gauge (C,n) by A505, A506; :: thesis:
A509: (F . (k + 1)) /. ((len (F . k)) + 1) = (Gauge (C,n)) * (i,j) by A506, FINSEQ_4:67;
A510: j2 + 1 > j2 by NAT_1:13;
A511: i2 + 1 > i2 by NAT_1:13;
A512: 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 A495, A497, A500, A501, A510, A505, A506, A508, A507, A509, GOBRD13:def 6; :: thesis:
A513: 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 A495, A497, A500, A501, A511, A505, A506, A508, A507, A509, 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 A495, A497, A500, A501, A513, A511, A505, A506, A508, A507, A509, 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 A495, A497, A500, A501, A512, A510, A505, A506, A508, A507, A509, GOBRD13:def 6; :: thesis:

end;

A514: for k being 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 Nat; :: thesis:
assume A515: k > 1 ; :: thesis:
A516: F . k is_sequence_on Gauge (C,n) by A440;
A517: len (F . k) = k by A177;
then A518: ((len (F . k)) -' 1) + 1 = len (F . k) by A515, XREAL_1:235;
1 <= (len (F . k)) -' 1 by A515, A517, NAT_D:49;
then ex i1, j1, i2, j2 being Nat st
( [i1,j1] in Indices (Gauge (C,n)) & (F . k) /. ((len (F . k)) -' 1) = (Gauge (C,n)) * (i1,j1) & [i2,j2] in Indices (Gauge (C,n)) & (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) ) by A516, A518, JORDAN8:3;
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 A441, A468, A493, A515, A517; :: thesis:

end;

A519: S₁[1,F . 1,F . (1 + 1)] by A156;
A520: for k being Nat ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> )

proof

let k be Nat; :: thesis:
A521: F . k is_sequence_on Gauge (C,n) by A440;
A522: len (F . k) = k by A177;

per cases by XXREAL_0:1;

suppose A523: 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 A523, NAT_1:14;
hence F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))))*> by A155, A467, FINSEQ_1:34; :: thesis:

end;

suppose A524: 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 A467, A519, A524, FINSEQ_1:def 9; :: thesis:

end;

suppose A525: k > 1 ; :: thesis:

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

now :: thesis:

per cases ;

suppose A532: ( 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 :: thesis:

per cases by A531;

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

then A534: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> by A441, A525, A527, A528, A529, A530, A532;
[(i2 -' 1),j2] in Indices (Gauge (C,n)) by A441, A525, A527, A528, A529, A530, A532, A533;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A534; :: thesis:

end;

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

then A536: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> by A441, A525, A527, A528, A529, A530, A532;
[i2,(j2 + 1)] in Indices (Gauge (C,n)) by A441, A525, A527, A528, A529, A530, A532, A535;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A536; :: thesis:

end;

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

then A538: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> by A441, A525, A527, A528, A529, A530, A532;
[i2,(j2 -' 1)] in Indices (Gauge (C,n)) by A441, A525, A527, A528, A529, A530, A532, A537;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A538; :: thesis:

end;

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

then A540: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> by A441, A525, A527, A528, A529, A530, A532;
[(i2 + 1),j2] in Indices (Gauge (C,n)) by A441, A525, A527, A528, A529, A530, A532, A539;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A540; :: thesis:

end;

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

end;

suppose A541: ( 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 :: thesis:

per cases by A531;

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

then A543: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> by A468, A525, A527, A528, A529, A530, A541;
[i2,(j2 + 1)] in Indices (Gauge (C,n)) by A468, A525, A527, A528, A529, A530, A541, A542;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A543; :: thesis:

end;

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

then A545: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> by A468, A525, A527, A528, A529, A530, A541;
[(i2 + 1),j2] in Indices (Gauge (C,n)) by A468, A525, A527, A528, A529, A530, A541, A544;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A545; :: thesis:

end;

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

then A547: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> by A468, A525, A527, A528, A529, A530, A541;
[(i2 -' 1),j2] in Indices (Gauge (C,n)) by A468, A525, A527, A528, A529, A530, A541, A546;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A547; :: thesis:

end;

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

then A549: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> by A468, A525, A527, A528, A529, A530, A541;
[i2,(j2 -' 1)] in Indices (Gauge (C,n)) by A468, A525, A527, A528, A529, A530, A541, A548;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A549; :: thesis:

end;

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

end;

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

now :: thesis:

per cases by A531;

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

then A552: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> by A493, A525, A527, A528, A529, A530, A550;
[(i2 + 1),j2] in Indices (Gauge (C,n)) by A493, A525, A527, A528, A529, A530, A550, A551;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A552; :: thesis:

end;

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

then A554: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> by A493, A525, A527, A528, A529, A530, A550;
[i2,(j2 -' 1)] in Indices (Gauge (C,n)) by A493, A525, A527, A528, A529, A530, A550, A553;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A554; :: thesis:

end;

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

then A556: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> by A493, A525, A527, A528, A529, A530, A550;
[i2,(j2 + 1)] in Indices (Gauge (C,n)) by A493, A525, A527, A528, A529, A530, A550, A555;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A556; :: thesis:

end;

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

then A558: F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> by A493, A525, A527, A528, A529, A530, A550;
[(i2 -' 1),j2] in Indices (Gauge (C,n)) by A493, A525, A527, A528, A529, A530, A550, A557;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A558; :: thesis:

end;

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

end;

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

end;

A559: for k being Nat st S₅[k] holds
S₅[k + 1]

proof

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

per cases by A561, XXREAL_0:1;

suppose m < k + 1 ; :: thesis:

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

end;

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

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

end;

A565: for k being Nat holds S₅[k] from NAT_1:sch 2(A466, A559);
A566: for j, k being Nat st 1 <= j & j <= k holds
(F . k) /. j = (F . j) /. j

proof

let j, k be Nat; :: thesis:
assume that
A567: 1 <= j and
A568: j <= k ; :: thesis:
j <= len (F . k) by A177, A568;
then len ((F . k) | j) = j by FINSEQ_1:59;
then A569: j in dom ((F . k) | j) by A567, FINSEQ_3:25;
(F . k) | j = F . j by A565, A568;
hence (F . k) /. j = (F . j) /. j by A569, FINSEQ_4:70; :: thesis:

end;

defpred S₇[ Nat] means F . $1 is unfolded ;
A570: for k being Nat st S₇[k] holds
S₇[k + 1]

proof

let k be Nat; :: thesis:
assume A571: F . k is unfolded ; :: thesis:
A572: F . k is_sequence_on Gauge (C,n) by A440;

per cases ;

suppose k <= 1 ; :: thesis:

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

end;

suppose A573: k > 1 ; :: thesis:

set m = k -' 1;
A574: (k -' 1) + 1 = k by A573, XREAL_1:235;
A575: len (F . k) = k by A177;
A576: 1 <= k -' 1 by A573, NAT_D:49;
then consider i1, j1, i2, j2 being Nat such that
A577: [i1,j1] in Indices (Gauge (C,n)) and
A578: (F . k) /. (k -' 1) = (Gauge (C,n)) * (i1,j1) and
A579: [i2,j2] in Indices (Gauge (C,n)) and
A580: (F . k) /. (len (F . k)) = (Gauge (C,n)) * (i2,j2) and
A581: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A572, A574, A575, JORDAN8:3;
A582: LSeg ((F . k),(k -' 1)) = LSeg (((Gauge (C,n)) * (i1,j1)),((Gauge (C,n)) * (i2,j2))) by A576, A574, A575, A578, A580, TOPREAL1:def 3;
A583: 1 <= j2 by A579, MATRIX_0:32;
then A584: (j2 -' 1) + 1 = j2 by XREAL_1:235;
A585: 1 <= j1 by A577, MATRIX_0:32;
A586: 1 <= i2 by A579, MATRIX_0:32;
then A587: (i2 -' 1) + 1 = i2 by XREAL_1:235;
A588: i1 <= len (Gauge (C,n)) by A577, MATRIX_0:32;
A589: j2 <= width (Gauge (C,n)) by A579, MATRIX_0:32;
A590: 1 <= i1 by A577, MATRIX_0:32;
A591: j1 <= width (Gauge (C,n)) by A577, MATRIX_0:32;
A592: i2 <= len (Gauge (C,n)) by A579, MATRIX_0:32;

now :: thesis:

per cases ;

suppose A593: ( 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 :: thesis:

per cases by A581;

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

then [(i2 -' 1),j2] in Indices (Gauge (C,n)) by A441, A573, A575, A577, A578, A579, A580, A593;
then 1 <= i2 -' 1 by MATRIX_0:32;
then A595: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * ((i2 -' 1),j2)))) = {((F . k) /. (len (F . k)))} by A580, A588, A585, A589, A587, A582, A594, GOBOARD7:16;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> by A441, A573, A575, A577, A578, A579, A580, A593, A594;
hence S₇[k + 1] by A571, A574, A575, A595, SPPOL_2:30; :: thesis:

end;

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

then [i2,(j2 + 1)] in Indices (Gauge (C,n)) by A441, A573, A575, A577, A578, A579, A580, A593;
then j2 + 1 <= width (Gauge (C,n)) by MATRIX_0:32;
then A597: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * (i2,(j2 + 1))))) = {((F . k) /. (len (F . k)))} by A580, A590, A585, A592, A582, A596, GOBOARD7:18;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> by A441, A573, A575, A577, A578, A579, A580, A593, A596;
hence S₇[k + 1] by A571, A574, A575, A597, SPPOL_2:30; :: thesis:

end;

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

then [i2,(j2 -' 1)] in Indices (Gauge (C,n)) by A441, A573, A575, A577, A578, A579, A580, A593;
then 1 <= j2 -' 1 by MATRIX_0:32;
then A599: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * (i2,(j2 -' 1))))) = {((F . k) /. (len (F . k)))} by A580, A588, A591, A586, A584, A582, A598, GOBOARD7:15;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> by A441, A573, A575, A577, A578, A579, A580, A593, A598;
hence S₇[k + 1] by A571, A574, A575, A599, SPPOL_2:30; :: thesis:

end;

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

then [(i2 + 1),j2] in Indices (Gauge (C,n)) by A441, A573, A575, A577, A578, A579, A580, A593;
then i2 + 1 <= len (Gauge (C,n)) by MATRIX_0:32;
then A601: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * ((i2 + 1),j2)))) = {((F . k) /. (len (F . k)))} by A580, A590, A591, A583, A582, A600, GOBOARD7:17;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> by A441, A573, A575, A577, A578, A579, A580, A593, A600;
hence S₇[k + 1] by A571, A574, A575, A601, SPPOL_2:30; :: thesis:

end;

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

end;

suppose A602: ( 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 :: thesis:

per cases by A581;

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

then [i2,(j2 + 1)] in Indices (Gauge (C,n)) by A468, A573, A575, A577, A578, A579, A580, A602;
then A604: j2 + 1 <= width (Gauge (C,n)) by MATRIX_0:32;
j2 + 1 = j1 + (1 + 1) by A603;
then A605: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * (i2,(j2 + 1))))) = {((F . k) /. (len (F . k)))} by A580, A590, A588, A585, A582, A603, A604, GOBOARD7:13;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> by A468, A573, A575, A577, A578, A579, A580, A602, A603;
hence S₇[k + 1] by A571, A574, A575, A605, SPPOL_2:30; :: thesis:

end;

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

then [(i2 + 1),j2] in Indices (Gauge (C,n)) by A468, A573, A575, A577, A578, A579, A580, A602;
then A607: i2 + 1 <= len (Gauge (C,n)) by MATRIX_0:32;
i2 + 1 = i1 + (1 + 1) by A606;
then A608: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * ((i2 + 1),j2)))) = {((F . k) /. (len (F . k)))} by A580, A590, A585, A591, A582, A606, A607, GOBOARD7:14;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> by A468, A573, A575, A577, A578, A579, A580, A602, A606;
hence S₇[k + 1] by A571, A574, A575, A608, SPPOL_2:30; :: thesis:

end;

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

then [(i2 -' 1),j2] in Indices (Gauge (C,n)) by A468, A573, A575, A577, A578, A579, A580, A602;
then A610: 1 <= i2 -' 1 by MATRIX_0:32;
((i2 -' 1) + 1) + 1 = (i2 -' 1) + (1 + 1) ;
then A611: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * ((i2 -' 1),j2)))) = {((F . k) /. (len (F . k)))} by A580, A588, A585, A591, A587, A582, A609, A610, GOBOARD7:14;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> by A468, A573, A575, A577, A578, A579, A580, A602, A609;
hence S₇[k + 1] by A571, A574, A575, A611, SPPOL_2:30; :: thesis:

end;

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

then [i2,(j2 -' 1)] in Indices (Gauge (C,n)) by A468, A573, A575, A577, A578, A579, A580, A602;
then A613: 1 <= j2 -' 1 by MATRIX_0:32;
((j2 -' 1) + 1) + 1 = (j2 -' 1) + (1 + 1) ;
then A614: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * (i2,(j2 -' 1))))) = {((F . k) /. (len (F . k)))} by A580, A590, A588, A591, A584, A582, A612, A613, GOBOARD7:13;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> by A468, A573, A575, A577, A578, A579, A580, A602, A612;
hence S₇[k + 1] by A571, A574, A575, A614, SPPOL_2:30; :: thesis:

end;

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

end;

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

now :: thesis:

per cases by A581;

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

then [(i2 + 1),j2] in Indices (Gauge (C,n)) by A493, A573, A575, A577, A578, A579, A580, A615;
then i2 + 1 <= len (Gauge (C,n)) by MATRIX_0:32;
then A617: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * ((i2 + 1),j2)))) = {((F . k) /. (len (F . k)))} by A580, A590, A585, A589, A582, A616, GOBOARD7:15;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 + 1),j2))*> by A493, A573, A575, A577, A578, A579, A580, A615, A616;
hence S₇[k + 1] by A571, A574, A575, A617, SPPOL_2:30; :: thesis:

end;

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

then [i2,(j2 -' 1)] in Indices (Gauge (C,n)) by A493, A573, A575, A577, A578, A579, A580, A615;
then 1 <= j2 -' 1 by MATRIX_0:32;
then A619: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * (i2,(j2 -' 1))))) = {((F . k) /. (len (F . k)))} by A580, A590, A591, A592, A584, A582, A618, GOBOARD7:16;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 -' 1)))*> by A493, A573, A575, A577, A578, A579, A580, A615, A618;
hence S₇[k + 1] by A571, A574, A575, A619, SPPOL_2:30; :: thesis:

end;

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

then [i2,(j2 + 1)] in Indices (Gauge (C,n)) by A493, A573, A575, A577, A578, A579, A580, A615;
then j2 + 1 <= width (Gauge (C,n)) by MATRIX_0:32;
then A621: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * (i2,(j2 + 1))))) = {((F . k) /. (len (F . k)))} by A580, A588, A585, A586, A582, A620, GOBOARD7:17;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i2,(j2 + 1)))*> by A493, A573, A575, A577, A578, A579, A580, A615, A620;
hence S₇[k + 1] by A571, A574, A575, A621, SPPOL_2:30; :: thesis:

end;

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

then [(i2 -' 1),j2] in Indices (Gauge (C,n)) by A493, A573, A575, A577, A578, A579, A580, A615;
then 1 <= i2 -' 1 by MATRIX_0:32;
then A623: (LSeg ((F . k),(k -' 1))) /\ (LSeg (((F . k) /. (len (F . k))),((Gauge (C,n)) * ((i2 -' 1),j2)))) = {((F . k) /. (len (F . k)))} by A580, A588, A591, A583, A587, A582, A622, GOBOARD7:18;
F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * ((i2 -' 1),j2))*> by A493, A573, A575, A577, A578, A579, A580, A615, A622;
hence S₇[k + 1] by A571, A574, A575, A623, SPPOL_2:30; :: thesis:

end;

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

end;

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

end;

now :: thesis:

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

proof

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

now :: thesis:

let n, m be Element of NAT ; :: thesis:
assume that
A627: n in dom (F . (k + 1)) and
A628: m in dom (F . (k + 1)) and
A629: (F . (k + 1)) /. n = (F . (k + 1)) /. m ; :: thesis:
A630: 1 <= n by A627, FINSEQ_3:25;
A631: m <= len (F . (k + 1)) by A628, FINSEQ_3:25;
A632: 1 <= m by A628, FINSEQ_3:25;
A633: n <= len (F . (k + 1)) by A627, FINSEQ_3:25;
A634: ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & F . (k + 1) = (F . k) ^ <*((Gauge (C,n)) * (i,j))*> ) by A520;
A635: len (F . k) = k by A177;
A636: len (F . (k + 1)) = k + 1 by A177;

per cases by A633, A631, A636, NAT_1:8;

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

then A638: m in dom (F . k) by A632, A635, FINSEQ_3:25;
then A639: (F . (k + 1)) /. m = (F . k) /. m by A634, FINSEQ_4:68;
A640: n in dom (F . k) by A630, A635, A637, FINSEQ_3:25;
then (F . (k + 1)) /. n = (F . k) /. n by A634, FINSEQ_4:68;
hence n = m by A626, A629, A640, A638, A639, PARTFUN2:10; :: thesis:

end;

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

hence n = m by A624, A628, A629, A636, NAT_1:12; :: thesis:

end;

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

hence n = m by A624, A627, A629, A636, NAT_1:12; :: thesis:

end;

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

hence n = m ; :: thesis:

end;

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

end;

A641: S₈[ 0 ] by A155;
A642: for k being Nat holds S₈[k] from NAT_1:sch 2(A641, A625);
A643: for k being Nat holds card (rng (F . k)) = k

proof

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

end;

reconsider k = ((len (Gauge (C,n))) * (width (Gauge (C,n)))) + 1 as Nat ;
A644: k > (len (Gauge (C,n))) * (width (Gauge (C,n))) by NAT_1:13;
F . k is_sequence_on Gauge (C,n) by A440;
then A645: card (rng (F . k)) <= card (Values (Gauge (C,n))) by GOBRD13:8, NAT_1:43;
card (Values (Gauge (C,n))) <= (len (Gauge (C,n))) * (width (Gauge (C,n))) by MATRIX_0:40;
then card (rng (F . k)) <= (len (Gauge (C,n))) * (width (Gauge (C,n))) by A645, XXREAL_0:2;
hence contradiction by A643, A644; :: thesis:

end;

then A646: ex k being Nat st S₆[k] ;
consider k being Nat such that
A647: S₆[k] and
A648: for l being Nat st S₆[l] holds
k <= l from NAT_1:sch 5(A646);
reconsider k = k as Nat ;
consider m being Nat such that
A649: m in dom (F . k) and
A650: m <> len (F . k) and
A651: (F . k) /. m = (F . k) /. (len (F . k)) by A647;
A652: 1 <= m by A649, FINSEQ_3:25;
reconsider f = F . k as non empty FinSequence of (TOP-REAL 2) by A647;
A653: f is_sequence_on Gauge (C,n) by A440;
A654: m <= len f by A649, FINSEQ_3:25;
then A655: m < len f by A650, XXREAL_0:1;
then 1 < len f by A652, XXREAL_0:2;
then A656: len f >= 1 + 1 by NAT_1:13;
then A657: k >= 2 by A177;
A658: S₇[ 0 ] by A155, CARD_1:27, SPPOL_2:26;
for k being Nat holds S₇[k] from NAT_1:sch 2(A658, A570);
then reconsider f = f as non empty non constant special unfolded FinSequence of (TOP-REAL 2) by A653, A656, JORDAN8:4, JORDAN8:5;
set g = f /^ (m -' 1);
A659: m + 1 <= len f by A655, NAT_1:13;
A660: for h being non constant standard special_circular_sequence st L~ h c= L~ f holds
for Comp being Subset of (TOP-REAL 2) st Comp is_a_component_of (L~ h) ` holds
for n being Nat st 1 <= n & n + 1 <= len f & f /. n in Comp & not f /. n in L~ h holds
C meets Comp

proof

proof

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

now :: thesis:

take p = p; :: thesis:

now :: thesis:

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

end;

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

end;

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

end;

Int (left_cell (f,n,(Gauge (C,n)))) is convex by A653, A663, A664, JORDAN9:10;
then rc is connected by A669, A671, A667, A672, CONNSP_1:18, XBOOLE_1:19;
then rc c= Comp by A662, A668, A670, GOBOARD9:4;
hence C meets Comp by A673, XBOOLE_1:63; :: thesis:

end;

A680: for i being 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 Nat; :: thesis:
assume that
A681: 1 <= i and
A682: i + 1 <= len f ; :: thesis:
consider i1, j1, i2, j2 being Nat such that
A683: [i1,j1] in Indices (Gauge (C,n)) and
A684: f /. i = (Gauge (C,n)) * (i1,j1) and
A685: [i2,j2] in Indices (Gauge (C,n)) and
A686: f /. (i + 1) = (Gauge (C,n)) * (i2,j2) and
A687: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A653, A681, A682, JORDAN8:3;
A688: i1 <= len (Gauge (C,n)) by A683, MATRIX_0:32;
A689: i2 <= len (Gauge (C,n)) by A685, MATRIX_0:32;
A690: i1 + 1 > i1 by NAT_1:13;
A691: j1 <= width (Gauge (C,n)) by A683, MATRIX_0:32;
A692: j1 + 1 > j1 by NAT_1:13;
A693: j2 <= width (Gauge (C,n)) by A685, MATRIX_0:32;
A694: i2 + 1 > i2 by NAT_1:13;
A695: j2 + 1 > j2 by NAT_1:13;

per cases by A687;

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

A697: i1 -' 1 <= len (Gauge (C,n)) by A688, NAT_D:44;
left_cell (f,i,(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j1) by A653, A681, A682, A683, A684, A685, A686, A692, A695, A696, GOBRD13:def 3;
hence left_cell (f,i,(Gauge (C,n))) = Cl (Int (left_cell (f,i,(Gauge (C,n))))) by A691, A697, 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 A653, A681, A682, A683, A684, A685, A686, A690, A694, GOBRD13:def 3;
hence left_cell (f,i,(Gauge (C,n))) = Cl (Int (left_cell (f,i,(Gauge (C,n))))) by A688, A691, GOBRD11:35; :: thesis:

end;

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

A699: j2 -' 1 <= width (Gauge (C,n)) by A693, NAT_D:44;
left_cell (f,i,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A653, A681, A682, A683, A684, A685, A686, A690, A694, A698, GOBRD13:def 3;
hence left_cell (f,i,(Gauge (C,n))) = Cl (Int (left_cell (f,i,(Gauge (C,n))))) by A689, A699, 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 A653, A681, A682, A683, A684, A685, A686, A692, A695, GOBRD13:def 3;
hence left_cell (f,i,(Gauge (C,n))) = Cl (Int (left_cell (f,i,(Gauge (C,n))))) by A688, A693, GOBRD11:35; :: thesis:

end;

m -' 1 <= m by NAT_D:44;
then m -' 1 < m + 1 by NAT_1:13;
then A700: m -' 1 < len f by A659, XXREAL_0:2;
then A701: len (f /^ (m -' 1)) = (len f) - (m -' 1) by RFINSEQ:def 1;
then (m -' 1) - (m -' 1) < len (f /^ (m -' 1)) by A700, XREAL_1:9;
then reconsider g = f /^ (m -' 1) as non empty FinSequence of (TOP-REAL 2) by CARD_1:27;
len g in dom g by FINSEQ_5:6;
then A702: g /. (len g) = f /. ((m -' 1) + (len g)) by FINSEQ_5:27
.= f /. (len f) by A701 ;
(m + 1) - (m -' 1) <= len g by A659, A701, XREAL_1:9;
then A703: (m + 1) - (m - 1) <= len g by A652, XREAL_1:233;
then A704: ((1 + m) - m) + 1 <= len g ;
A705: g is_sequence_on Gauge (C,n) by A440, JORDAN8:2;
then A706: g is standard by JORDAN8:4;
A707: not g is constant

proof

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

end;

A710: len (F . k) = k by A177;
A711: for j, i being Nat st 1 <= i & i < len g & 1 <= j & j < len g & g /. i = g /. j holds
i = j

proof

let j, i be Nat; :: thesis:
assume that
A712: 1 <= i and
A713: i < len g and
A714: 1 <= j and
A715: j < len g and
A716: g /. i = g /. j and
A717: i <> j ; :: thesis:
A718: i in dom g by A712, A713, FINSEQ_3:25;
then A719: g /. i = f /. ((m -' 1) + i) by FINSEQ_5:27;
A720: j in dom g by A714, A715, FINSEQ_3:25;
then A721: g /. j = f /. ((m -' 1) + j) by FINSEQ_5:27;

per cases by A717, XXREAL_0:1;

suppose A722: i < j ; :: thesis:

set l = (m -' 1) + j;
set m9 = (m -' 1) + i;
A723: (m -' 1) + i < (m -' 1) + j by A722, XREAL_1:6;
A724: len (F . ((m -' 1) + j)) = (m -' 1) + j by A177;
A725: (m -' 1) + j < k by A710, A701, A715, XREAL_1:20;
then A726: f | ((m -' 1) + j) = F . ((m -' 1) + j) by A565;
0 + j <= (m -' 1) + j by XREAL_1:6;
then A727: 1 <= (m -' 1) + j by A714, XXREAL_0:2;
then (m -' 1) + j in dom (F . ((m -' 1) + j)) by A724, FINSEQ_3:25;
then A728: (F . ((m -' 1) + j)) /. ((m -' 1) + j) = f /. ((m -' 1) + j) by A726, FINSEQ_4:70;
0 + i <= (m -' 1) + i by XREAL_1:6;
then 1 <= (m -' 1) + i by A712, XXREAL_0:2;
then A729: (m -' 1) + i in dom (F . ((m -' 1) + j)) by A723, A724, FINSEQ_3:25;
then (F . ((m -' 1) + j)) /. ((m -' 1) + i) = f /. ((m -' 1) + i) by A726, FINSEQ_4:70;
hence contradiction by A648, A716, A719, A720, A723, A725, A727, A724, A729, A728, FINSEQ_5:27; :: thesis:

end;

suppose A730: j < i ; :: thesis:

set l = (m -' 1) + i;
set m9 = (m -' 1) + j;
A731: (m -' 1) + j < (m -' 1) + i by A730, XREAL_1:6;
A732: len (F . ((m -' 1) + i)) = (m -' 1) + i by A177;
A733: (m -' 1) + i < k by A710, A701, A713, XREAL_1:20;
then A734: f | ((m -' 1) + i) = F . ((m -' 1) + i) by A565;
0 + i <= (m -' 1) + i by XREAL_1:6;
then A735: 1 <= (m -' 1) + i by A712, XXREAL_0:2;
then (m -' 1) + i in dom (F . ((m -' 1) + i)) by A732, FINSEQ_3:25;
then A736: (F . ((m -' 1) + i)) /. ((m -' 1) + i) = f /. ((m -' 1) + i) by A734, FINSEQ_4:70;
0 + j <= (m -' 1) + j by XREAL_1:6;
then 1 <= (m -' 1) + j by A714, XXREAL_0:2;
then A737: (m -' 1) + j in dom (F . ((m -' 1) + i)) by A731, A732, FINSEQ_3:25;
then (F . ((m -' 1) + i)) /. ((m -' 1) + j) = f /. ((m -' 1) + j) by A734, FINSEQ_4:70;
hence contradiction by A648, A716, A718, A721, A731, A733, A735, A732, A737, A736, FINSEQ_5:27; :: thesis:

end;

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

proof

let j, i be Nat; :: thesis:
assume that
A740: 1 < i and
A741: i < j and
A742: j <= len g and
A743: g /. i = g /. j ; :: thesis:
A744: 1 < j by A740, A741, XXREAL_0:2;
A745: i < len g by A741, A742, XXREAL_0:2;
then A746: 1 < len g by A740, XXREAL_0:2;

per cases ;

suppose j <> len g ; :: thesis:

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

end;

suppose j = len g ; :: thesis:

hence contradiction by A651, A738, A702, A711, A740, A741, A743, A746; :: thesis:

end;

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

proof

let j, i be Nat; :: thesis:
assume that
A748: 1 <= i and
A749: i < j and
A750: j < len g and
A751: g /. i = g /. j ; :: thesis:
A752: i < len g by A749, A750, XXREAL_0:2;
1 < j by A748, A749, XXREAL_0:2;
hence contradiction by A711, A748, A749, A750, A751, A752; :: thesis:

end;

g is s.c.c.

proof

let i be Nat; :: according to GOBOARD5:def 4 :: thesis:
let j be Nat; :: thesis:
assume that
A753: i + 1 < j and
A754: ( ( i > 1 & j < len g ) or j + 1 < len g ) ; :: thesis:
A755: 1 < j by A753, NAT_1:12;
A756: 1 <= i + 1 by NAT_1:12;
A757: j <= j + 1 by NAT_1:12;
then A758: i + 1 < j + 1 by A753, XXREAL_0:2;
i < j by A753, NAT_1:13;
then A759: i < j + 1 by A757, XXREAL_0:2;

per cases by A754, NAT_1:14;

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

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

now :: thesis:

per cases by A768, A784;

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

then A795: i1 = i19 by A762, A765, A767, A769, A772, A776, A770, A779, A781, A783, A785, A791, A789, A786, A792, GOBOARD7:19;

now :: thesis:

per cases by A762, A765, A767, A769, A772, A776, A770, A779, A781, A783, A785, A791, A789, A786, A792, A794, GOBOARD7:22;

suppose j1 = j19 ; :: thesis:

hence contradiction by A711, A753, A757, A755, A760, A763, A765, A781, A795; :: thesis:

end;

suppose j1 = j19 + 1 ; :: thesis:

hence contradiction by A739, A759, A760, A765, A778, A783, A794, A795; :: thesis:

end;

suppose j1 + 1 = j19 ; :: thesis:

hence contradiction by A711, A753, A756, A755, A760, A761, A767, A781, A794, A795; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A762, A765, A767, A769, A772, A776, A770, A779, A781, A783, A785, A789, A787, A790, A792, A796, GOBOARD7:21;

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

hence contradiction by A711, A753, A757, A755, A760, A763, A765, A781; :: thesis:

end;

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

hence contradiction by A739, A753, A760, A777, A767, A781, A796; :: thesis:

end;

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

hence contradiction by A739, A759, A760, A765, A778, A783, A796; :: thesis:

end;

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

hence contradiction by A739, A758, A777, A767, A778, A783, A796; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A762, A765, A767, A769, A772, A776, A770, A779, A781, A783, A791, A789, A787, A793, A792, A797, GOBOARD7:21;

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

hence contradiction by A739, A759, A760, A765, A778, A783, A797; :: thesis:

end;

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

hence contradiction by A739, A758, A777, A767, A778, A783, A797; :: thesis:

end;

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

hence contradiction by A711, A753, A757, A755, A760, A763, A765, A781, A797; :: thesis:

end;

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

hence contradiction by A711, A753, A756, A755, A760, A761, A767, A781, A797; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A799: i1 = i19 by A762, A765, A767, A769, A772, A776, A770, A779, A781, A783, A785, A791, A787, A788, A792, GOBOARD7:19;

now :: thesis:

per cases by A762, A765, A767, A769, A772, A776, A770, A779, A781, A783, A785, A791, A787, A788, A792, A798, GOBOARD7:22;

suppose j1 = j29 ; :: thesis:

hence contradiction by A711, A753, A756, A755, A760, A761, A767, A781, A798, A799; :: thesis:

end;

suppose j1 = j29 + 1 ; :: thesis:

hence contradiction by A711, A753, A757, A755, A760, A763, A765, A781, A798, A799; :: thesis:

end;

suppose j1 + 1 = j29 ; :: thesis:

hence contradiction by A739, A758, A777, A767, A778, A783, A798, A799; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A762, A765, A767, A769, A776, A774, A775, A779, A781, A783, A785, A791, A789, A786, A792, A800, GOBOARD7:21;

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

hence contradiction by A711, A753, A757, A755, A760, A763, A765, A781; :: thesis:

end;

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

hence contradiction by A739, A759, A760, A765, A778, A783, A800; :: thesis:

end;

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

hence contradiction by A711, A753, A756, A755, A760, A761, A767, A781, A800; :: thesis:

end;

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

hence contradiction by A739, A758, A777, A767, A778, A783, A800; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A802: j1 = j19 by A762, A765, A767, A769, A776, A774, A775, A779, A781, A783, A785, A789, A787, A790, A792, GOBOARD7:20;

now :: thesis:

per cases by A762, A765, A767, A769, A776, A774, A775, A779, A781, A783, A785, A789, A787, A790, A792, A801, GOBOARD7:23;

suppose i1 = i19 ; :: thesis:

hence contradiction by A711, A753, A757, A755, A760, A763, A765, A781, A802; :: thesis:

end;

suppose i1 = i19 + 1 ; :: thesis:

hence contradiction by A739, A759, A760, A765, A778, A783, A801, A802; :: thesis:

end;

suppose i1 + 1 = i19 ; :: thesis:

hence contradiction by A711, A753, A756, A755, A760, A761, A767, A781, A801, A802; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A804: j1 = j19 by A762, A765, A767, A769, A776, A774, A775, A779, A781, A783, A791, A789, A787, A793, A792, GOBOARD7:20;

now :: thesis:

per cases by A762, A765, A767, A769, A776, A774, A775, A779, A781, A783, A791, A789, A787, A793, A792, A803, GOBOARD7:23;

suppose i1 = i29 ; :: thesis:

hence contradiction by A739, A759, A760, A765, A778, A783, A803, A804; :: thesis:

end;

suppose i1 = i29 + 1 ; :: thesis:

hence contradiction by A711, A753, A757, A755, A760, A763, A765, A781, A803, A804; :: thesis:

end;

suppose i1 + 1 = i29 ; :: thesis:

hence contradiction by A739, A758, A777, A767, A778, A783, A803, A804; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A762, A765, A767, A769, A776, A774, A775, A779, A781, A783, A785, A791, A787, A788, A792, A805, GOBOARD7:21;

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

hence contradiction by A739, A759, A760, A765, A778, A783, A805; :: thesis:

end;

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

hence contradiction by A711, A753, A757, A755, A760, A763, A765, A781, A805; :: thesis:

end;

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

hence contradiction by A739, A758, A777, A767, A778, A783, A805; :: thesis:

end;

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

hence contradiction by A711, A753, A756, A755, A760, A761, A767, A781, A805; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A762, A765, A767, A772, A776, A774, A771, A779, A781, A783, A785, A791, A789, A786, A792, A806, GOBOARD7:21;

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

hence contradiction by A711, A753, A756, A755, A760, A761, A767, A781, A806; :: thesis:

end;

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

hence contradiction by A739, A758, A777, A767, A778, A783, A806; :: thesis:

end;

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

hence contradiction by A711, A753, A757, A755, A760, A763, A765, A781, A806; :: thesis:

end;

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

hence contradiction by A739, A759, A760, A765, A778, A783, A806; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A808: j1 = j19 by A762, A765, A767, A772, A776, A774, A771, A779, A781, A783, A785, A789, A787, A790, A792, GOBOARD7:20;

now :: thesis:

per cases by A762, A765, A767, A772, A776, A774, A771, A779, A781, A783, A785, A789, A787, A790, A792, A807, GOBOARD7:23;

suppose i2 = i19 ; :: thesis:

hence contradiction by A711, A753, A756, A755, A760, A761, A767, A781, A807, A808; :: thesis:

end;

suppose i2 = i19 + 1 ; :: thesis:

hence contradiction by A739, A758, A777, A767, A778, A783, A807, A808; :: thesis:

end;

suppose i2 + 1 = i19 ; :: thesis:

hence contradiction by A711, A753, A757, A755, A760, A763, A765, A781, A807, A808; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A810: j1 = j19 by A762, A765, A767, A772, A776, A774, A771, A779, A781, A783, A791, A789, A787, A793, A792, GOBOARD7:20;

now :: thesis:

per cases by A762, A765, A767, A772, A776, A774, A771, A779, A781, A783, A791, A789, A787, A793, A792, A809, GOBOARD7:23;

suppose i2 = i29 ; :: thesis:

hence contradiction by A739, A758, A777, A767, A778, A783, A809, A810; :: thesis:

end;

suppose i2 = i29 + 1 ; :: thesis:

hence contradiction by A711, A753, A756, A755, A760, A761, A767, A781, A809, A810; :: thesis:

end;

suppose i2 + 1 = i29 ; :: thesis:

hence contradiction by A739, A759, A760, A765, A778, A783, A809, A810; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A762, A765, A767, A772, A776, A774, A771, A779, A781, A783, A785, A791, A787, A788, A792, A811, GOBOARD7:21;

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

hence contradiction by A739, A758, A777, A767, A778, A783, A811; :: thesis:

end;

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

hence contradiction by A711, A753, A756, A755, A760, A761, A767, A781, A811; :: thesis:

end;

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

hence contradiction by A739, A759, A760, A765, A778, A783, A811; :: thesis:

end;

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

hence contradiction by A711, A753, A757, A755, A760, A763, A765, A781, A811; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A813: i1 = i19 by A762, A765, A767, A769, A772, A774, A773, A779, A781, A783, A785, A791, A789, A786, A792, GOBOARD7:19;

now :: thesis:

per cases by A762, A765, A767, A769, A772, A774, A773, A779, A781, A783, A785, A791, A789, A786, A792, A812, GOBOARD7:22;

suppose j2 = j19 ; :: thesis:

hence contradiction by A711, A753, A756, A755, A760, A761, A767, A781, A812, A813; :: thesis:

end;

suppose j2 = j19 + 1 ; :: thesis:

hence contradiction by A739, A758, A777, A767, A778, A783, A812, A813; :: thesis:

end;

suppose j2 + 1 = j19 ; :: thesis:

hence contradiction by A711, A753, A757, A755, A760, A763, A765, A781, A812, A813; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A762, A765, A767, A769, A772, A774, A773, A779, A781, A783, A785, A789, A787, A790, A792, A814, GOBOARD7:21;

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

hence contradiction by A711, A753, A756, A755, A760, A761, A767, A781, A814; :: thesis:

end;

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

hence contradiction by A711, A753, A757, A755, A760, A763, A765, A781, A814; :: thesis:

end;

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

hence contradiction by A739, A758, A777, A767, A778, A783, A814; :: thesis:

end;

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

hence contradiction by A739, A759, A760, A765, A778, A783, A814; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A762, A765, A767, A769, A772, A774, A773, A779, A781, A783, A791, A789, A787, A793, A792, A815, GOBOARD7:21;

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

hence contradiction by A739, A758, A777, A767, A778, A783, A815; :: thesis:

end;

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

hence contradiction by A739, A759, A760, A765, A778, A783, A815; :: thesis:

end;

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

hence contradiction by A711, A753, A756, A755, A760, A761, A767, A781, A815; :: thesis:

end;

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

hence contradiction by A711, A753, A757, A755, A760, A763, A765, A781, A815; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A817: i1 = i19 by A762, A765, A767, A769, A772, A774, A773, A779, A781, A783, A785, A791, A787, A788, A792, GOBOARD7:19;

now :: thesis:

per cases by A762, A765, A767, A769, A772, A774, A773, A779, A781, A783, A785, A791, A787, A788, A792, A816, GOBOARD7:22;

suppose j2 = j29 ; :: thesis:

hence contradiction by A739, A758, A777, A767, A778, A783, A816, A817; :: thesis:

end;

suppose j2 = j29 + 1 ; :: thesis:

hence contradiction by A711, A753, A756, A755, A760, A761, A767, A781, A816, A817; :: thesis:

end;

suppose j2 + 1 = j29 ; :: thesis:

hence contradiction by A739, A759, A760, A765, A778, A783, A816, A817; :: 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 3;
hence (LSeg (g,i)) /\ (LSeg (g,j)) = {} ; :: according to XBOOLE_0:def 7 :: thesis:

end;

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

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

now :: thesis:

per cases by A842, A823;

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

then A853: i1 = i19 by A836, A839, A841, A843, A849, A847, A844, A850, A820, A822, A824, A827, A831, A825, A832, GOBOARD7:19;

now :: thesis:

per cases by A836, A839, A841, A843, A849, A847, A844, A850, A820, A822, A824, A827, A831, A825, A832, A852, GOBOARD7:22;

suppose j1 = j19 ; :: thesis:

hence contradiction by A711, A753, A757, A755, A818, A837, A834, A839, A820, A853; :: thesis:

end;

suppose j1 = j19 + 1 ; :: thesis:

hence contradiction by A747, A759, A818, A839, A822, A852, A853; :: thesis:

end;

suppose j1 + 1 = j19 ; :: thesis:

hence contradiction by A711, A753, A756, A755, A835, A834, A841, A820, A852, A853; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A836, A839, A841, A843, A849, A847, A844, A850, A820, A822, A824, A831, A829, A830, A832, A854, GOBOARD7:21;

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

hence contradiction by A711, A753, A757, A755, A818, A837, A834, A839, A820; :: thesis:

end;

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

hence contradiction by A739, A753, A833, A834, A841, A820, A854; :: thesis:

end;

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

hence contradiction by A747, A759, A818, A839, A822, A854; :: thesis:

end;

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

hence contradiction by A739, A758, A818, A833, A841, A822, A854; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A836, A839, A841, A843, A849, A847, A844, A850, A820, A822, A827, A831, A829, A826, A832, A855, GOBOARD7:21;

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

hence contradiction by A747, A759, A818, A839, A822, A855; :: thesis:

end;

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

hence contradiction by A739, A758, A818, A833, A841, A822, A855; :: thesis:

end;

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

hence contradiction by A711, A753, A757, A755, A818, A837, A834, A839, A820, A855; :: thesis:

end;

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

hence contradiction by A711, A753, A756, A755, A835, A834, A841, A820, A855; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A857: i1 = i19 by A836, A839, A841, A843, A849, A847, A844, A850, A820, A822, A824, A827, A829, A828, A832, GOBOARD7:19;

now :: thesis:

per cases by A836, A839, A841, A843, A849, A847, A844, A850, A820, A822, A824, A827, A829, A828, A832, A856, GOBOARD7:22;

suppose j1 = j29 ; :: thesis:

hence contradiction by A711, A753, A756, A755, A835, A834, A841, A820, A856, A857; :: thesis:

end;

suppose j1 = j29 + 1 ; :: thesis:

hence contradiction by A711, A753, A757, A755, A818, A837, A834, A839, A820, A856, A857; :: thesis:

end;

suppose j1 + 1 = j29 ; :: thesis:

hence contradiction by A739, A758, A818, A833, A841, A822, A856, A857; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A836, A839, A841, A843, A847, A845, A848, A850, A820, A822, A824, A827, A831, A825, A832, A858, GOBOARD7:21;

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

hence contradiction by A711, A753, A757, A755, A818, A837, A834, A839, A820; :: thesis:

end;

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

hence contradiction by A747, A759, A818, A839, A822, A858; :: thesis:

end;

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

hence contradiction by A711, A753, A756, A755, A835, A834, A841, A820, A858; :: thesis:

end;

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

hence contradiction by A739, A758, A818, A833, A841, A822, A858; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A860: j1 = j19 by A836, A839, A841, A843, A847, A845, A848, A850, A820, A822, A824, A831, A829, A830, A832, GOBOARD7:20;

now :: thesis:

per cases by A836, A839, A841, A843, A847, A845, A848, A850, A820, A822, A824, A831, A829, A830, A832, A859, GOBOARD7:23;

suppose i1 = i19 ; :: thesis:

hence contradiction by A711, A753, A757, A755, A818, A837, A834, A839, A820, A860; :: thesis:

end;

suppose i1 = i19 + 1 ; :: thesis:

hence contradiction by A747, A759, A818, A839, A822, A859, A860; :: thesis:

end;

suppose i1 + 1 = i19 ; :: thesis:

hence contradiction by A711, A753, A756, A755, A835, A834, A841, A820, A859, A860; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A862: j1 = j19 by A836, A839, A841, A843, A847, A845, A848, A850, A820, A822, A827, A831, A829, A826, A832, GOBOARD7:20;

now :: thesis:

per cases by A836, A839, A841, A843, A847, A845, A848, A850, A820, A822, A827, A831, A829, A826, A832, A861, GOBOARD7:23;

suppose i1 = i29 ; :: thesis:

hence contradiction by A747, A759, A818, A839, A822, A861, A862; :: thesis:

end;

suppose i1 = i29 + 1 ; :: thesis:

hence contradiction by A711, A753, A757, A755, A818, A837, A834, A839, A820, A861, A862; :: thesis:

end;

suppose i1 + 1 = i29 ; :: thesis:

hence contradiction by A739, A758, A818, A833, A841, A822, A861, A862; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A836, A839, A841, A843, A847, A845, A848, A850, A820, A822, A824, A827, A829, A828, A832, A863, GOBOARD7:21;

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

hence contradiction by A747, A759, A818, A839, A822, A863; :: thesis:

end;

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

hence contradiction by A711, A753, A757, A755, A818, A837, A834, A839, A820, A863; :: thesis:

end;

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

hence contradiction by A739, A758, A818, A833, A841, A822, A863; :: thesis:

end;

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

hence contradiction by A711, A753, A756, A755, A835, A834, A841, A820, A863; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A836, A839, A841, A849, A847, A845, A851, A850, A820, A822, A824, A827, A831, A825, A832, A864, GOBOARD7:21;

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

hence contradiction by A711, A753, A756, A755, A835, A834, A841, A820, A864; :: thesis:

end;

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

hence contradiction by A739, A758, A818, A833, A841, A822, A864; :: thesis:

end;

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

hence contradiction by A711, A753, A757, A755, A818, A837, A834, A839, A820, A864; :: thesis:

end;

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

hence contradiction by A747, A759, A818, A839, A822, A864; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A866: j1 = j19 by A836, A839, A841, A849, A847, A845, A851, A850, A820, A822, A824, A831, A829, A830, A832, GOBOARD7:20;

now :: thesis:

per cases by A836, A839, A841, A849, A847, A845, A851, A850, A820, A822, A824, A831, A829, A830, A832, A865, GOBOARD7:23;

suppose i2 = i19 ; :: thesis:

hence contradiction by A711, A753, A756, A755, A835, A834, A841, A820, A865, A866; :: thesis:

end;

suppose i2 = i19 + 1 ; :: thesis:

hence contradiction by A739, A758, A818, A833, A841, A822, A865, A866; :: thesis:

end;

suppose i2 + 1 = i19 ; :: thesis:

hence contradiction by A711, A753, A757, A755, A818, A837, A834, A839, A820, A865, A866; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A868: j1 = j19 by A836, A839, A841, A849, A847, A845, A851, A850, A820, A822, A827, A831, A829, A826, A832, GOBOARD7:20;

now :: thesis:

per cases by A836, A839, A841, A849, A847, A845, A851, A850, A820, A822, A827, A831, A829, A826, A832, A867, GOBOARD7:23;

suppose i2 = i29 ; :: thesis:

hence contradiction by A739, A758, A818, A833, A841, A822, A867, A868; :: thesis:

end;

suppose i2 = i29 + 1 ; :: thesis:

hence contradiction by A711, A753, A756, A755, A835, A834, A841, A820, A867, A868; :: thesis:

end;

suppose i2 + 1 = i29 ; :: thesis:

hence contradiction by A747, A759, A818, A839, A822, A867, A868; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A836, A839, A841, A849, A847, A845, A851, A850, A820, A822, A824, A827, A829, A828, A832, A869, GOBOARD7:21;

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

hence contradiction by A739, A758, A818, A833, A841, A822, A869; :: thesis:

end;

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

hence contradiction by A711, A753, A756, A755, A835, A834, A841, A820, A869; :: thesis:

end;

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

hence contradiction by A747, A759, A818, A839, A822, A869; :: thesis:

end;

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

hence contradiction by A711, A753, A757, A755, A818, A837, A834, A839, A820, A869; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A871: i1 = i19 by A836, A839, A841, A843, A849, A845, A846, A850, A820, A822, A824, A827, A831, A825, A832, GOBOARD7:19;

now :: thesis:

per cases by A836, A839, A841, A843, A849, A845, A846, A850, A820, A822, A824, A827, A831, A825, A832, A870, GOBOARD7:22;

suppose j2 = j19 ; :: thesis:

hence contradiction by A711, A753, A756, A755, A835, A834, A841, A820, A870, A871; :: thesis:

end;

suppose j2 = j19 + 1 ; :: thesis:

hence contradiction by A739, A758, A818, A833, A841, A822, A870, A871; :: thesis:

end;

suppose j2 + 1 = j19 ; :: thesis:

hence contradiction by A711, A753, A757, A755, A818, A837, A834, A839, A820, A870, A871; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A836, A839, A841, A843, A849, A845, A846, A850, A820, A822, A824, A831, A829, A830, A832, A872, GOBOARD7:21;

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

hence contradiction by A711, A753, A756, A755, A835, A834, A841, A820, A872; :: thesis:

end;

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

hence contradiction by A711, A753, A757, A755, A818, A837, A834, A839, A820, A872; :: thesis:

end;

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

hence contradiction by A739, A758, A818, A833, A841, A822, A872; :: thesis:

end;

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

hence contradiction by A747, A759, A818, A839, A822, A872; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

now :: thesis:

per cases by A836, A839, A841, A843, A849, A845, A846, A850, A820, A822, A827, A831, A829, A826, A832, A873, GOBOARD7:21;

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

hence contradiction by A739, A758, A818, A833, A841, A822, A873; :: thesis:

end;

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

hence contradiction by A747, A759, A818, A839, A822, A873; :: thesis:

end;

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

hence contradiction by A711, A753, A756, A755, A835, A834, A841, A820, A873; :: thesis:

end;

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

hence contradiction by A711, A753, A757, A755, A818, A837, A834, A839, A820, A873; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A875: i1 = i19 by A836, A839, A841, A843, A849, A845, A846, A850, A820, A822, A824, A827, A829, A828, A832, GOBOARD7:19;

now :: thesis:

per cases by A836, A839, A841, A843, A849, A845, A846, A850, A820, A822, A824, A827, A829, A828, A832, A874, GOBOARD7:22;

suppose j2 = j29 ; :: thesis:

hence contradiction by A739, A758, A818, A833, A841, A822, A874, A875; :: thesis:

end;

suppose j2 = j29 + 1 ; :: thesis:

hence contradiction by A711, A753, A756, A755, A835, A834, A841, A820, A874, A875; :: thesis:

end;

suppose j2 + 1 = j29 ; :: thesis:

hence contradiction by A747, A759, A818, A839, A822, A874, A875; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then reconsider g = g as non constant standard special_circular_sequence by A651, A738, A702, A705, A707, FINSEQ_6:def 1, JORDAN8:4;
reconsider Lg9 = (L~ g) ` as Subset of (TOP-REAL 2) ;
A876: C c= Lg9

proof

let c be object ; :: according to TARSKI:def 3 :: thesis:
assume that
A877: c in C and
A878: not c in Lg9 ; :: thesis:
reconsider c = c as Point of (TOP-REAL 2) by A877;
consider i being Nat such that
A879: 1 <= i and
A880: i + 1 <= len g and
A881: c in LSeg ((g /. i),(g /. (i + 1))) by A878, SPPOL_2:14, SUBSET_1:29;
A882: 1 <= i + (m -' 1) by A879, NAT_1:12;
i + 1 in dom g by A879, A880, SEQ_4:134;
then A883: g /. (i + 1) = f /. ((i + 1) + (m -' 1)) by FINSEQ_5:27;
(i + 1) + (m -' 1) = (i + (m -' 1)) + 1 ;
then A884: (i + (m -' 1)) + 1 <= (len g) + (m -' 1) by A880, XREAL_1:6;
i in dom g by A879, A880, SEQ_4:134;
then g /. i = f /. (i + (m -' 1)) by FINSEQ_5:27;
then c in LSeg (f,(i + (m -' 1))) by A701, A881, A883, A882, A884, TOPREAL1:def 3;
then c in (right_cell (f,(i + (m -' 1)),(Gauge (C,n)))) /\ (left_cell (f,(i + (m -' 1)),(Gauge (C,n)))) by A440, A701, A882, A884, GOBRD13:29;
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 A877, XBOOLE_0:3;
hence contradiction by A440, A701, A882, A884; :: thesis:

end;

A885: LeftComp g is_a_component_of (L~ g) ` by GOBOARD9:def 1;
(L~ g) ` is open by TOPS_1:3;
then A886: (L~ g) ` = Int ((L~ g) `) by TOPS_1:23;
A887: C meets LeftComp g

proof

left_cell (f,m,(Gauge (C,n))) meets C by A440, A652, A659;
then consider p being object such that
A888: p in left_cell (f,m,(Gauge (C,n))) and
A889: p in C by XBOOLE_0:3;
reconsider p = p as Element of (TOP-REAL 2) by A888;

now :: thesis:

reconsider u = p as Element of (Euclid 2) by TOPREAL3:8;
take p = p; :: thesis:
thus p in C by A889; :: thesis:
A890: Int (left_cell (g,1)) c= LeftComp g by A704, GOBOARD9:21;
Int (left_cell (g,1,(Gauge (C,n)))) c= Int (left_cell (g,1)) by A705, A704, GOBRD13:33, TOPS_1:19;
then Int (left_cell (g,1,(Gauge (C,n)))) c= LeftComp g by A890;
then Int (left_cell (f,((m -' 1) + 1),(Gauge (C,n)))) c= LeftComp g by A653, A700, A704, GOBRD13:32;
then A891: Int (left_cell (f,m,(Gauge (C,n)))) c= LeftComp g by A652, XREAL_1:235;
consider r being Real such that
A892: r > 0 and
A893: Ball (u,r) c= (L~ g) ` by A876, A886, A889, GOBOARD6:5;
reconsider r = r as Real ;
reconsider B = Ball (u,r) as non empty Subset of (TOP-REAL 2) by A4, A892, TBSP_1:11, TOPMETR:12;
A894: B is open by GOBOARD6:3;
A895: left_cell (f,m,(Gauge (C,n))) = Cl (Int (left_cell (f,m,(Gauge (C,n))))) by A652, A659, A680;
p in Ball (u,r) by A892, TBSP_1:11;
then A896: Int (left_cell (f,m,(Gauge (C,n)))) meets B by A888, A895, A894, TOPS_1:12;
A897: p in B by A892, TBSP_1:11;
B is connected by SPRECT_3:7;
then B c= LeftComp g by A885, A893, A891, A896, GOBOARD9:4;
hence p in LeftComp g by A897; :: thesis:

end;

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

end;

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

proof

A900: for n being Nat st 1 <= n holds
(n -' 1) + 2 = n + 1

proof

let n be 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 A901: 1 < m by A652, XXREAL_0:1;
A902: for n being Nat st 1 <= n & n <= m -' 1 holds
not f /. n in L~ g

proof

A903: 2 <= len (Gauge (C,n)) by A2, NAT_1:12;
let n be Nat; :: thesis:
assume that
A904: 1 <= n and
A905: n <= m -' 1 ; :: thesis:
set p = f /. n;
A906: n <= len f by A700, A905, XXREAL_0:2;
then A907: f /. n in Values (Gauge (C,n)) by A440, A904, JORDAN9:6;
assume f /. n in L~ g ; :: thesis:
then consider j being Nat such that
A908: (m -' 1) + 1 <= j and
A909: j + 1 <= len f and
A910: f /. n in LSeg (f,j) by A700, JORDAN9:7;
A911: j + 1 <= k by A177, A909;
A912: j < k by A710, A909, NAT_1:13;
A913: n < (m -' 1) + 1 by A905, NAT_1:13;
then A914: n < j by A908, XXREAL_0:2;
A915: (m -' 1) + 1 = m by A652, XREAL_1:235;
then A916: 1 < j by A901, A908, XXREAL_0:2;

per cases by A6, A440, A909, A910, A916, A903, A907, JORDAN9:23;

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

A918: n <> len (F . j) by A177, A908, A913;
n <= len (F . j) by A177, A914;
then A919: n in dom (F . j) by A904, FINSEQ_3:25;
(F . j) /. n = (F . n) /. n by A566, A904, A914
.= f /. n by A710, A566, A904, A906
.= (F . j) /. j by A566, A916, A912, A917
.= (F . j) /. (len (F . j)) by A177 ;
hence contradiction by A648, A916, A912, A919, A918; :: thesis:

end;

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

now :: thesis:

per cases by A911, XXREAL_0:1;

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

A922: n <> len (F . m) by A177, A913, A915;
n <= len (F . m) by A177, A913, A915;
then A923: n in dom (F . m) by A904, FINSEQ_3:25;
(F . m) /. n = (F . n) /. n by A566, A904, A913, A915
.= f /. n by A710, A566, A904, A906
.= (F . m) /. m by A651, A710, A652, A654, A566, A920, A921
.= (F . m) /. (len (F . m)) by A177 ;
hence contradiction by A648, A710, A652, A655, A923, A922; :: thesis:

end;

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

set l = j + 1;
A925: 1 <= j + 1 by NAT_1:11;
A926: n < n + 1 by XREAL_1:29;
A927: n + 1 < j + 1 by A914, XREAL_1:6;
then A928: n <> len (F . (j + 1)) by A177, A926;
A929: n < j + 1 by A926, A927, XXREAL_0:2;
then n <= len (F . (j + 1)) by A177;
then A930: n in dom (F . (j + 1)) by A904, FINSEQ_3:25;
(F . (j + 1)) /. n = (F . n) /. n by A566, A904, A929
.= f /. n by A710, A566, A904, A906
.= (F . (j + 1)) /. (j + 1) by A566, A920, A924, A925
.= (F . (j + 1)) /. (len (F . (j + 1))) by A177 ;
hence contradiction by A648, A924, A930, A928, NAT_1:11; :: thesis:

end;

hence contradiction ; :: thesis:

end;

C meets LeftComp (Rev g)

proof

1 <= len g by A704, XREAL_1:145;
then A931: ((len g) -' 1) + 2 = (len g) + 1 by A900;
A932: 1 - 1 < m - 1 by A901, XREAL_1:9;
A933: (m -' 1) + 2 = m + 1 by A652, A900;
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;
A934: (1 + 1) - 1 <= (len g) - 1 by A703, XREAL_1:9;
(1 + 1) -' 1 <= (len g) -' 1 by A703, NAT_D:42;
then A935: 1 <= (len g) -' 1 by NAT_D:34;
then (m -' 1) + 1 <= (m -' 1) + ((len g) -' 1) by XREAL_1:6;
then m -' 1 < (m -' 1) + ((len g) -' 1) by NAT_1:13;
then A936: m -' 1 <> len (F . ((m -' 1) + ((len g) -' 1))) by A177;
A937: 1 + 1 <= len (Rev g) by A703, FINSEQ_5:def 3;
then (1 + 1) -' 1 <= (len (Rev g)) -' 1 by NAT_D:42;
then A938: 1 <= (len (Rev g)) -' 1 by NAT_D:34;
A939: Rev g is_sequence_on Gauge (C,n) by A705, JORDAN9:5;
then consider p1, p2, q1, q2 being Nat such that
A940: [p1,p2] in Indices (Gauge (C,n)) and
A941: (Rev g) /. 1 = (Gauge (C,n)) * (p1,p2) and
A942: [q1,q2] in Indices (Gauge (C,n)) and
A943: (Rev g) /. 2 = (Gauge (C,n)) * (q1,q2) and
A944: ( ( p1 = q1 & p2 + 1 = q2 ) or ( p1 + 1 = q1 & p2 = q2 ) or ( p1 = q1 + 1 & p2 = q2 ) or ( p1 = q1 & p2 = q2 + 1 ) ) by A937, JORDAN8:3;
A945: 1 <= p1 by A940, MATRIX_0:32;
A946: p2 <= width (Gauge (C,n)) by A940, MATRIX_0:32;
A947: p1 <= len (Gauge (C,n)) by A940, MATRIX_0:32;
A948: 1 <= p2 by A940, MATRIX_0:32;
A949: (Rev g) /. 1 = f /. m by A651, A702, FINSEQ_5:65;
(len g) -' 1 <= len g by NAT_D:44;
then A950: (len g) -' 1 in dom g by A935, FINSEQ_3:25;
then A951: (Rev g) /. 2 = g /. ((len g) -' 1) by A931, FINSEQ_5:66
.= f /. ((m -' 1) + ((len g) -' 1)) by A950, FINSEQ_5:27 ;
1 < len (Rev g) by A937, NAT_1:13;
then A952: ((len (Rev g)) -' 1) + 1 = len (Rev g) by XREAL_1:235;
A953: (m -' 1) + ((len g) -' 1) = (m + ((len g) -' 1)) -' 1 by A652, NAT_D:38
.= (((len g) -' 1) + m) - 1 by A935, NAT_D:37
.= (((len g) - 1) + m) - 1 by A934, XREAL_0:def 2
.= (((k - (m - 1)) - 1) + m) - 1 by A710, A701, A932, XREAL_0:def 2
.= k - 1 ;
then A954: (Rev g) /. 1 = f /. (((m -' 1) + ((len g) -' 1)) + 1) by A710, A702, FINSEQ_5:65;
A955: (m -' 1) + 1 = m by A652, XREAL_1:235;
then A956: 1 <= m -' 1 by A901, NAT_1:13;
then A957: left_cell (f,(m -' 1),(Gauge (C,n))) meets C by A440, A654, A955;
m -' 1 <= (m -' 1) + ((len g) -' 1) by NAT_1:11;
then m -' 1 <= len (F . ((m -' 1) + ((len g) -' 1))) by A177;
then A958: m -' 1 in dom (F . ((m -' 1) + ((len g) -' 1))) by A956, FINSEQ_3:25;
not f /. (m -' 1) in L~ g by A902, A956;
then A959: not f /. (m -' 1) in L~ (Rev g) by SPPOL_2:22;
A960: k = ((m -' 1) + ((len g) -' 1)) + 1 by A953;
then A961: (m -' 1) + ((len g) -' 1) < k by XREAL_1:29;
(len g) -' 1 <= (m -' 1) + ((len g) -' 1) by NAT_1:11;
then A962: 1 <= (m -' 1) + ((len g) -' 1) by A935, XXREAL_0:2;
then A963: left_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) meets C by A440, A710, A960;

per cases by A944;

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

consider a1, a2, p91, p92 being Nat such that
A965: [a1,a2] in Indices (Gauge (C,n)) and
A966: f /. (m -' 1) = (Gauge (C,n)) * (a1,a2) and
A967: [p91,p92] in Indices (Gauge (C,n)) and
A968: (Rev g) /. 1 = (Gauge (C,n)) * (p91,p92) and
A969: ( ( a1 = p91 & a2 + 1 = p92 ) or ( a1 + 1 = p91 & a2 = p92 ) or ( a1 = p91 + 1 & a2 = p92 ) or ( a1 = p91 & a2 = p92 + 1 ) ) by A653, A654, A949, A955, A956, JORDAN8:3;
A970: 1 <= a2 by A965, MATRIX_0:32;
thus C meets LeftComp (Rev g) :: thesis:

proof

per cases by A969;

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

A972: m -' 1 <= m by A955, NAT_1:11;
A973: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A710, A700, A566, A956
.= (F . m) /. (m -' 1) by A566, A956, A972 ;
A974: 2 in dom g by A703, FINSEQ_3:25;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A931, FINSEQ_5:def 3;
then A975: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A974, FINSEQ_5:66
.= f /. (m + 1) by A933, A974, FINSEQ_5:27 ;
A976: L~ (Rev g) c= L~ f by A898, SPPOL_2:22;
A977: (Rev g) /. 1 = g /. 1 by A651, A738, A702, FINSEQ_5:65
.= (Rev g) /. (len g) by FINSEQ_5:65
.= (Rev g) /. (len (Rev g)) by FINSEQ_5:def 3 ;
A978: (F . k) | (m + 1) = F . (m + 1) by A565, A710, A659;
A979: a1 = p1 by A940, A941, A967, A968, A971, GOBOARD1:5;
A980: f /. ((m -' 1) + 1) = (F . m) /. m by A710, A652, A654, A566, A955;
A981: (m -' 1) + 1 <= len (F . m) by A177, A955;
set rc = (left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g));
A982: a2 + 1 > a2 by NAT_1:13;
A983: a2 + 1 = p2 by A940, A941, A967, A968, A971, GOBOARD1:5;
then A984: 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 A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A964, GOBRD13:27
.= front_right_cell ((F . m),(m -' 1),(Gauge (C,n))) by A440, A949, A955, A956, A940, A941, A965, A966, A979, A983, A981, A973, A980, GOBRD13:35 ;
then F . (m + 1) turns_right m -' 1, Gauge (C,n) by A514, A901, A963;
then A985: f turns_right m -' 1, Gauge (C,n) by A956, A933, A978, GOBRD13:43;
A986: p2 + 1 > a2 + 1 by A983, NAT_1:13;
then A987: [(p1 + 1),p2] in Indices (Gauge (C,n)) by A949, A955, A940, A941, A965, A966, A982, A985, GOBRD13:def 6;
then A988: p1 + 1 <= len (Gauge (C,n)) by MATRIX_0:32;
f /. (m + 1) = (Gauge (C,n)) * ((p1 + 1),p2) by A949, A955, A933, A940, A941, A965, A966, A986, A982, A985, GOBRD13:def 6;
then left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),p1,a2) by A939, A938, A952, A940, A941, A987, A984, A975, A977, GOBRD13:25;
then f /. (m -' 1) in left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) by A945, A946, A966, A970, A979, A983, A988, JORDAN9:20;
then A989: f /. (m -' 1) in (left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g)) by A959, XBOOLE_0:def 5;
A990: 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 A939, A938, A952, JORDAN9:27;
hence C meets LeftComp (Rev g) by A654, A660, A955, A956, A959, A989, A976, A990; :: thesis:

end;

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

then a1 + 1 = p1 by A940, A941, A967, A968, GOBOARD1:5;
then A992: q1 -' 1 = a1 by A964, NAT_D:34;
a2 = p2 by A940, A941, A967, A968, A991, GOBOARD1:5;
then right_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) = cell ((Gauge (C,n)),a1,a2) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A964, A992, GOBRD13:28
.= left_cell (f,(m -' 1),(Gauge (C,n))) by A440, A654, A949, A955, A956, A965, A966, A967, A968, A991, GOBRD13:23 ;
hence C meets LeftComp (Rev g) by A440, A710, A960, A962, A957; :: thesis:

end;

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

then A994: a2 = p2 by A940, A941, A967, A968, GOBOARD1:5;
a1 = p1 + 1 by A940, A941, A967, A968, A993, GOBOARD1:5;
then right_cell (f,(m -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),p1,p2) by A651, A653, A654, A702, A955, A956, A940, A941, A965, A966, A994, FINSEQ_5:65, GOBRD13:26
.= left_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A964, GOBRD13:27 ;
hence C meets LeftComp (Rev g) by A440, A654, A955, A956, A963; :: thesis:

end;

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

then A996: a2 = q2 by A940, A941, A964, A967, A968, GOBOARD1:5;
A997: a1 = q1 by A940, A941, A964, A967, A968, A995, GOBOARD1:5;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A566, A956, NAT_1:11
.= (Rev g) /. 2 by A710, A700, A566, A956, A943, A966, A997, A996
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A566, A961, A962, A951
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A177 ;
hence C meets LeftComp (Rev g) by A648, A961, A962, A958, A936; :: thesis:

end;

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

consider a1, a2, p91, p92 being Nat such that
A999: [a1,a2] in Indices (Gauge (C,n)) and
A1000: f /. (m -' 1) = (Gauge (C,n)) * (a1,a2) and
A1001: [p91,p92] in Indices (Gauge (C,n)) and
A1002: (Rev g) /. 1 = (Gauge (C,n)) * (p91,p92) and
A1003: ( ( a1 = p91 & a2 + 1 = p92 ) or ( a1 + 1 = p91 & a2 = p92 ) or ( a1 = p91 + 1 & a2 = p92 ) or ( a1 = p91 & a2 = p92 + 1 ) ) by A653, A654, A949, A955, A956, JORDAN8:3;
A1004: 1 <= a2 by A999, MATRIX_0:32;
A1005: a2 <= width (Gauge (C,n)) by A999, MATRIX_0:32;
A1006: 1 <= a1 by A999, MATRIX_0:32;
thus C meets LeftComp (Rev g) :: thesis:

proof

per cases by A1003;

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

then a2 + 1 = p2 by A940, A941, A1001, A1002, GOBOARD1:5;
then A1008: q2 -' 1 = a2 by A998, NAT_D:34;
A1009: a1 = p1 by A940, A941, A1001, A1002, A1007, GOBOARD1:5;
right_cell (f,(m -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),a1,a2) by A440, A654, A949, A955, A956, A999, A1000, A1001, A1002, A1007, GOBRD13:22
.= left_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A998, A1009, A1008, GOBRD13:25 ;
hence C meets LeftComp (Rev g) by A440, A654, A955, A956, A963; :: thesis:

end;

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

A1011: m -' 1 <= m by A955, NAT_1:11;
A1012: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A710, A700, A566, A956
.= (F . m) /. (m -' 1) by A566, A956, A1011 ;
A1013: 2 in dom g by A703, FINSEQ_3:25;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A931, FINSEQ_5:def 3;
then A1014: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A1013, FINSEQ_5:66
.= f /. (m + 1) by A933, A1013, FINSEQ_5:27 ;
A1015: L~ (Rev g) c= L~ f by A898, SPPOL_2:22;
A1016: (F . k) | (m + 1) = F . (m + 1) by A565, A710, A659;
A1017: (m -' 1) + 1 <= len (F . m) by A177, A955;
A1018: a2 = p2 by A940, A941, A1001, A1002, A1010, GOBOARD1:5;
A1019: (Rev g) /. 1 = g /. 1 by A651, A738, A702, FINSEQ_5:65
.= (Rev g) /. (len g) by FINSEQ_5:65
.= (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));
A1020: p1 < p1 + 1 by XREAL_1:29;
A1021: f /. ((m -' 1) + 1) = (F . m) /. m by A710, A652, A654, A566, A955;
A1022: (a2 -' 1) + 1 = a2 by A1004, XREAL_1:235;
A1023: a1 + 1 = p1 by A940, A941, A1001, A1002, A1010, GOBOARD1:5;
then A1024: 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 A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A998, GOBRD13:25
.= front_right_cell ((F . m),(m -' 1),(Gauge (C,n))) by A440, A949, A955, A956, A940, A941, A999, A1000, A1023, A1018, A1017, A1012, A1021, GOBRD13:37 ;
then F . (m + 1) turns_right m -' 1, Gauge (C,n) by A514, A901, A963;
then A1025: f turns_right m -' 1, Gauge (C,n) by A956, A933, A1016, GOBRD13:43;
A1026: a1 < a1 + 1 by XREAL_1:29;
then A1027: [p1,(p2 -' 1)] in Indices (Gauge (C,n)) by A949, A955, A940, A941, A999, A1000, A1023, A1020, A1025, GOBRD13:def 6;
then A1028: 1 <= a2 -' 1 by A1018, MATRIX_0:32;
f /. (m + 1) = (Gauge (C,n)) * (p1,(p2 -' 1)) by A949, A955, A933, A940, A941, A999, A1000, A1023, A1026, A1020, A1025, GOBRD13:def 6;
then left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),a1,(a2 -' 1)) by A939, A938, A952, A940, A941, A1018, A1027, A1024, A1014, A1022, A1019, GOBRD13:21;
then f /. (m -' 1) in left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) by A947, A1000, A1006, A1005, A1023, A1022, A1028, JORDAN9:20;
then A1029: f /. (m -' 1) in (left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g)) by A959, XBOOLE_0:def 5;
A1030: 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 A939, A938, A952, JORDAN9:27;
hence C meets LeftComp (Rev g) by A654, A660, A955, A956, A959, A1029, A1015, A1030; :: thesis:

end;

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

then A1032: a2 = q2 by A940, A941, A998, A1001, A1002, GOBOARD1:5;
A1033: a1 = q1 by A940, A941, A998, A1001, A1002, A1031, GOBOARD1:5;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A566, A956, NAT_1:11
.= (Rev g) /. 2 by A710, A700, A566, A956, A943, A1000, A1033, A1032
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A566, A961, A962, A951
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A177 ;
hence C meets LeftComp (Rev g) by A648, A961, A962, A958, A936; :: thesis:

end;

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

then A1035: a2 = p2 + 1 by A940, A941, A1001, A1002, GOBOARD1:5;
A1036: a1 = p1 by A940, A941, A1001, A1002, A1034, GOBOARD1:5;
right_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) = cell ((Gauge (C,n)),p1,p2) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A998, GOBRD13:26
.= left_cell (f,(m -' 1),(Gauge (C,n))) by A651, A653, A654, A702, A955, A956, A940, A941, A999, A1000, A1036, A1035, FINSEQ_5:65, GOBRD13:27 ;
hence C meets LeftComp (Rev g) by A440, A710, A960, A962, A957; :: thesis:

end;

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

consider a1, a2, p91, p92 being Nat such that
A1038: [a1,a2] in Indices (Gauge (C,n)) and
A1039: f /. (m -' 1) = (Gauge (C,n)) * (a1,a2) and
A1040: [p91,p92] in Indices (Gauge (C,n)) and
A1041: (Rev g) /. 1 = (Gauge (C,n)) * (p91,p92) and
A1042: ( ( a1 = p91 & a2 + 1 = p92 ) or ( a1 + 1 = p91 & a2 = p92 ) or ( a1 = p91 + 1 & a2 = p92 ) or ( a1 = p91 & a2 = p92 + 1 ) ) by A653, A654, A949, A955, A956, JORDAN8:3;
A1043: a1 <= len (Gauge (C,n)) by A1038, MATRIX_0:32;
thus C meets LeftComp (Rev g) :: thesis:

proof

per cases by A1042;

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

then a2 + 1 = p2 by A940, A941, A1040, A1041, GOBOARD1:5;
then A1045: q2 -' 1 = a2 by A1037, NAT_D:34;
a1 = p1 by A940, A941, A1040, A1041, A1044, GOBOARD1:5;
then A1046: q1 = a1 -' 1 by A1037, NAT_D:34;
right_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) = cell ((Gauge (C,n)),q1,(q2 -' 1)) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A1037, GOBRD13:24
.= left_cell (f,(m -' 1),(Gauge (C,n))) by A440, A654, A949, A955, A956, A1038, A1039, A1040, A1041, A1044, A1046, A1045, GOBRD13:21 ;
hence C meets LeftComp (Rev g) by A440, A710, A960, A962, A957; :: thesis:

end;

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

then A1048: a2 = p2 by A940, A941, A1040, A1041, GOBOARD1:5;
A1049: a1 + 1 = p1 by A940, A941, A1040, A1041, A1047, GOBOARD1:5;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A566, A956, NAT_1:11
.= (Rev g) /. 2 by A710, A700, A566, A956, A943, A1037, A1039, A1049, A1048
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A566, A961, A962, A951
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A177 ;
hence C meets LeftComp (Rev g) by A648, A961, A962, A958, A936; :: thesis:

end;

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

A1051: m -' 1 <= m by A955, NAT_1:11;
A1052: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A710, A700, A566, A956
.= (F . m) /. (m -' 1) by A566, A956, A1051 ;
A1053: 2 in dom g by A703, FINSEQ_3:25;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A931, FINSEQ_5:def 3;
then A1054: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A1053, FINSEQ_5:66
.= f /. (m + 1) by A933, A1053, FINSEQ_5:27 ;
A1055: L~ (Rev g) c= L~ f by A898, SPPOL_2:22;
set rc = (left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g));
A1056: LeftComp (Rev g) is_a_component_of (L~ (Rev g)) ` by GOBOARD9:def 1;
A1057: p1 -' 1 = q1 by A1037, NAT_D:34;
A1058: (F . k) | (m + 1) = F . (m + 1) by A565, A710, A659;
A1059: a1 = p1 + 1 by A940, A941, A1040, A1041, A1050, GOBOARD1:5;
A1060: f /. ((m -' 1) + 1) = (F . m) /. m by A710, A652, A654, A566, A955;
A1061: (m -' 1) + 1 <= len (F . m) by A177, A955;
A1062: a2 = p2 by A940, A941, A1040, A1041, A1050, GOBOARD1:5;
left_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) = cell ((Gauge (C,n)),q1,q2) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A1037, GOBRD13:23
.= front_right_cell ((F . m),(m -' 1),(Gauge (C,n))) by A440, A949, A955, A956, A940, A941, A1037, A1038, A1039, A1059, A1062, A1057, A1061, A1052, A1060, GOBRD13:39 ;
then F . (m + 1) turns_right m -' 1, Gauge (C,n) by A514, A901, A963;
then A1063: f turns_right m -' 1, Gauge (C,n) by A956, A933, A1058, GOBRD13:43;
p1 + 1 > p1 by XREAL_1:29;
then A1064: a1 + 1 > p1 by A1059, NAT_1:13;
then A1065: [p1,(p2 + 1)] in Indices (Gauge (C,n)) by A949, A955, A940, A941, A1038, A1039, A1062, A1063, GOBRD13:def 6;
then A1066: p2 + 1 <= width (Gauge (C,n)) by MATRIX_0:32;
a2 + 1 > p2 by A1062, NAT_1:13;
then A1067: f /. (m + 1) = (Gauge (C,n)) * (p1,(p2 + 1)) by A949, A955, A933, A940, A941, A1038, A1039, A1062, A1064, A1063, GOBRD13:def 6;
(Rev g) /. 1 = g /. 1 by A651, A738, A702, FINSEQ_5:65
.= (Rev g) /. (len g) by FINSEQ_5:65
.= (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 A939, A938, A952, A940, A941, A1067, A1065, A1054, GOBRD13:27;
then f /. (m -' 1) in left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) by A945, A948, A1039, A1043, A1059, A1062, A1066, JORDAN9:20;
then A1068: f /. (m -' 1) in (left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g)) by A959, XBOOLE_0:def 5;
(left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g)) c= LeftComp (Rev g) by A939, A938, A952, JORDAN9:27;
hence C meets LeftComp (Rev g) by A654, A660, A955, A956, A959, A1068, A1055, A1056; :: thesis:

end;

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

then a1 = p1 by A940, A941, A1040, A1041, GOBOARD1:5;
then A1070: q1 = a1 -' 1 by A1037, NAT_D:34;
a2 = p2 + 1 by A940, A941, A1040, A1041, A1069, GOBOARD1:5;
then right_cell (f,(m -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),q1,q2) by A651, A653, A654, A702, A955, A956, A1037, A1038, A1039, A1040, A1041, A1069, A1070, FINSEQ_5:65, GOBRD13:28
.= left_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A1037, GOBRD13:23 ;
hence C meets LeftComp (Rev g) by A440, A654, A955, A956, A963; :: thesis:

end;

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

consider a1, a2, p91, p92 being Nat such that
A1072: [a1,a2] in Indices (Gauge (C,n)) and
A1073: f /. (m -' 1) = (Gauge (C,n)) * (a1,a2) and
A1074: [p91,p92] in Indices (Gauge (C,n)) and
A1075: (Rev g) /. 1 = (Gauge (C,n)) * (p91,p92) and
A1076: ( ( a1 = p91 & a2 + 1 = p92 ) or ( a1 + 1 = p91 & a2 = p92 ) or ( a1 = p91 + 1 & a2 = p92 ) or ( a1 = p91 & a2 = p92 + 1 ) ) by A653, A654, A949, A955, A956, JORDAN8:3;
A1077: a2 <= width (Gauge (C,n)) by A1072, MATRIX_0:32;
thus C meets LeftComp (Rev g) :: thesis:

proof

per cases by A1076;

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

then A1079: a2 + 1 = p2 by A940, A941, A1074, A1075, GOBOARD1:5;
A1080: a1 = p1 by A940, A941, A1074, A1075, A1078, GOBOARD1:5;
(F . ((m -' 1) + ((len g) -' 1))) /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A566, A956, NAT_1:11
.= (Rev g) /. 2 by A710, A700, A566, A956, A943, A1071, A1073, A1080, A1079
.= (F . ((m -' 1) + ((len g) -' 1))) /. ((m -' 1) + ((len g) -' 1)) by A566, A961, A962, A951
.= (F . ((m -' 1) + ((len g) -' 1))) /. (len (F . ((m -' 1) + ((len g) -' 1)))) by A177 ;
hence C meets LeftComp (Rev g) by A648, A961, A962, A958, A936; :: thesis:

end;

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

then a2 = p2 by A940, A941, A1074, A1075, GOBOARD1:5;
then A1082: a2 -' 1 = q2 by A1071, NAT_D:34;
a1 + 1 = p1 by A940, A941, A1074, A1075, A1081, GOBOARD1:5;
then A1083: a1 = q1 -' 1 by A1071, NAT_D:34;
right_cell (f,(m -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),a1,(a2 -' 1)) by A440, A654, A949, A955, A956, A1072, A1073, A1074, A1075, A1081, GOBRD13:24
.= left_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A1071, A1083, A1082, GOBRD13:21 ;
hence C meets LeftComp (Rev g) by A440, A654, A955, A956, A963; :: thesis:

end;

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

then a2 = p2 by A940, A941, A1074, A1075, GOBOARD1:5;
then A1085: a2 -' 1 = q2 by A1071, NAT_D:34;
A1086: a1 = p1 + 1 by A940, A941, A1074, A1075, A1084, GOBOARD1:5;
right_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) = cell ((Gauge (C,n)),q1,q2) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A1071, GOBRD13:22
.= left_cell (f,(m -' 1),(Gauge (C,n))) by A651, A653, A654, A702, A955, A956, A1071, A1072, A1073, A1074, A1075, A1084, A1086, A1085, FINSEQ_5:65, GOBRD13:25 ;
hence C meets LeftComp (Rev g) by A440, A710, A960, A962, A957; :: thesis:

end;

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

then A1088: a2 = p2 + 1 by A940, A941, A1074, A1075, GOBOARD1:5;
A1089: f /. ((m -' 1) + 1) = (F . m) /. m by A710, A652, A654, A566, A955;
A1090: 2 in dom g by A703, FINSEQ_3:25;
((len (Rev g)) -' 1) + 2 = (len g) + 1 by A931, FINSEQ_5:def 3;
then A1091: (Rev g) /. ((len (Rev g)) -' 1) = g /. 2 by A1090, FINSEQ_5:66
.= f /. (m + 1) by A933, A1090, FINSEQ_5:27 ;
A1092: (p1 -' 1) + 1 = p1 by A945, XREAL_1:235;
A1093: m -' 1 <= m by A955, NAT_1:11;
A1094: f /. (m -' 1) = (F . (m -' 1)) /. (m -' 1) by A710, A700, A566, A956
.= (F . m) /. (m -' 1) by A566, A956, A1093 ;
A1095: p2 -' 1 = q2 by A1071, NAT_D:34;
set rc = (left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g));
A1096: p2 + 1 > p2 by NAT_1:13;
A1097: (Rev g) /. 1 = g /. 1 by A651, A738, A702, FINSEQ_5:65
.= (Rev g) /. (len g) by FINSEQ_5:65
.= (Rev g) /. (len (Rev g)) by FINSEQ_5:def 3 ;
A1098: (m -' 1) + 1 <= len (F . m) by A177, A955;
A1099: (F . k) | (m + 1) = F . (m + 1) by A565, A710, A659;
A1100: L~ (Rev g) c= L~ f by A898, SPPOL_2:22;
A1101: a1 = p1 by A940, A941, A1074, A1075, A1087, GOBOARD1:5;
left_cell (f,((m -' 1) + ((len g) -' 1)),(Gauge (C,n))) = cell ((Gauge (C,n)),(q1 -' 1),q2) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A1071, GOBRD13:21
.= front_right_cell ((F . m),(m -' 1),(Gauge (C,n))) by A440, A949, A955, A956, A940, A941, A1071, A1072, A1073, A1101, A1088, A1095, A1098, A1094, A1089, GOBRD13:41 ;
then F . (m + 1) turns_right m -' 1, Gauge (C,n) by A514, A901, A963;
then A1102: f turns_right m -' 1, Gauge (C,n) by A956, A933, A1099, GOBRD13:43;
A1103: a2 + 1 > p2 + 1 by A1088, NAT_1:13;
then A1104: [(p1 -' 1),p2] in Indices (Gauge (C,n)) by A949, A955, A940, A941, A1072, A1073, A1096, A1102, GOBRD13:def 6;
then A1105: 1 <= p1 -' 1 by MATRIX_0:32;
f /. (m + 1) = (Gauge (C,n)) * ((p1 -' 1),p2) by A949, A955, A933, A940, A941, A1072, A1073, A1103, A1096, A1102, GOBRD13:def 6;
then left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(p1 -' 1),p2) by A939, A938, A952, A940, A941, A1104, A1091, A1097, A1092, GOBRD13:23;
then f /. (m -' 1) in left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n))) by A947, A948, A1073, A1077, A1101, A1088, A1105, A1092, JORDAN9:20;
then A1106: f /. (m -' 1) in (left_cell ((Rev g),((len (Rev g)) -' 1),(Gauge (C,n)))) \ (L~ (Rev g)) by A959, XBOOLE_0:def 5;
A1107: 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 A939, A938, A952, JORDAN9:27;
hence C meets LeftComp (Rev g) by A654, A660, A955, A956, A959, A1106, A1100, A1107; :: thesis:

end;

then C meets RightComp g by GOBOARD9:23;
hence contradiction by A876, A885, A899, A887, JORDAN9:1, SPRECT_4:6; :: thesis:

end;

then A1108: g = f /^ 0 by XREAL_1:232
.= f by FINSEQ_5:28 ;
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 A1109: (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) = (F . 1) /. 1 by FINSEQ_4:16
.= f /. 1 by A647, A566 ;
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 A1110: (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) = (F . 2) /. 2 by FINSEQ_4:17
.= f /. 2 by A657, A566 ;
A1111: 2 < X-SpanStart (C,n) by JORDAN1H:49;
f is clockwise_oriented

proof

LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
then C c= LeftComp f by A876, A887, A1108, GOBOARD9:4;
then RightComp f misses C by GOBRD14:14, XBOOLE_1:63;
then A1112: RightComp f c= C ` by SUBSET_1:23;
UBD (L~ f) is_outside_component_of L~ f by JORDAN2C:68;
then UBD (L~ f) is_a_component_of (L~ f) ` by JORDAN2C:def 3;
then A1113: ( UBD (L~ f) = RightComp f or UBD (L~ f) = LeftComp f ) by JORDAN1H:24;
A1114: ((X-SpanStart (C,n)) -' 1) + 1 = X-SpanStart (C,n) by A1111, XREAL_1:235, 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:16;
A1116: BDD C = union { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } by JORDAN2C:def 4;
A1117: Int (right_cell (f,1,(Gauge (C,n)))) <> {} by A653, A656, JORDAN9:9;
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, A440, A656, A1109, A1110, A1114, A1118, GOBRD13:26;
then A1119: Int (right_cell (f,1,(Gauge (C,n)))) c= BDD C by A1115;
Int (right_cell (f,1,(Gauge (C,n)))) c= RightComp f by A653, A656, JORDAN1H:25;
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:80;
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 2;
B is_a_component_of C ` by A1123, JORDAN2C:def 2;
then RightComp f is bounded by A1121, A1122, A1112, A1124, GOBOARD9:4, RLTOPSP1:42;
hence f is clockwise_oriented by A1113, JORDAN1H:39, JORDAN1H:41; :: 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 A440; :: thesis:
thus f /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) by A1109; :: thesis:
thus f /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A1110; :: thesis:
let m be Nat; :: thesis:
assume that
A1125: 1 <= m and
A1126: m + 2 <= len f ; :: thesis:
A1127: F . ((m + 1) + 1) = f | ((m + 1) + 1) by A565, A710, A1126;
A1128: m + 1 < m + 2 by XREAL_1:6;
then A1129: f | (m + 1) = F . (m + 1) by A565, A710, 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 A653, A1125, A1129, GOBRD13:42;
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 A653, A1125, A1130, A1129, GOBRD13:42;

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 A514, A1133, A1132, A1131, A1134, A1135, A1136;
hence f turns_left m, Gauge (C,n) by A1125, A1126, A1127, GOBRD13:44; :: 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 A514, A1133, A1132, A1131, A1134, A1137, A1138;
hence f goes_straight m, Gauge (C,n) by A1125, A1126, A1127, GOBRD13:45; :: 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 A514, A1133, A1132, A1131;
hence f turns_right m, Gauge (C,n) by A1125, A1126, A1127, GOBRD13:43; :: thesis: