jordan13.miz



    begin

    reserve i,j,k,l,m,n,i1,i2,j1,j2 for Nat;

    definition

      let C be non vertical non horizontal non empty being_simple_closed_curve Subset of ( TOP-REAL 2), n be Nat;

      assume

       A1: n is_sufficiently_large_for C;

      :: JORDAN13:def1

      func Span (C,n) -> clockwise_oriented standard non constant special_circular_sequence means it is_sequence_on ( Gauge (C,n)) & (it /. 1) = (( Gauge (C,n)) * (( X-SpanStart (C,n)),( Y-SpanStart (C,n)))) & (it /. 2) = (( Gauge (C,n)) * ((( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n)))) & for k be Nat st 1 <= k & (k + 2) <= ( len it ) holds (( front_right_cell (it ,k,( Gauge (C,n)))) misses C & ( front_left_cell (it ,k,( Gauge (C,n)))) misses C implies it turns_left (k,( Gauge (C,n)))) & (( front_right_cell (it ,k,( Gauge (C,n)))) misses C & ( front_left_cell (it ,k,( Gauge (C,n)))) meets C implies it goes_straight (k,( Gauge (C,n)))) & (( front_right_cell (it ,k,( Gauge (C,n)))) meets C implies it turns_right (k,( Gauge (C,n))));

      existence

      proof

        set XS = ( X-SpanStart (C,n)), YS = ( Y-SpanStart (C,n));

        set G = ( Gauge (C,n));

        

         A2: ( len G) = ((2 |^ n) + 3) by JORDAN8:def 1;

        defpred P[ Nat, set, set] means ($1 = 0 implies $3 = <*(G * (( X-SpanStart (C,n)),( Y-SpanStart (C,n))))*>) & ($1 = 1 implies $3 = <*(G * (( X-SpanStart (C,n)),( Y-SpanStart (C,n)))), (G * ((( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n))))*>) & ($1 > 1 & $2 is FinSequence of ( TOP-REAL 2) implies for f be FinSequence of ( TOP-REAL 2) st $2 = f holds (( len f) = $1 implies (f is_sequence_on G & ( left_cell (f,(( len f) -' 1),G)) meets C implies (( front_right_cell (f,(( len f) -' 1),G)) misses C & ( front_left_cell (f,(( len f) -' 1),G)) misses C implies ex i, j st (f ^ <*(G * (i,j))*>) turns_left ((( len f) -' 1),G) & $3 = (f ^ <*(G * (i,j))*>)) & (( front_right_cell (f,(( len f) -' 1),G)) misses C & ( front_left_cell (f,(( len f) -' 1),G)) meets C implies ex i, j st (f ^ <*(G * (i,j))*>) goes_straight ((( len f) -' 1),G) & $3 = (f ^ <*(G * (i,j))*>)) & (( front_right_cell (f,(( len f) -' 1),G)) meets C implies ex i, j st (f ^ <*(G * (i,j))*>) turns_right ((( len f) -' 1),G) & $3 = (f ^ <*(G * (i,j))*>))) & ( not f is_sequence_on G or ( left_cell (f,(( len f) -' 1),G)) misses C implies $3 = (f ^ <*(G * (1,1))*>))) & (( len f) <> $1 implies $3 = {} )) & ($1 > 1 & not $2 is FinSequence of ( TOP-REAL 2) implies $3 = {} );

        

         A3: (1 + 1) <= XS by JORDAN1H: 49;

        

         A4: the TopStruct of ( TOP-REAL 2) = ( TopSpaceMetr ( Euclid 2)) by EUCLID:def 8;

        

         A5: [( X-SpanStart (C,n)), ( Y-SpanStart (C,n))] in ( Indices G) by A1, JORDAN11: 8;

        

         A6: ( len G) = ( width G) by JORDAN8:def 1;

        

         A7: for k be Nat, x be set holds ex y be set st P[k, x, y]

        proof

          let k be Nat, x be set;

          per cases by NAT_1: 25;

            suppose

             A8: k = 0 ;

            take <*(G * (( X-SpanStart (C,n)),( Y-SpanStart (C,n))))*>;

            thus thesis by A8;

          end;

            suppose

             A9: k = 1;

            take <*(G * (( X-SpanStart (C,n)),( Y-SpanStart (C,n)))), (G * ((( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n))))*>;

            thus thesis by A9;

          end;

            suppose that

             A10: k > 1 and

             A11: x is FinSequence of ( TOP-REAL 2);

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

            thus thesis

            proof

              per cases ;

                suppose

                 A12: ( len f) = k;

                thus thesis

                proof

                  per cases ;

                    suppose

                     A13: f is_sequence_on G & ( left_cell (f,(( len f) -' 1),G)) meets C;

                    

                     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 be Nat such that

                     A18: [i1, j1] in ( Indices G) and

                     A19: (f /. (( len f) -' 1)) = (G * (i1,j1)) and

                     A20: [i2, j2] in ( Indices G) and

                     A21: (f /. ((( len f) -' 1) + 1)) = (G * (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 G) by A18, MATRIX_0: 32;

                    

                     A24: 1 <= (j2 + 1) by NAT_1: 12;

                    

                     A25: 1 <= i2 by A20, MATRIX_0: 32;

                    

                     A26: j1 <= ( width G) 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 G) by A20, MATRIX_0: 32;

                    then

                     A31: (j2 -' 1) <= ( width G) by NAT_D: 44;

                    

                     A32: i2 <= ( len G) by A20, MATRIX_0: 32;

                    then

                     A33: (i2 -' 1) <= ( len G) by NAT_D: 44;

                    thus thesis

                    proof

                      per cases ;

                        suppose

                         A34: ( front_right_cell (f,(( len f) -' 1),G)) misses C & ( front_left_cell (f,(( len f) -' 1),G)) misses C;

                        thus thesis

                        proof

                          per cases by A22;

                            suppose

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

                            take f1 = (f ^ <*(G * ((i2 -' 1),j2))*>);

                            now

                              take i = (i2 -' 1), j = j2;

                              now

                                 A36:

                                now

                                  assume (i2 -' 1) < 1;

                                  then i2 <= 1 by NAT_1: 14, NAT_D: 36;

                                  then i2 = 1 by A25, XXREAL_0: 1;

                                  then ( cell (G,(1 -' 1),j1)) meets C by A13, A17, A14, A18, A19, A20, A21, A35, GOBRD13: 21;

                                  then ( cell (G, 0 ,j1)) meets C by XREAL_1: 232;

                                  hence contradiction by A6, A26, JORDAN8: 18;

                                end;

                                let i19,j19,i29,j29 be Nat;

                                assume that

                                 A37: [i19, j19] in ( Indices G) and

                                 A38: [i29, j29] in ( Indices G) and

                                 A39: (f1 /. (( len f) -' 1)) = (G * (i19,j19)) and

                                 A40: (f1 /. ((( len f) -' 1) + 1)) = (G * (i29,j29));

                                

                                 A41: (f /. (( len f) -' 1)) = (G * (i19,j19)) by A29, A39, FINSEQ_4: 68;

                                

                                 A42: (f /. ((( len f) -' 1) + 1)) = (G * (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 G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 -' 1),j29)) or (i19 + 1) = i29 & j19 = j29 & [i29, (j29 + 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 + 1))) or i19 = (i29 + 1) & j19 = j29 & [i29, (j29 -' 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 -' 1))) or i19 = i29 & j19 = (j29 + 1) & [(i29 + 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 + 1),j29)) by A18, A19, A28, A30, A33, A15, A35, A37, A41, A43, A36, FINSEQ_4: 67, GOBOARD1: 5, MATRIX_0: 30;

                              end;

                              hence f1 turns_left ((( len f) -' 1),G) by GOBRD13:def 7;

                              thus f1 = (f ^ <*(G * (i,j))*>);

                            end;

                            hence thesis by A10, A12, A13, A34;

                          end;

                            suppose

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

                            take f1 = (f ^ <*(G * (i2,(j2 + 1)))*>);

                            now

                              take i = i2, j = (j2 + 1);

                              now

                                 A45:

                                now

                                  assume (j2 + 1) > ( len G);

                                  then

                                   A46: (( len G) + 1) <= (j2 + 1) by NAT_1: 13;

                                  (j2 + 1) <= (( len G) + 1) by A6, A30, XREAL_1: 6;

                                  then (j2 + 1) = (( len G) + 1) by A46, XXREAL_0: 1;

                                  then ( cell (G,i1,( len G))) meets C by A13, A17, A14, A18, A19, A20, A21, A44, GOBRD13: 23;

                                  hence contradiction by A23, JORDAN8: 15;

                                end;

                                let i19,j19,i29,j29 be Nat;

                                assume that

                                 A47: [i19, j19] in ( Indices G) and

                                 A48: [i29, j29] in ( Indices G) and

                                 A49: (f1 /. (( len f) -' 1)) = (G * (i19,j19)) and

                                 A50: (f1 /. ((( len f) -' 1) + 1)) = (G * (i29,j29));

                                

                                 A51: (f /. (( len f) -' 1)) = (G * (i19,j19)) by A29, A49, FINSEQ_4: 68;

                                

                                 A52: (f /. ((( len f) -' 1) + 1)) = (G * (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 G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 -' 1),j29)) or (i19 + 1) = i29 & j19 = j29 & [i29, (j29 + 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 + 1))) or i19 = (i29 + 1) & j19 = j29 & [i29, (j29 -' 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 -' 1))) or i19 = i29 & j19 = (j29 + 1) & [(i29 + 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 + 1),j29)) by A6, A18, A19, A25, A32, A24, A15, A44, A47, A51, A53, A45, FINSEQ_4: 67, GOBOARD1: 5, MATRIX_0: 30;

                              end;

                              hence f1 turns_left ((( len f) -' 1),G) by GOBRD13:def 7;

                              thus f1 = (f ^ <*(G * (i,j))*>);

                            end;

                            hence thesis by A10, A12, A13, A34;

                          end;

                            suppose

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

                            take f1 = (f ^ <*(G * (i2,(j2 -' 1)))*>);

                            now

                              take i = i2, j = (j2 -' 1);

                              now

                                 A55:

                                now

                                  assume (j2 -' 1) < 1;

                                  then j2 <= 1 by NAT_1: 14, NAT_D: 36;

                                  then j2 = 1 by A28, XXREAL_0: 1;

                                  then ( cell (G,i2,(1 -' 1))) meets C by A13, A17, A14, A18, A19, A20, A21, A54, GOBRD13: 25;

                                  then ( cell (G,i2, 0 )) meets C by XREAL_1: 232;

                                  hence contradiction by A32, JORDAN8: 17;

                                end;

                                let i19,j19,i29,j29 be Nat;

                                assume that

                                 A56: [i19, j19] in ( Indices G) and

                                 A57: [i29, j29] in ( Indices G) and

                                 A58: (f1 /. (( len f) -' 1)) = (G * (i19,j19)) and

                                 A59: (f1 /. ((( len f) -' 1) + 1)) = (G * (i29,j29));

                                

                                 A60: (f /. (( len f) -' 1)) = (G * (i19,j19)) by A29, A58, FINSEQ_4: 68;

                                

                                 A61: (f /. ((( len f) -' 1) + 1)) = (G * (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 G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 -' 1),j29)) or (i19 + 1) = i29 & j19 = j29 & [i29, (j29 + 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 + 1))) or i19 = (i29 + 1) & j19 = j29 & [i29, (j29 -' 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 -' 1))) or i19 = i29 & j19 = (j29 + 1) & [(i29 + 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 + 1),j29)) by A18, A19, A25, A32, A31, A15, A54, A56, A60, A62, A55, FINSEQ_4: 67, GOBOARD1: 5, MATRIX_0: 30;

                              end;

                              hence f1 turns_left ((( len f) -' 1),G) by GOBRD13:def 7;

                              thus f1 = (f ^ <*(G * (i,j))*>);

                            end;

                            hence thesis by A10, A12, A13, A34;

                          end;

                            suppose

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

                            take f1 = (f ^ <*(G * ((i2 + 1),j2))*>);

                            now

                              take i = (i2 + 1), j = j2;

                              now

                                 A64:

                                now

                                  assume (i2 + 1) > ( len G);

                                  then

                                   A65: (( len G) + 1) <= (i2 + 1) by NAT_1: 13;

                                  (i2 + 1) <= (( len G) + 1) by A32, XREAL_1: 6;

                                  then (i2 + 1) = (( len G) + 1) by A65, XXREAL_0: 1;

                                  then ( cell (G,( len G),j2)) meets C by A13, A17, A14, A18, A19, A20, A21, A63, GOBRD13: 27;

                                  hence contradiction by A6, A30, JORDAN8: 16;

                                end;

                                let i19,j19,i29,j29 be Nat;

                                assume that

                                 A66: [i19, j19] in ( Indices G) and

                                 A67: [i29, j29] in ( Indices G) and

                                 A68: (f1 /. (( len f) -' 1)) = (G * (i19,j19)) and

                                 A69: (f1 /. ((( len f) -' 1) + 1)) = (G * (i29,j29));

                                

                                 A70: (f /. (( len f) -' 1)) = (G * (i19,j19)) by A29, A68, FINSEQ_4: 68;

                                

                                 A71: (f /. ((( len f) -' 1) + 1)) = (G * (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 G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 -' 1),j29)) or (i19 + 1) = i29 & j19 = j29 & [i29, (j29 + 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 + 1))) or i19 = (i29 + 1) & j19 = j29 & [i29, (j29 -' 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 -' 1))) or i19 = i29 & j19 = (j29 + 1) & [(i29 + 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 + 1),j29)) by A18, A19, A28, A30, A27, A15, A63, A66, A70, A72, A64, FINSEQ_4: 67, GOBOARD1: 5, MATRIX_0: 30;

                              end;

                              hence f1 turns_left ((( len f) -' 1),G) by GOBRD13:def 7;

                              thus f1 = (f ^ <*(G * (i,j))*>);

                            end;

                            hence thesis by A10, A12, A13, A34;

                          end;

                        end;

                      end;

                        suppose

                         A73: ( front_right_cell (f,(( len f) -' 1),G)) misses C & ( front_left_cell (f,(( len f) -' 1),G)) meets C;

                        thus thesis

                        proof

                          per cases by A22;

                            suppose

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

                            take f1 = (f ^ <*(G * (i2,(j2 + 1)))*>);

                            now

                              take i = i2, j = (j2 + 1);

                              now

                                 A75:

                                now

                                  assume (j2 + 1) > ( len G);

                                  then

                                   A76: (( len G) + 1) <= (j2 + 1) by NAT_1: 13;

                                  (j2 + 1) <= (( len G) + 1) by A6, A30, XREAL_1: 6;

                                  then (j2 + 1) = (( len G) + 1) by A76, XXREAL_0: 1;

                                  then ( cell (G,(i1 -' 1),( len G))) meets C by A13, A17, A14, A18, A19, A20, A21, A73, A74, GOBRD13: 34;

                                  hence contradiction by A23, JORDAN8: 15, NAT_D: 44;

                                end;

                                let i19,j19,i29,j29 be Nat;

                                assume that

                                 A77: [i19, j19] in ( Indices G) and

                                 A78: [i29, j29] in ( Indices G) and

                                 A79: (f1 /. (( len f) -' 1)) = (G * (i19,j19)) and

                                 A80: (f1 /. ((( len f) -' 1) + 1)) = (G * (i29,j29));

                                

                                 A81: (f /. (( len f) -' 1)) = (G * (i19,j19)) by A29, A79, FINSEQ_4: 68;

                                

                                 A82: (f /. ((( len f) -' 1) + 1)) = (G * (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 G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 + 1))) or (i19 + 1) = i29 & j19 = j29 & [(i29 + 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 + 1),j29)) or i19 = (i29 + 1) & j19 = j29 & [(i29 -' 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 -' 1),j29)) or i19 = i29 & j19 = (j29 + 1) & [i29, (j29 -' 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 -' 1))) by A6, A18, A19, A25, A32, A24, A15, A74, A77, A81, A83, A75, FINSEQ_4: 67, GOBOARD1: 5, MATRIX_0: 30;

                              end;

                              hence f1 goes_straight ((( len f) -' 1),G) by GOBRD13:def 8;

                              thus f1 = (f ^ <*(G * (i,j))*>);

                            end;

                            hence thesis by A10, A12, A13, A73;

                          end;

                            suppose

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

                            take f1 = (f ^ <*(G * ((i2 + 1),j2))*>);

                            now

                              take i = (i2 + 1), j = j2;

                              now

                                 A85:

                                now

                                  assume (i2 + 1) > ( len G);

                                  then

                                   A86: (( len G) + 1) <= (i2 + 1) by NAT_1: 13;

                                  (i2 + 1) <= (( len G) + 1) by A32, XREAL_1: 6;

                                  then (i2 + 1) = (( len G) + 1) by A86, XXREAL_0: 1;

                                  then ( cell (G,( len G),j1)) meets C by A13, A17, A14, A18, A19, A20, A21, A73, A84, GOBRD13: 36;

                                  hence contradiction by A6, A26, JORDAN8: 16;

                                end;

                                let i19,j19,i29,j29 be Nat;

                                assume that

                                 A87: [i19, j19] in ( Indices G) and

                                 A88: [i29, j29] in ( Indices G) and

                                 A89: (f1 /. (( len f) -' 1)) = (G * (i19,j19)) and

                                 A90: (f1 /. ((( len f) -' 1) + 1)) = (G * (i29,j29));

                                

                                 A91: (f /. (( len f) -' 1)) = (G * (i19,j19)) by A29, A89, FINSEQ_4: 68;

                                

                                 A92: (f /. ((( len f) -' 1) + 1)) = (G * (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 G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 + 1))) or (i19 + 1) = i29 & j19 = j29 & [(i29 + 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 + 1),j29)) or i19 = (i29 + 1) & j19 = j29 & [(i29 -' 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 -' 1),j29)) or i19 = i29 & j19 = (j29 + 1) & [i29, (j29 -' 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 -' 1))) by A18, A19, A28, A30, A27, A15, A84, A87, A91, A93, A85, FINSEQ_4: 67, GOBOARD1: 5, MATRIX_0: 30;

                              end;

                              hence f1 goes_straight ((( len f) -' 1),G) by GOBRD13:def 8;

                              thus f1 = (f ^ <*(G * (i,j))*>);

                            end;

                            hence thesis by A10, A12, A13, A73;

                          end;

                            suppose

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

                            take f1 = (f ^ <*(G * ((i2 -' 1),j2))*>);

                            now

                              take i = (i2 -' 1), j = j2;

                              now

                                 A95:

                                now

                                  assume (i2 -' 1) < 1;

                                  then i2 <= 1 by NAT_1: 14, NAT_D: 36;

                                  then i2 = 1 by A25, XXREAL_0: 1;

                                  then ( cell (G,(1 -' 1),(j1 -' 1))) meets C by A13, A17, A14, A18, A19, A20, A21, A73, A94, GOBRD13: 38;

                                  then ( cell (G, 0 ,(j1 -' 1))) meets C by XREAL_1: 232;

                                  hence contradiction by A6, A26, JORDAN8: 18, NAT_D: 44;

                                end;

                                let i19,j19,i29,j29 be Nat;

                                assume that

                                 A96: [i19, j19] in ( Indices G) and

                                 A97: [i29, j29] in ( Indices G) and

                                 A98: (f1 /. (( len f) -' 1)) = (G * (i19,j19)) and

                                 A99: (f1 /. ((( len f) -' 1) + 1)) = (G * (i29,j29));

                                

                                 A100: (f /. (( len f) -' 1)) = (G * (i19,j19)) by A29, A98, FINSEQ_4: 68;

                                

                                 A101: (f /. ((( len f) -' 1) + 1)) = (G * (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 G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 + 1))) or (i19 + 1) = i29 & j19 = j29 & [(i29 + 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 + 1),j29)) or i19 = (i29 + 1) & j19 = j29 & [(i29 -' 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 -' 1),j29)) or i19 = i29 & j19 = (j29 + 1) & [i29, (j29 -' 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 -' 1))) by A18, A19, A28, A30, A33, A15, A94, A96, A100, A102, A95, FINSEQ_4: 67, GOBOARD1: 5, MATRIX_0: 30;

                              end;

                              hence f1 goes_straight ((( len f) -' 1),G) by GOBRD13:def 8;

                              thus f1 = (f ^ <*(G * (i,j))*>);

                            end;

                            hence thesis by A10, A12, A13, A73;

                          end;

                            suppose

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

                            take f1 = (f ^ <*(G * (i2,(j2 -' 1)))*>);

                            now

                              take i = i2, j = (j2 -' 1);

                              now

                                 A104:

                                now

                                  assume (j2 -' 1) < 1;

                                  then j2 <= 1 by NAT_1: 14, NAT_D: 36;

                                  then j2 = 1 by A28, XXREAL_0: 1;

                                  then ( cell (G,i1,(1 -' 1))) meets C by A13, A17, A14, A18, A19, A20, A21, A73, A103, GOBRD13: 40;

                                  then ( cell (G,i1, 0 )) meets C by XREAL_1: 232;

                                  hence contradiction by A23, JORDAN8: 17;

                                end;

                                let i19,j19,i29,j29 be Nat;

                                assume that

                                 A105: [i19, j19] in ( Indices G) and

                                 A106: [i29, j29] in ( Indices G) and

                                 A107: (f1 /. (( len f) -' 1)) = (G * (i19,j19)) and

                                 A108: (f1 /. ((( len f) -' 1) + 1)) = (G * (i29,j29));

                                

                                 A109: (f /. (( len f) -' 1)) = (G * (i19,j19)) by A29, A107, FINSEQ_4: 68;

                                

                                 A110: (f /. ((( len f) -' 1) + 1)) = (G * (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 G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 + 1))) or (i19 + 1) = i29 & j19 = j29 & [(i29 + 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 + 1),j29)) or i19 = (i29 + 1) & j19 = j29 & [(i29 -' 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 -' 1),j29)) or i19 = i29 & j19 = (j29 + 1) & [i29, (j29 -' 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 -' 1))) by A18, A19, A25, A32, A31, A15, A103, A105, A109, A111, A104, FINSEQ_4: 67, GOBOARD1: 5, MATRIX_0: 30;

                              end;

                              hence f1 goes_straight ((( len f) -' 1),G) by GOBRD13:def 8;

                              thus f1 = (f ^ <*(G * (i,j))*>);

                            end;

                            hence thesis by A10, A12, A13, A73;

                          end;

                        end;

                      end;

                        suppose

                         A112: ( front_right_cell (f,(( len f) -' 1),G)) meets C;

                        thus thesis

                        proof

                          per cases by A22;

                            suppose

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

                            take f1 = (f ^ <*(G * ((i2 + 1),j2))*>);

                            now

                              take i = (i2 + 1), j = j2;

                              now

                                 A114:

                                now

                                  assume (i2 + 1) > ( len G);

                                  then

                                   A115: (( len G) + 1) <= (i2 + 1) by NAT_1: 13;

                                  (i2 + 1) <= (( len G) + 1) by A32, XREAL_1: 6;

                                  then (i2 + 1) = (( len G) + 1) by A115, XXREAL_0: 1;

                                  then ( cell (G,( len G),j2)) meets C by A13, A17, A14, A18, A19, A20, A21, A112, A113, GOBRD13: 35;

                                  hence contradiction by A6, A30, JORDAN8: 16;

                                end;

                                let i19,j19,i29,j29 be Nat;

                                assume that

                                 A116: [i19, j19] in ( Indices G) and

                                 A117: [i29, j29] in ( Indices G) and

                                 A118: (f1 /. (( len f) -' 1)) = (G * (i19,j19)) and

                                 A119: (f1 /. ((( len f) -' 1) + 1)) = (G * (i29,j29));

                                

                                 A120: (f /. (( len f) -' 1)) = (G * (i19,j19)) by A29, A118, FINSEQ_4: 68;

                                

                                 A121: (f /. ((( len f) -' 1) + 1)) = (G * (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 G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 + 1),j29)) or (i19 + 1) = i29 & j19 = j29 & [i29, (j29 -' 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 -' 1))) or i19 = (i29 + 1) & j19 = j29 & [i29, (j29 + 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 + 1))) or i19 = i29 & j19 = (j29 + 1) & [(i29 -' 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 -' 1),j29)) by A18, A19, A28, A30, A27, A15, A113, A116, A120, A122, A114, FINSEQ_4: 67, GOBOARD1: 5, MATRIX_0: 30;

                              end;

                              hence f1 turns_right ((( len f) -' 1),G) by GOBRD13:def 6;

                              thus f1 = (f ^ <*(G * (i,j))*>);

                            end;

                            hence thesis by A10, A12, A13, A112;

                          end;

                            suppose

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

                            take f1 = (f ^ <*(G * (i2,(j2 -' 1)))*>);

                            now

                              take i = i2, j = (j2 -' 1);

                              now

                                 A124:

                                now

                                  assume (j2 -' 1) < 1;

                                  then j2 <= 1 by NAT_1: 14, NAT_D: 36;

                                  then j2 = 1 by A28, XXREAL_0: 1;

                                  then ( cell (G,i2,(1 -' 1))) meets C by A13, A17, A14, A18, A19, A20, A21, A112, A123, GOBRD13: 37;

                                  then ( cell (G,i2, 0 )) meets C by XREAL_1: 232;

                                  hence contradiction by A32, JORDAN8: 17;

                                end;

                                let i19,j19,i29,j29 be Nat;

                                assume that

                                 A125: [i19, j19] in ( Indices G) and

                                 A126: [i29, j29] in ( Indices G) and

                                 A127: (f1 /. (( len f) -' 1)) = (G * (i19,j19)) and

                                 A128: (f1 /. ((( len f) -' 1) + 1)) = (G * (i29,j29));

                                

                                 A129: (f /. (( len f) -' 1)) = (G * (i19,j19)) by A29, A127, FINSEQ_4: 68;

                                

                                 A130: (f /. ((( len f) -' 1) + 1)) = (G * (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 G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 + 1),j29)) or (i19 + 1) = i29 & j19 = j29 & [i29, (j29 -' 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 -' 1))) or i19 = (i29 + 1) & j19 = j29 & [i29, (j29 + 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 + 1))) or i19 = i29 & j19 = (j29 + 1) & [(i29 -' 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 -' 1),j29)) by A18, A19, A25, A32, A31, A15, A123, A125, A129, A131, A124, FINSEQ_4: 67, GOBOARD1: 5, MATRIX_0: 30;

                              end;

                              hence f1 turns_right ((( len f) -' 1),G) by GOBRD13:def 6;

                              thus f1 = (f ^ <*(G * (i,j))*>);

                            end;

                            hence thesis by A10, A12, A13, A112;

                          end;

                            suppose

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

                            take f1 = (f ^ <*(G * (i2,(j2 + 1)))*>);

                            now

                              take i = i2, j = (j2 + 1);

                              now

                                 A133:

                                now

                                  assume (j2 + 1) > ( len G);

                                  then

                                   A134: (( len G) + 1) <= (j2 + 1) by NAT_1: 13;

                                  (j2 + 1) <= (( len G) + 1) by A6, A30, XREAL_1: 6;

                                  then (j2 + 1) = (( len G) + 1) by A134, XXREAL_0: 1;

                                  then ( cell (G,(i2 -' 1),( len G))) meets C by A13, A17, A14, A18, A19, A20, A21, A112, A132, GOBRD13: 39;

                                  hence contradiction by A32, JORDAN8: 15, NAT_D: 44;

                                end;

                                let i19,j19,i29,j29 be Nat;

                                assume that

                                 A135: [i19, j19] in ( Indices G) and

                                 A136: [i29, j29] in ( Indices G) and

                                 A137: (f1 /. (( len f) -' 1)) = (G * (i19,j19)) and

                                 A138: (f1 /. ((( len f) -' 1) + 1)) = (G * (i29,j29));

                                

                                 A139: (f /. (( len f) -' 1)) = (G * (i19,j19)) by A29, A137, FINSEQ_4: 68;

                                

                                 A140: (f /. ((( len f) -' 1) + 1)) = (G * (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 G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 + 1),j29)) or (i19 + 1) = i29 & j19 = j29 & [i29, (j29 -' 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 -' 1))) or i19 = (i29 + 1) & j19 = j29 & [i29, (j29 + 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 + 1))) or i19 = i29 & j19 = (j29 + 1) & [(i29 -' 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 -' 1),j29)) by A6, A18, A19, A25, A32, A24, A15, A132, A135, A139, A141, A133, FINSEQ_4: 67, GOBOARD1: 5, MATRIX_0: 30;

                              end;

                              hence f1 turns_right ((( len f) -' 1),G) by GOBRD13:def 6;

                              thus f1 = (f ^ <*(G * (i,j))*>);

                            end;

                            hence thesis by A10, A12, A13, A112;

                          end;

                            suppose

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

                            take f1 = (f ^ <*(G * ((i2 -' 1),j2))*>);

                            now

                              take i = (i2 -' 1), j = j2;

                              now

                                 A143:

                                now

                                  assume (i2 -' 1) < 1;

                                  then i2 <= 1 by NAT_1: 14, NAT_D: 36;

                                  then i2 = 1 by A25, XXREAL_0: 1;

                                  then ( cell (G,(1 -' 1),(j2 -' 1))) meets C by A13, A17, A14, A18, A19, A20, A21, A112, A142, GOBRD13: 41;

                                  then ( cell (G, 0 ,(j2 -' 1))) meets C by XREAL_1: 232;

                                  hence contradiction by A6, A30, JORDAN8: 18, NAT_D: 44;

                                end;

                                let i19,j19,i29,j29 be Nat;

                                assume that

                                 A144: [i19, j19] in ( Indices G) and

                                 A145: [i29, j29] in ( Indices G) and

                                 A146: (f1 /. (( len f) -' 1)) = (G * (i19,j19)) and

                                 A147: (f1 /. ((( len f) -' 1) + 1)) = (G * (i29,j29));

                                

                                 A148: (f /. (( len f) -' 1)) = (G * (i19,j19)) by A29, A146, FINSEQ_4: 68;

                                

                                 A149: (f /. ((( len f) -' 1) + 1)) = (G * (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 G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 + 1),j29)) or (i19 + 1) = i29 & j19 = j29 & [i29, (j29 -' 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 -' 1))) or i19 = (i29 + 1) & j19 = j29 & [i29, (j29 + 1)] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * (i29,(j29 + 1))) or i19 = i29 & j19 = (j29 + 1) & [(i29 -' 1), j29] in ( Indices G) & (f1 /. ((( len f) -' 1) + 2)) = (G * ((i29 -' 1),j29)) by A18, A19, A28, A30, A33, A15, A142, A144, A148, A150, A143, FINSEQ_4: 67, GOBOARD1: 5, MATRIX_0: 30;

                              end;

                              hence f1 turns_right ((( len f) -' 1),G) by GOBRD13:def 6;

                              thus f1 = (f ^ <*(G * (i,j))*>);

                            end;

                            hence thesis by A10, A12, A13, A112;

                          end;

                        end;

                      end;

                    end;

                  end;

                    suppose

                     A151: not f is_sequence_on G or ( left_cell (f,(( len f) -' 1),G)) misses C;

                    take (f ^ <*(G * (1,1))*>);

                    thus thesis by A10, A12, A151;

                  end;

                end;

              end;

                suppose

                 A152: ( len f) <> k;

                take {} ;

                thus thesis by A10, A152;

              end;

            end;

          end;

            suppose

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

            take {} ;

            thus thesis by A153;

          end;

        end;

        consider F be Function such that

         A154: ( dom F) = NAT and

         A155: (F . 0 ) = {} and

         A156: for k be Nat holds P[k, (F . k), (F . (k + 1))] from RECDEF_1:sch 1( A7);

        defpred P[ Nat] means (F . $1) is FinSequence of ( TOP-REAL 2);

        

         A157: {} = ( <*> the carrier of ( TOP-REAL 2));

        

         A158: for k st P[k] holds P[(k + 1)]

        proof

          let k such that

           A159: (F . k) is FinSequence of ( TOP-REAL 2);

          per cases by NAT_1: 25;

            suppose k = 0 ;

            hence thesis by A156;

          end;

            suppose k = 1;

            hence thesis by A156;

          end;

            suppose

             A160: k > 1;

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

            per cases ;

              suppose

               A161: ( len f) = k;

              per cases ;

                suppose

                 A162: f is_sequence_on G & ( left_cell (f,(( len f) -' 1),G)) meets C;

                then

                 A163: ( front_right_cell (f,(( len f) -' 1),G)) meets C implies ex i, j st (f ^ <*(G * (i,j))*>) turns_right ((( len f) -' 1),G) & (F . (k + 1)) = (f ^ <*(G * (i,j))*>) by A156, A160, A161;

                

                 A164: ( front_right_cell (f,(( len f) -' 1),G)) misses C & ( front_left_cell (f,(( len f) -' 1),G)) meets C implies ex i, j st (f ^ <*(G * (i,j))*>) goes_straight ((( len f) -' 1),G) & (F . (k + 1)) = (f ^ <*(G * (i,j))*>) by A156, A160, A161, A162;

                ( front_right_cell (f,(( len f) -' 1),G)) misses C & ( front_left_cell (f,(( len f) -' 1),G)) misses C implies ex i, j st (f ^ <*(G * (i,j))*>) turns_left ((( len f) -' 1),G) & (F . (k + 1)) = (f ^ <*(G * (i,j))*>) by A156, A160, A161, A162;

                hence thesis by A164, A163;

              end;

                suppose

                 A165: not f is_sequence_on G or ( left_cell (f,(( len f) -' 1),G)) misses C;

                (f ^ <*(G * (1,1))*>) is FinSequence of ( TOP-REAL 2);

                hence thesis by A156, A160, A161, A165;

              end;

            end;

              suppose

               A166: ( len f) <> k;

              thus thesis by A156, A157, A160, A166;

            end;

          end;

        end;

        

         A167: P[ 0 ] by A155, A157;

        

         A168: for k holds P[k] from NAT_1:sch 2( A167, A158);

        ( rng F) c= (the carrier of ( TOP-REAL 2) * )

        proof

          let y be object;

          assume y in ( rng F);

          then ex x be 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 thesis by FINSEQ_1:def 11;

        end;

        then

        reconsider F as sequence of (the carrier of ( TOP-REAL 2) * ) by A154, FUNCT_2:def 1, RELSET_1: 4;

        defpred P[ Nat] means ( len (F . $1) qua FinSequence of ( TOP-REAL 2)) = $1;

        

         A169: for k st P[k] holds P[(k + 1)]

        proof

          let k such that

           A170: ( len (F . k)) = k;

          

           A171: P[k, (F . k), (F . (k + 1))] by A156;

          per cases by NAT_1: 25;

            suppose k = 0 ;

            hence thesis by A171, FINSEQ_1: 39;

          end;

            suppose k = 1;

            hence thesis by A171, FINSEQ_1: 44;

          end;

            suppose

             A172: k > 1;

            thus thesis

            proof

              per cases ;

                suppose

                 A173: (F . k) is_sequence_on G & ( left_cell ((F . k),(( len (F . k)) -' 1),G)) meets C;

                then

                 A174: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) meets C implies ex i, j st ((F . k) ^ <*(G * (i,j))*>) turns_right ((( len (F . k)) -' 1),G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A156, A170, A172;

                

                 A175: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C & ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) meets C implies ex i, j st ((F . k) ^ <*(G * (i,j))*>) goes_straight ((( len (F . k)) -' 1),G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A156, A170, A172, A173;

                ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C & ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) misses C implies ex i, j st ((F . k) ^ <*(G * (i,j))*>) turns_left ((( len (F . k)) -' 1),G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A156, A170, A172, A173;

                hence thesis by A170, A175, A174, FINSEQ_2: 16;

              end;

                suppose not (F . k) is_sequence_on G or ( left_cell ((F . k),(( len (F . k)) -' 1),G)) misses C;

                then (F . (k + 1)) = ((F . k) ^ <*(G * (1,1))*>) by A156, A170, A172;

                hence thesis by A170, FINSEQ_2: 16;

              end;

            end;

          end;

        end;

        defpred Q[ Nat] means (F . $1) is_sequence_on G & for m st 1 <= m & (m + 1) <= ( len (F . $1)) holds ( right_cell ((F . $1),m,G)) misses C & ( left_cell ((F . $1),m,G)) meets C;

        

         A176: P[ 0 ] by A155, CARD_1: 27;

        

         A177: for k holds P[k] from NAT_1:sch 2( A176, A169);

        

         A178: 1 <= XS by JORDAN1H: 49, XXREAL_0: 2;

        

         A179: for k st Q[k] holds Q[(k + 1)]

        proof

          let k such that

           A180: (F . k) is_sequence_on G and

           A181: for m st 1 <= m & (m + 1) <= ( len (F . k)) holds ( right_cell ((F . k),m,G)) misses C & ( left_cell ((F . k),m,G)) meets C;

          

           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 ;

            then

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

             A186:

            now

              let l;

              assume

               A187: l in ( dom (F . (k + 1)));

              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 st [i, j] in ( Indices G) & ((F . (k + 1)) /. l) = (G * (i,j)) by A5, A185, FINSEQ_4: 16;

            end;

            now

              let l;

              assume that

               A189: l in ( dom (F . (k + 1))) and

               A190: (l + 1) in ( dom (F . (k + 1)));

              

               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 st [i1, j1] in ( Indices G) & [i2, j2] in ( Indices G) & ((F . (k + 1)) /. l) = (G * (i1,j1)) & ((F . (k + 1)) /. (l + 1)) = (G * (i2,j2)) holds ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A183, A184, A190, FINSEQ_3: 25;

            end;

            hence (F . (k + 1)) is_sequence_on G by A186, GOBOARD1:def 9;

            let m;

            assume that

             A192: 1 <= m and

             A193: (m + 1) <= ( len (F . (k + 1)));

            1 <= (m + 1) by NAT_1: 12;

            then (m + 1) = ( 0 + 1) by A183, A184, A193, XXREAL_0: 1;

            hence thesis by A192;

          end;

            suppose

             A194: k = 1;

            

             A195: (XS -' 1) < XS by A178, JORDAN5B: 1;

            

             A196: XS <= (XS + 1) by NAT_1: 11;

            

             A197: [( X-SpanStart (C,n)), ( Y-SpanStart (C,n))] in ( Indices G) by A1, JORDAN11: 8;

            

             A198: (F . (k + 1)) = <*(G * (( X-SpanStart (C,n)),( Y-SpanStart (C,n)))), (G * ((( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n))))*> by A156, A194;

            then

             A199: ((F . (k + 1)) /. 1) = (G * (( X-SpanStart (C,n)),( Y-SpanStart (C,n)))) by FINSEQ_4: 17;

            

             A200: [(( X-SpanStart (C,n)) -' 1), ( Y-SpanStart (C,n))] in ( Indices G) by A1, JORDAN11: 9;

            

             A201: ((F . (k + 1)) /. 2) = (G * ((( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n)))) by A198, FINSEQ_4: 17;

             A202:

            now

              let l;

              assume that

               A203: l in ( dom (F . (k + 1))) and

               A204: (l + 1) in ( dom (F . (k + 1)));

              let i1,j1,i2,j2 be Nat such that

               A205: [i1, j1] in ( Indices G) and

               A206: [i2, j2] in ( Indices G) and

               A207: ((F . (k + 1)) /. l) = (G * (i1,j1)) and

               A208: ((F . (k + 1)) /. (l + 1)) = (G * (i2,j2));

              l <= 2 by A183, A194, A203, FINSEQ_3: 25;

              then

               A209: l = 0 or ... or l = 2;

              then

               A210: i2 = (XS -' 1) by A183, A194, A201, A200, A203, A204, A206, A208, FINSEQ_3: 25, GOBOARD1: 5;

              

               A211: j1 = YS by A199, A201, A197, A200, A203, A209, A205, A207, FINSEQ_3: 25, GOBOARD1: 5;

              j2 = YS 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 = XS 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;

            end;

            now

              let l;

              assume

               A213: l in ( dom (F . (k + 1)));

              then l <= 2 by A183, A194, FINSEQ_3: 25;

              then l = 0 or ... or l = 2;

              hence ex i, j st [i, j] in ( Indices G) & ((F . (k + 1)) /. l) = (G * (i,j)) by A199, A201, A197, A200, A213, FINSEQ_3: 25;

            end;

            hence

             A214: (F . (k + 1)) is_sequence_on G by A202, GOBOARD1:def 9;

            let m;

            assume that

             A215: 1 <= m and

             A216: (m + 1) <= ( len (F . (k + 1)));

            (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,G)) = ( cell (G,(XS -' 1),YS)) by A199, A201, A197, A200, A214, A216, A195, A196, GOBRD13:def 2;

            hence ( right_cell ((F . (k + 1)),m,G)) misses C by A1, JORDAN11: 11;

            ( left_cell ((F . (k + 1)),m,G)) = ( cell (G,(XS -' 1),(YS -' 1))) by A199, A201, A197, A200, A214, A216, A217, A195, A196, GOBRD13:def 3;

            hence thesis by A1, JORDAN11: 10;

          end;

            suppose

             A218: k > 1;

            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 be Nat such that

             A223: [i1, j1] in ( Indices G) and

             A224: ((F . k) /. (( len (F . k)) -' 1)) = (G * (i1,j1)) and

             A225: [i2, j2] in ( Indices G) and

             A226: ((F . k) /. ( len (F . k))) = (G * (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),G)) meets C & i1 = (i2 + 1) & j1 = j2 implies [(i2 -' 1), j2] in ( Indices G) 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),G)) meets C & (i1 + 1) = i2 & j1 = j2 implies [(i2 + 1), j2] in ( Indices G) 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),G)) meets C & i1 = i2 & (j1 + 1) = j2 implies [i1, (j2 + 1)] in ( Indices G) by A180, A182, A218, A223, A224, A225, A226, JORDAN1H: 56;

            

             A230: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) meets C & i1 = i2 & j1 = (j2 + 1) implies [(i2 -' 1), j2] in ( Indices G) 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),G)) meets C & i1 = (i2 + 1) & j1 = j2 implies [i2, (j2 + 1)] in ( Indices G) by A180, A182, A218, A223, A224, A225, A226, JORDAN1H: 62;

            

             A233: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) meets C & (i1 + 1) = i2 & j1 = j2 implies [i2, (j2 -' 1)] in ( Indices G) by A180, A182, A218, A223, A224, A225, A226, JORDAN1H: 61;

            

             A234: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) meets C & i1 = i2 & (j1 + 1) = j2 implies [(i2 + 1), j2] in ( Indices G) by A180, A182, A218, A223, A224, A225, A226, JORDAN1H: 60;

            

             A235: ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) meets C & i1 = i2 & j1 = (j2 + 1) implies [i2, (j2 -' 1)] in ( Indices G) 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),G)) meets C by A181, A222, A220;

            then

             A238: i1 = i2 & (j1 + 1) = j2 implies [(i1 -' 1), (j1 + 1)] in ( Indices G) by A180, A182, A218, A223, A224, A225, A226, JORDAN1H: 52;

            

             A239: i1 = i2 & j1 = (j2 + 1) implies [(i1 + 1), j2] in ( Indices G) by A180, A182, A218, A223, A224, A225, A226, A237, JORDAN1H: 55;

            

             A240: i1 = (i2 + 1) & j1 = j2 implies [i2, (j1 -' 1)] in ( Indices G) by A180, A182, A218, A223, A224, A225, A226, A237, JORDAN1H: 54;

            

             A241: (i1 + 1) = i2 & j1 = j2 implies [(i1 + 1), (j1 + 1)] in ( Indices G) 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 G

            proof

              per cases ;

                suppose ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C & ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) misses C;

                then

                consider i, j such that

                 A244: ((F . k) ^ <*(G * (i,j))*>) turns_left ((( len (F . k)) -' 1),G) and

                 A245: (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A156, A180, A182, A218, A237;

                set f = ((F . k) ^ <*(G * (i,j))*>);

                

                 A246: (f /. (( len (F . k)) + 1)) = (G * (i,j)) by FINSEQ_4: 67;

                

                 A247: (f /. ( len (F . k))) = (G * (i2,j2)) by A226, A219, FINSEQ_4: 68;

                

                 A248: (f /. (( len (F . k)) -' 1)) = (G * (i1,j1)) by A224, A231, FINSEQ_4: 68;

                thus 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 /. (( len (F . k)) + 1)) = (G * ((i2 -' 1),j2));

                    now

                      let i19,j19,i29,j29 be Nat;

                      assume that

                       A251: [i19, j19] in ( Indices G) and

                       A252: [i29, j29] in ( Indices G) and

                       A253: ((F . k) /. ( len (F . k))) = (G * (i19,j19)) and

                       A254: (G * ((i2 -' 1),j2)) = (G * (i29,j29));

                      

                       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;

                    end;

                    hence thesis by A180, A182, A218, A238, A245, A246, A249, A250, CARD_1: 27, JORDAN8: 6;

                  end;

                    suppose that

                     A258: (i1 + 1) = i2 & j1 = j2 and

                     A259: (f /. (( len (F . k)) + 1)) = (G * (i2,(j2 + 1)));

                    now

                      let i19,j19,i29,j29 be Nat;

                      assume that

                       A260: [i19, j19] in ( Indices G) and

                       A261: [i29, j29] in ( Indices G) and

                       A262: ((F . k) /. ( len (F . k))) = (G * (i19,j19)) and

                       A263: (G * (i2,(j2 + 1))) = (G * (i29,j29));

                      

                       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;

                    end;

                    hence thesis by A180, A182, A218, A241, A245, A246, A258, A259, CARD_1: 27, JORDAN8: 6;

                  end;

                    suppose that

                     A267: i1 = (i2 + 1) & j1 = j2 and

                     A268: (f /. (( len (F . k)) + 1)) = (G * (i2,(j2 -' 1)));

                    now

                      let i19,j19,i29,j29 be Nat;

                      assume that

                       A269: [i19, j19] in ( Indices G) and

                       A270: [i29, j29] in ( Indices G) and

                       A271: ((F . k) /. ( len (F . k))) = (G * (i19,j19)) and

                       A272: (G * (i2,(j2 -' 1))) = (G * (i29,j29));

                      

                       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;

                    end;

                    hence thesis by A180, A182, A218, A240, A245, A246, A267, A268, CARD_1: 27, JORDAN8: 6;

                  end;

                    suppose that

                     A276: i1 = i2 & j1 = (j2 + 1) and

                     A277: (f /. (( len (F . k)) + 1)) = (G * ((i2 + 1),j2));

                    now

                      let i19,j19,i29,j29 be Nat;

                      assume that

                       A278: [i19, j19] in ( Indices G) and

                       A279: [i29, j29] in ( Indices G) and

                       A280: ((F . k) /. ( len (F . k))) = (G * (i19,j19)) and

                       A281: (G * ((i2 + 1),j2)) = (G * (i29,j29));

                      

                       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;

                    end;

                    hence thesis by A180, A182, A218, A239, A245, A246, A276, A277, CARD_1: 27, JORDAN8: 6;

                  end;

                end;

              end;

                suppose

                 A285: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C & ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) meets C;

                then

                consider i, j such that

                 A286: ((F . k) ^ <*(G * (i,j))*>) goes_straight ((( len (F . k)) -' 1),G) and

                 A287: (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A156, A180, A182, A218, A237;

                set f = ((F . k) ^ <*(G * (i,j))*>);

                

                 A288: (f /. (( len (F . k)) + 1)) = (G * (i,j)) by FINSEQ_4: 67;

                

                 A289: (f /. ( len (F . k))) = (G * (i2,j2)) by A226, A219, FINSEQ_4: 68;

                

                 A290: (f /. (( len (F . k)) -' 1)) = (G * (i1,j1)) by A224, A231, FINSEQ_4: 68;

                thus 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 /. (( len (F . k)) + 1)) = (G * (i2,(j2 + 1)));

                    now

                      let i19,j19,i29,j29 be Nat;

                      assume that

                       A293: [i19, j19] in ( Indices G) and

                       A294: [i29, j29] in ( Indices G) and

                       A295: ((F . k) /. ( len (F . k))) = (G * (i19,j19)) and

                       A296: (G * (i2,(j2 + 1))) = (G * (i29,j29));

                      

                       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;

                    end;

                    hence thesis by A180, A182, A218, A229, A285, A287, A288, A291, A292, CARD_1: 27, JORDAN8: 6;

                  end;

                    suppose that

                     A300: (i1 + 1) = i2 & j1 = j2 and

                     A301: (f /. (( len (F . k)) + 1)) = (G * ((i2 + 1),j2));

                    now

                      let i19,j19,i29,j29 be Nat;

                      assume that

                       A302: [i19, j19] in ( Indices G) and

                       A303: [i29, j29] in ( Indices G) and

                       A304: ((F . k) /. ( len (F . k))) = (G * (i19,j19)) and

                       A305: (G * ((i2 + 1),j2)) = (G * (i29,j29));

                      

                       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;

                    end;

                    hence thesis by A180, A182, A218, A228, A285, A287, A288, A300, A301, CARD_1: 27, JORDAN8: 6;

                  end;

                    suppose that

                     A309: i1 = (i2 + 1) & j1 = j2 and

                     A310: (f /. (( len (F . k)) + 1)) = (G * ((i2 -' 1),j2));

                    now

                      let i19,j19,i29,j29 be Nat;

                      assume that

                       A311: [i19, j19] in ( Indices G) and

                       A312: [i29, j29] in ( Indices G) and

                       A313: ((F . k) /. ( len (F . k))) = (G * (i19,j19)) and

                       A314: (G * ((i2 -' 1),j2)) = (G * (i29,j29));

                      

                       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;

                    end;

                    hence thesis by A180, A182, A218, A227, A285, A287, A288, A309, A310, CARD_1: 27, JORDAN8: 6;

                  end;

                    suppose that

                     A318: i1 = i2 & j1 = (j2 + 1) and

                     A319: (f /. (( len (F . k)) + 1)) = (G * (i2,(j2 -' 1)));

                    now

                      let i19,j19,i29,j29 be Nat;

                      assume that

                       A320: [i19, j19] in ( Indices G) and

                       A321: [i29, j29] in ( Indices G) and

                       A322: ((F . k) /. ( len (F . k))) = (G * (i19,j19)) and

                       A323: (G * (i2,(j2 -' 1))) = (G * (i29,j29));

                      

                       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;

                    end;

                    hence thesis by A180, A182, A218, A235, A285, A287, A288, A318, A319, CARD_1: 27, JORDAN8: 6;

                  end;

                end;

              end;

                suppose

                 A327: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) meets C;

                then

                consider i, j such that

                 A328: ((F . k) ^ <*(G * (i,j))*>) turns_right ((( len (F . k)) -' 1),G) and

                 A329: (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A156, A180, A182, A218, A237;

                set f = ((F . k) ^ <*(G * (i,j))*>);

                

                 A330: (f /. (( len (F . k)) + 1)) = (G * (i,j)) by FINSEQ_4: 67;

                

                 A331: (f /. ( len (F . k))) = (G * (i2,j2)) by A226, A219, FINSEQ_4: 68;

                

                 A332: (f /. (( len (F . k)) -' 1)) = (G * (i1,j1)) by A224, A231, FINSEQ_4: 68;

                thus 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 /. (( len (F . k)) + 1)) = (G * ((i2 + 1),j2));

                    now

                      let i19,j19,i29,j29 be Nat;

                      assume that

                       A335: [i19, j19] in ( Indices G) and

                       A336: [i29, j29] in ( Indices G) and

                       A337: ((F . k) /. ( len (F . k))) = (G * (i19,j19)) and

                       A338: (G * ((i2 + 1),j2)) = (G * (i29,j29));

                      

                       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;

                    end;

                    hence thesis by A180, A182, A218, A234, A327, A329, A330, A333, A334, CARD_1: 27, JORDAN8: 6;

                  end;

                    suppose that

                     A342: (i1 + 1) = i2 & j1 = j2 and

                     A343: (f /. (( len (F . k)) + 1)) = (G * (i2,(j2 -' 1)));

                    now

                      let i19,j19,i29,j29 be Nat;

                      assume that

                       A344: [i19, j19] in ( Indices G) and

                       A345: [i29, j29] in ( Indices G) and

                       A346: ((F . k) /. ( len (F . k))) = (G * (i19,j19)) and

                       A347: (G * (i2,(j2 -' 1))) = (G * (i29,j29));

                      

                       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;

                    end;

                    hence thesis by A180, A182, A218, A233, A327, A329, A330, A342, A343, CARD_1: 27, JORDAN8: 6;

                  end;

                    suppose that

                     A351: i1 = (i2 + 1) & j1 = j2 and

                     A352: (f /. (( len (F . k)) + 1)) = (G * (i2,(j2 + 1)));

                    now

                      let i19,j19,i29,j29 be Nat;

                      assume that

                       A353: [i19, j19] in ( Indices G) and

                       A354: [i29, j29] in ( Indices G) and

                       A355: ((F . k) /. ( len (F . k))) = (G * (i19,j19)) and

                       A356: (G * (i2,(j2 + 1))) = (G * (i29,j29));

                      

                       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;

                    end;

                    hence thesis by A180, A182, A218, A232, A327, A329, A330, A351, A352, CARD_1: 27, JORDAN8: 6;

                  end;

                    suppose that

                     A360: i1 = i2 & j1 = (j2 + 1) and

                     A361: (f /. (( len (F . k)) + 1)) = (G * ((i2 -' 1),j2));

                    now

                      let i19,j19,i29,j29 be Nat;

                      assume that

                       A362: [i19, j19] in ( Indices G) and

                       A363: [i29, j29] in ( Indices G) and

                       A364: ((F . k) /. ( len (F . k))) = (G * (i19,j19)) and

                       A365: (G * ((i2 -' 1),j2)) = (G * (i29,j29));

                      

                       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;

                    end;

                    hence thesis by A180, A182, A218, A230, A327, A329, A330, A360, A361, CARD_1: 27, JORDAN8: 6;

                  end;

                end;

              end;

            end;

            let m such that

             A369: 1 <= m and

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

            

             A371: ( right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C by A181, A222, A220;

            now

              per cases ;

                suppose

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

                

                 A373: ((j2 -' 1) + 1) = j2 by A236, XREAL_1: 235;

                

                 A374: ((i2 -' 1) + 1) = i2 by A242, XREAL_1: 235;

                thus thesis

                proof

                  per cases ;

                    suppose

                     A375: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C & ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) misses C;

                    then

                     A376: ex i, j st ((F . k) ^ <*(G * (i,j))*>) turns_left ((( len (F . k)) -' 1),G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A156, A180, A182, A218, A237;

                    then

                     A377: ((F . (k + 1)) /. ( len (F . k))) = (G * (i2,j2)) by A226, A219, FINSEQ_4: 68;

                    

                     A378: ((F . (k + 1)) /. (( len (F . k)) -' 1)) = (G * (i1,j1)) by A224, A231, A376, FINSEQ_4: 68;

                    now

                      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)) = (G * ((i2 -' 1),j2));

                        ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,(i1 -' 1),j2)) by A180, A222, A220, A223, A224, A225, A226, A379, GOBRD13: 34;

                        hence ( right_cell ((F . (k + 1)),m,G)) misses C by A182, A183, A225, A238, A243, A369, A372, A374, A375, A377, A379, A380, GOBRD13: 26;

                        

                         A381: (j2 -' 1) = j1 by A379, NAT_D: 34;

                        ( cell (G,(i1 -' 1),j1)) meets C by A180, A222, A220, A223, A224, A225, A226, A237, A379, GOBRD13: 21;

                        hence ( left_cell ((F . (k + 1)),m,G)) meets C by A182, A183, A225, A238, A243, A369, A372, A374, A377, A379, A380, A381, GOBRD13: 25;

                      end;

                        suppose that

                         A382: (i1 + 1) = i2 & j1 = j2 and

                         A383: ((F . (k + 1)) /. (( len (F . k)) + 1)) = (G * (i2,(j2 + 1)));

                        ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,i2,j2)) by A180, A222, A220, A223, A224, A225, A226, A382, GOBRD13: 36;

                        hence ( right_cell ((F . (k + 1)),m,G)) misses C by A182, A183, A225, A241, A243, A369, A372, A375, A377, A382, A383, GOBRD13: 22;

                        

                         A384: ((i1 + 1) -' 1) = i1 by NAT_D: 34;

                        ( cell (G,i1,j1)) meets C by A180, A222, A220, A223, A224, A225, A226, A237, A382, GOBRD13: 23;

                        hence ( left_cell ((F . (k + 1)),m,G)) meets C by A182, A183, A225, A241, A243, A369, A372, A377, A382, A383, A384, GOBRD13: 21;

                      end;

                        suppose that

                         A385: i1 = (i2 + 1) & j1 = j2 and

                         A386: ((F . (k + 1)) /. (( len (F . k)) + 1)) = (G * (i2,(j2 -' 1)));

                        ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,(i2 -' 1),(j2 -' 1))) by A180, A222, A220, A223, A224, A225, A226, A385, GOBRD13: 38;

                        hence ( right_cell ((F . (k + 1)),m,G)) misses C by A182, A183, A225, A240, A243, A369, A372, A373, A375, A377, A385, A386, GOBRD13: 28;

                        ( cell (G,i2,(j2 -' 1))) meets C by A180, A222, A220, A223, A224, A225, A226, A237, A385, GOBRD13: 25;

                        hence ( left_cell ((F . (k + 1)),m,G)) meets C by A182, A183, A225, A240, A243, A369, A372, A373, A377, A385, A386, GOBRD13: 27;

                      end;

                        suppose that

                         A387: i1 = i2 & j1 = (j2 + 1) and

                         A388: ((F . (k + 1)) /. (( len (F . k)) + 1)) = (G * ((i2 + 1),j2));

                        ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,i2,(j2 -' 1))) by A180, A222, A220, A223, A224, A225, A226, A387, GOBRD13: 40;

                        hence ( right_cell ((F . (k + 1)),m,G)) misses C by A182, A183, A225, A239, A243, A369, A372, A375, A377, A387, A388, GOBRD13: 24;

                        ( cell (G,i2,j2)) meets C by A180, A222, A220, A223, A224, A225, A226, A237, A387, GOBRD13: 27;

                        hence ( left_cell ((F . (k + 1)),m,G)) meets C by A182, A183, A225, A239, A243, A369, A372, A377, A387, A388, GOBRD13: 23;

                      end;

                    end;

                    hence thesis;

                  end;

                    suppose

                     A389: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C & ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) meets C;

                    then

                     A390: ex i, j st ((F . k) ^ <*(G * (i,j))*>) goes_straight ((( len (F . k)) -' 1),G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A156, A180, A182, A218, A237;

                    then

                     A391: ((F . (k + 1)) /. ( len (F . k))) = (G * (i2,j2)) by A226, A219, FINSEQ_4: 68;

                    

                     A392: ((F . (k + 1)) /. (( len (F . k)) -' 1)) = (G * (i1,j1)) by A224, A231, A390, FINSEQ_4: 68;

                    now

                      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)) = (G * (i2,(j2 + 1)));

                        ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,i1,j2)) by A180, A222, A220, A223, A224, A225, A226, A393, GOBRD13: 35;

                        hence ( right_cell ((F . (k + 1)),m,G)) misses C by A182, A183, A225, A229, A243, A369, A372, A389, A391, A393, A394, GOBRD13: 22;

                        ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,(i1 -' 1),j2)) by A180, A222, A220, A223, A224, A225, A226, A393, GOBRD13: 34;

                        hence ( left_cell ((F . (k + 1)),m,G)) meets C by A182, A183, A225, A229, A243, A369, A372, A389, A391, A393, A394, GOBRD13: 21;

                      end;

                        suppose that

                         A395: (i1 + 1) = i2 & j1 = j2 and

                         A396: ((F . (k + 1)) /. (( len (F . k)) + 1)) = (G * ((i2 + 1),j2));

                        ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,i2,(j2 -' 1))) by A180, A222, A220, A223, A224, A225, A226, A395, GOBRD13: 37;

                        hence ( right_cell ((F . (k + 1)),m,G)) misses C by A182, A183, A225, A228, A243, A369, A372, A389, A391, A395, A396, GOBRD13: 24;

                        ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,i2,j2)) by A180, A222, A220, A223, A224, A225, A226, A395, GOBRD13: 36;

                        hence ( left_cell ((F . (k + 1)),m,G)) meets C by A182, A183, A225, A228, A243, A369, A372, A389, A391, A395, A396, GOBRD13: 23;

                      end;

                        suppose that

                         A397: i1 = (i2 + 1) & j1 = j2 and

                         A398: ((F . (k + 1)) /. (( len (F . k)) + 1)) = (G * ((i2 -' 1),j2));

                        ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,(i2 -' 1),j2)) by A180, A222, A220, A223, A224, A225, A226, A397, GOBRD13: 39;

                        hence ( right_cell ((F . (k + 1)),m,G)) misses C by A182, A183, A225, A227, A243, A369, A372, A374, A389, A391, A397, A398, GOBRD13: 26;

                        ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,(i2 -' 1),(j2 -' 1))) by A180, A222, A220, A223, A224, A225, A226, A397, GOBRD13: 38;

                        hence ( left_cell ((F . (k + 1)),m,G)) meets C by A182, A183, A225, A227, A243, A369, A372, A374, A389, A391, A397, A398, GOBRD13: 25;

                      end;

                        suppose that

                         A399: i1 = i2 & j1 = (j2 + 1) and

                         A400: ((F . (k + 1)) /. (( len (F . k)) + 1)) = (G * (i2,(j2 -' 1)));

                        ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,(i2 -' 1),(j2 -' 1))) by A180, A222, A220, A223, A224, A225, A226, A399, GOBRD13: 41;

                        hence ( right_cell ((F . (k + 1)),m,G)) misses C by A182, A183, A225, A235, A243, A369, A372, A373, A389, A391, A399, A400, GOBRD13: 28;

                        ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,i2,(j2 -' 1))) by A180, A222, A220, A223, A224, A225, A226, A399, GOBRD13: 40;

                        hence ( left_cell ((F . (k + 1)),m,G)) meets C by A182, A183, A225, A235, A243, A369, A372, A373, A389, A391, A399, A400, GOBRD13: 27;

                      end;

                    end;

                    hence thesis;

                  end;

                    suppose

                     A401: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) meets C;

                    then

                     A402: ex i, j st ((F . k) ^ <*(G * (i,j))*>) turns_right ((( len (F . k)) -' 1),G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A156, A180, A182, A218, A237;

                    then

                     A403: ((F . (k + 1)) /. ( len (F . k))) = (G * (i2,j2)) by A226, A219, FINSEQ_4: 68;

                    

                     A404: ((F . (k + 1)) /. (( len (F . k)) -' 1)) = (G * (i1,j1)) by A224, A231, A402, FINSEQ_4: 68;

                    now

                      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)) = (G * ((i2 + 1),j2));

                        

                         A407: (j2 -' 1) = j1 by A405, NAT_D: 34;

                        ( cell (G,i1,j1)) misses C by A180, A222, A220, A223, A224, A225, A226, A371, A405, GOBRD13: 22;

                        hence ( right_cell ((F . (k + 1)),m,G)) misses C by A182, A183, A225, A234, A243, A369, A372, A401, A403, A405, A406, A407, GOBRD13: 24;

                        ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,i2,j2)) by A180, A222, A220, A223, A224, A225, A226, A405, GOBRD13: 35;

                        hence ( left_cell ((F . (k + 1)),m,G)) meets C by A182, A183, A225, A234, A243, A369, A372, A401, A403, A405, A406, GOBRD13: 23;

                      end;

                        suppose that

                         A408: (i1 + 1) = i2 & j1 = j2 and

                         A409: ((F . (k + 1)) /. (( len (F . k)) + 1)) = (G * (i2,(j2 -' 1)));

                        

                         A410: (i2 -' 1) = i1 by A408, NAT_D: 34;

                        ( cell (G,i1,(j1 -' 1))) misses C by A180, A222, A220, A223, A224, A225, A226, A371, A408, GOBRD13: 24;

                        hence ( right_cell ((F . (k + 1)),m,G)) misses C by A182, A183, A225, A233, A243, A369, A372, A373, A401, A403, A408, A409, A410, GOBRD13: 28;

                        ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,i2,(j2 -' 1))) by A180, A222, A220, A223, A224, A225, A226, A408, GOBRD13: 37;

                        hence ( left_cell ((F . (k + 1)),m,G)) meets C by A182, A183, A225, A233, A243, A369, A372, A373, A401, A403, A408, A409, GOBRD13: 27;

                      end;

                        suppose that

                         A411: i1 = (i2 + 1) & j1 = j2 and

                         A412: ((F . (k + 1)) /. (( len (F . k)) + 1)) = (G * (i2,(j2 + 1)));

                        ( cell (G,i2,j2)) misses C by A180, A222, A220, A223, A224, A225, A226, A371, A411, GOBRD13: 26;

                        hence ( right_cell ((F . (k + 1)),m,G)) misses C by A182, A183, A225, A232, A243, A369, A372, A401, A403, A411, A412, GOBRD13: 22;

                        ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,(i2 -' 1),j2)) by A180, A222, A220, A223, A224, A225, A226, A411, GOBRD13: 39;

                        hence ( left_cell ((F . (k + 1)),m,G)) meets C by A182, A183, A225, A232, A243, A369, A372, A401, A403, A411, A412, GOBRD13: 21;

                      end;

                        suppose that

                         A413: i1 = i2 & j1 = (j2 + 1) and

                         A414: ((F . (k + 1)) /. (( len (F . k)) + 1)) = (G * ((i2 -' 1),j2));

                        ( cell (G,(i2 -' 1),j2)) misses C by A180, A222, A220, A223, A224, A225, A226, A371, A413, GOBRD13: 28;

                        hence ( right_cell ((F . (k + 1)),m,G)) misses C by A182, A183, A225, A230, A243, A369, A372, A374, A401, A403, A413, A414, GOBRD13: 26;

                        ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) = ( cell (G,(i2 -' 1),(j2 -' 1))) by A180, A222, A220, A223, A224, A225, A226, A413, GOBRD13: 41;

                        hence ( left_cell ((F . (k + 1)),m,G)) meets C by A182, A183, A225, A230, A243, A369, A372, A374, A401, A403, A413, A414, GOBRD13: 25;

                      end;

                    end;

                    hence thesis;

                  end;

                end;

              end;

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

                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 be Nat such that

                 A416: [i1, j1] in ( Indices G) and

                 A417: ((F . k) /. m) = (G * (i1,j1)) and

                 A418: [i2, j2] in ( Indices G) and

                 A419: ((F . k) /. (m + 1)) = (G * (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,G)) misses C by A181, A369, A415;

                 A422:

                now

                  per cases ;

                    suppose ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C & ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) misses C;

                    then

                    consider i, j such that ((F . k) ^ <*(G * (i,j))*>) turns_left ((( len (F . k)) -' 1),G) and

                     A423: (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A156, A180, A182, A218, A237;

                    take i, j;

                    thus (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A423;

                  end;

                    suppose ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C & ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) meets C;

                    then

                    consider i, j such that ((F . k) ^ <*(G * (i,j))*>) goes_straight ((( len (F . k)) -' 1),G) and

                     A424: (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A156, A180, A182, A218, A237;

                    take i, j;

                    thus (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A424;

                  end;

                    suppose ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) meets C;

                    then

                    consider i, j such that ((F . k) ^ <*(G * (i,j))*>) turns_right ((( len (F . k)) -' 1),G) and

                     A425: (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A156, A180, A182, A218, A237;

                    take i, j;

                    thus (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A425;

                  end;

                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)) = (G * (i2,j2)) by A419, A422, FINSEQ_4: 68;

                

                 A427: ( left_cell ((F . k),m,G)) 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) = (G * (i1,j1)) by A417, A422, FINSEQ_4: 68;

                now

                  per cases by A420;

                    suppose

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

                    then

                     A430: ( right_cell ((F . k),m,G)) = ( cell (G,i1,j1)) by A180, A369, A415, A416, A417, A418, A419, GOBRD13: 22;

                    ( left_cell ((F . k),m,G)) = ( cell (G,(i1 -' 1),j1)) by A180, A369, A415, A416, A417, A418, A419, A429, GOBRD13: 21;

                    hence thesis by A243, A369, A370, A416, A418, A421, A427, A428, A426, A429, A430, GOBRD13: 21, GOBRD13: 22;

                  end;

                    suppose

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

                    then

                     A432: ( right_cell ((F . k),m,G)) = ( cell (G,i1,(j1 -' 1))) by A180, A369, A415, A416, A417, A418, A419, GOBRD13: 24;

                    ( left_cell ((F . k),m,G)) = ( cell (G,i1,j1)) by A180, A369, A415, A416, A417, A418, A419, A431, GOBRD13: 23;

                    hence thesis by A243, A369, A370, A416, A418, A421, A427, A428, A426, A431, A432, GOBRD13: 23, GOBRD13: 24;

                  end;

                    suppose

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

                    then

                     A434: ( right_cell ((F . k),m,G)) = ( cell (G,i2,j2)) by A180, A369, A415, A416, A417, A418, A419, GOBRD13: 26;

                    ( left_cell ((F . k),m,G)) = ( cell (G,i2,(j2 -' 1))) by A180, A369, A415, A416, A417, A418, A419, A433, GOBRD13: 25;

                    hence thesis by A243, A369, A370, A416, A418, A421, A427, A428, A426, A433, A434, GOBRD13: 25, GOBRD13: 26;

                  end;

                    suppose

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

                    then

                     A436: ( right_cell ((F . k),m,G)) = ( cell (G,(i1 -' 1),j2)) by A180, A369, A415, A416, A417, A418, A419, GOBRD13: 28;

                    ( left_cell ((F . k),m,G)) = ( cell (G,i2,j2)) by A180, A369, A415, A416, A417, A418, A419, A435, GOBRD13: 27;

                    hence thesis by A243, A369, A370, A416, A418, A421, A427, A428, A426, A435, A436, GOBRD13: 27, GOBRD13: 28;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        

         A437: Q[ 0 ]

        proof

          

           A438: for n st n in ( dom (F . 0 )) & (n + 1) in ( dom (F . 0 )) holds for m, k, i, j st [m, k] in ( Indices G) & [i, j] in ( Indices G) & ((F . 0 ) /. n) = (G * (m,k)) & ((F . 0 ) /. (n + 1)) = (G * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1 by A155;

          for n st n in ( dom (F . 0 )) holds ex i, j st [i, j] in ( Indices G) & ((F . 0 ) /. n) = (G * (i,j)) by A155;

          hence (F . 0 ) is_sequence_on G by A438, GOBOARD1:def 9;

          let m;

          assume that 1 <= m and

           A439: (m + 1) <= ( len (F . 0 ));

          thus thesis by A155, A439, CARD_1: 27;

        end;

        

         A440: for k holds Q[k] from NAT_1:sch 2( A437, A179);

        

         A441: for k, i1, i2, j1, j2 st k > 1 & [i1, j1] in ( Indices G) & ((F . k) /. (( len (F . k)) -' 1)) = (G * (i1,j1)) & [i2, j2] in ( Indices G) & ((F . k) /. ( len (F . k))) = (G * (i2,j2)) holds (( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C & ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) misses C implies (F . (k + 1)) turns_left ((( len (F . k)) -' 1),G) & (i1 = i2 & (j1 + 1) = j2 implies [(i2 -' 1), j2] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 -' 1),j2))*>)) & ((i1 + 1) = i2 & j1 = j2 implies [i2, (j2 + 1)] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 + 1)))*>)) & (i1 = (i2 + 1) & j1 = j2 implies [i2, (j2 -' 1)] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 -' 1)))*>)) & (i1 = i2 & j1 = (j2 + 1) implies [(i2 + 1), j2] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 + 1),j2))*>)))

        proof

          let k, i1, i2, j1, j2 such that

           A442: k > 1 and

           A443: [i1, j1] in ( Indices G) and

           A444: ((F . k) /. (( len (F . k)) -' 1)) = (G * (i1,j1)) and

           A445: [i2, j2] in ( Indices G) and

           A446: ((F . k) /. ( len (F . k))) = (G * (i2,j2));

          

           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 G 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),G)) meets C by A440, A448, A456;

          hereby

            assume that

             A459: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C and

             A460: ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) misses C;

            consider i, j such that

             A461: ((F . k) ^ <*(G * (i,j))*>) turns_left ((( len (F . k)) -' 1),G) and

             A462: (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A156, A442, A451, A447, A458, A459, A460;

            thus (F . (k + 1)) turns_left ((( len (F . k)) -' 1),G) by A461, A462;

            

             A463: ((F . (k + 1)) /. (( len (F . k)) + 1)) = (G * (i,j)) by A462, FINSEQ_4: 67;

            

             A464: ((F . (k + 1)) /. ( len (F . k))) = (G * (i2,j2)) by A446, A453, A462, FINSEQ_4: 68;

            

             A465: ((F . (k + 1)) /. (( len (F . k)) -' 1)) = (G * (i1,j1)) by A444, A449, A462, FINSEQ_4: 68;

            hence i1 = i2 & (j1 + 1) = j2 implies [(i2 -' 1), j2] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 -' 1),j2))*>) by A443, A445, A456, A457, A452, A455, A461, A462, A464, A463, GOBRD13:def 7;

            thus (i1 + 1) = i2 & j1 = j2 implies [i2, (j2 + 1)] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 + 1)))*>) by A443, A445, A456, A457, A450, A454, A461, A462, A465, A464, A463, GOBRD13:def 7;

            thus i1 = (i2 + 1) & j1 = j2 implies [i2, (j2 -' 1)] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 -' 1)))*>) by A443, A445, A456, A457, A450, A454, A461, A462, A465, A464, A463, GOBRD13:def 7;

            thus i1 = i2 & j1 = (j2 + 1) implies [(i2 + 1), j2] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 + 1),j2))*>) by A443, A445, A456, A457, A452, A455, A461, A462, A465, A464, A463, GOBRD13:def 7;

          end;

        end;

        defpred P[ Nat] means for m st m <= $1 holds ((F . $1) | m) = (F . m);

        

         A466: P[ 0 ]

        proof

          let m;

          assume m <= 0 ;

          then 0 = m;

          hence thesis by A155;

        end;

        defpred K[ Nat] means ex w be Nat st w = $1 & $1 >= 1 & ex m st m in ( dom (F . w)) & m <> ( len (F . w)) & ((F . w) /. m) = ((F . w) /. ( len (F . w)));

        

         A467: P[ 0 , (F . 0 ), (F . ( 0 + 1))] by A156;

        

         A468: for k, i1, i2, j1, j2 st k > 1 & [i1, j1] in ( Indices G) & ((F . k) /. (( len (F . k)) -' 1)) = (G * (i1,j1)) & [i2, j2] in ( Indices G) & ((F . k) /. ( len (F . k))) = (G * (i2,j2)) holds (( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C & ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) meets C implies (F . (k + 1)) goes_straight ((( len (F . k)) -' 1),G) & (i1 = i2 & (j1 + 1) = j2 implies [i2, (j2 + 1)] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 + 1)))*>)) & ((i1 + 1) = i2 & j1 = j2 implies [(i2 + 1), j2] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 + 1),j2))*>)) & (i1 = (i2 + 1) & j1 = j2 implies [(i2 -' 1), j2] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 -' 1),j2))*>)) & (i1 = i2 & j1 = (j2 + 1) implies [i2, (j2 -' 1)] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 -' 1)))*>)))

        proof

          let k, i1, i2, j1, j2 such that

           A469: k > 1 and

           A470: [i1, j1] in ( Indices G) and

           A471: ((F . k) /. (( len (F . k)) -' 1)) = (G * (i1,j1)) and

           A472: [i2, j2] in ( Indices G) and

           A473: ((F . k) /. ( len (F . k))) = (G * (i2,j2));

          

           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 G 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),G)) meets C by A440, A475, A483;

          hereby

            assume that

             A486: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C and

             A487: ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) meets C;

            consider i, j such that

             A488: ((F . k) ^ <*(G * (i,j))*>) goes_straight ((( len (F . k)) -' 1),G) and

             A489: (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>) by A156, A469, A478, A474, A485, A486, A487;

            thus (F . (k + 1)) goes_straight ((( len (F . k)) -' 1),G) by A488, A489;

            

             A490: ((F . (k + 1)) /. (( len (F . k)) + 1)) = (G * (i,j)) by A489, FINSEQ_4: 67;

            

             A491: ((F . (k + 1)) /. ( len (F . k))) = (G * (i2,j2)) by A473, A480, A489, FINSEQ_4: 68;

            

             A492: ((F . (k + 1)) /. (( len (F . k)) -' 1)) = (G * (i1,j1)) by A471, A476, A489, FINSEQ_4: 68;

            hence i1 = i2 & (j1 + 1) = j2 implies [i2, (j2 + 1)] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 + 1)))*>) by A470, A472, A483, A484, A479, A482, A488, A489, A491, A490, GOBRD13:def 8;

            thus (i1 + 1) = i2 & j1 = j2 implies [(i2 + 1), j2] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 + 1),j2))*>) by A470, A472, A483, A484, A477, A481, A488, A489, A492, A491, A490, GOBRD13:def 8;

            thus i1 = (i2 + 1) & j1 = j2 implies [(i2 -' 1), j2] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 -' 1),j2))*>) by A470, A472, A483, A484, A477, A481, A488, A489, A492, A491, A490, GOBRD13:def 8;

            thus i1 = i2 & j1 = (j2 + 1) implies [i2, (j2 -' 1)] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 -' 1)))*>) by A470, A472, A483, A484, A479, A482, A488, A489, A492, A491, A490, GOBRD13:def 8;

          end;

        end;

        

         A493: for k, i1, i2, j1, j2 st k > 1 & [i1, j1] in ( Indices G) & ((F . k) /. (( len (F . k)) -' 1)) = (G * (i1,j1)) & [i2, j2] in ( Indices G) & ((F . k) /. ( len (F . k))) = (G * (i2,j2)) holds (( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) meets C implies (F . (k + 1)) turns_right ((( len (F . k)) -' 1),G) & (i1 = i2 & (j1 + 1) = j2 implies [(i2 + 1), j2] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 + 1),j2))*>)) & ((i1 + 1) = i2 & j1 = j2 implies [i2, (j2 -' 1)] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 -' 1)))*>)) & (i1 = (i2 + 1) & j1 = j2 implies [i2, (j2 + 1)] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 + 1)))*>)) & (i1 = i2 & j1 = (j2 + 1) implies [(i2 -' 1), j2] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 -' 1),j2))*>)))

        proof

          let k, i1, i2, j1, j2 such that

           A494: k > 1 and

           A495: [i1, j1] in ( Indices G) and

           A496: ((F . k) /. (( len (F . k)) -' 1)) = (G * (i1,j1)) and

           A497: [i2, j2] in ( Indices G) and

           A498: ((F . k) /. ( len (F . k))) = (G * (i2,j2));

          

           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 G by A440;

          assume

           A503: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) meets C;

          

           A504: 1 <= (( len (F . k)) -' 1) by A494, A499, NAT_D: 49;

          then ( left_cell ((F . k),(( len (F . k)) -' 1),G)) meets C by A440, A500;

          then

          consider i, j such that

           A505: ((F . k) ^ <*(G * (i,j))*>) turns_right ((( len (F . k)) -' 1),G) and

           A506: (F . (k + 1)) = ((F . k) ^ <*(G * (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))) = (G * (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)) = (G * (i1,j1)) by A496, A506, FINSEQ_4: 68;

          thus (F . (k + 1)) turns_right ((( len (F . k)) -' 1),G) by A505, A506;

          

           A509: ((F . (k + 1)) /. (( len (F . k)) + 1)) = (G * (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 G) & (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 + 1),j2))*>) by A495, A497, A500, A501, A510, A505, A506, A508, A507, A509, GOBRD13:def 6;

          

           A513: (i1 + 1) > i1 by NAT_1: 13;

          hence (i1 + 1) = i2 & j1 = j2 implies [i2, (j2 -' 1)] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 -' 1)))*>) by A495, A497, A500, A501, A511, A505, A506, A508, A507, A509, GOBRD13:def 6;

          thus i1 = (i2 + 1) & j1 = j2 implies [i2, (j2 + 1)] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 + 1)))*>) by A495, A497, A500, A501, A513, A511, A505, A506, A508, A507, A509, GOBRD13:def 6;

          thus thesis by A495, A497, A500, A501, A512, A510, A505, A506, A508, A507, A509, GOBRD13:def 6;

        end;

        

         A514: for k 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 such that

           A515: k > 1;

          

           A516: (F . k) is_sequence_on G 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 be Nat st [i1, j1] in ( Indices G) & ((F . k) /. (( len (F . k)) -' 1)) = (G * (i1,j1)) & [i2, j2] in ( Indices G) & ((F . k) /. ( len (F . k))) = (G * (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 thesis by A441, A468, A493, A515, A517;

        end;

        

         A519: P[1, (F . 1), (F . (1 + 1))] by A156;

        

         A520: for k holds ex i, j st [i, j] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (i,j))*>)

        proof

          let k;

          

           A521: (F . k) is_sequence_on G by A440;

          

           A522: ( len (F . k)) = k by A177;

          per cases by XXREAL_0: 1;

            suppose

             A523: k < 1;

            take ( X-SpanStart (C,n)), ( Y-SpanStart (C,n));

            thus [( X-SpanStart (C,n)), ( Y-SpanStart (C,n))] in ( Indices G) by A1, JORDAN11: 8;

            k = 0 by A523, NAT_1: 14;

            hence thesis by A155, A467, FINSEQ_1: 34;

          end;

            suppose

             A524: k = 1;

            take (( X-SpanStart (C,n)) -' 1), ( Y-SpanStart (C,n));

            thus [(( X-SpanStart (C,n)) -' 1), ( Y-SpanStart (C,n))] in ( Indices G) by A1, JORDAN11: 9;

            thus thesis by A467, A519, A524, FINSEQ_1:def 9;

          end;

            suppose

             A525: k > 1;

            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 be Nat such that

             A527: [i1, j1] in ( Indices G) and

             A528: ((F . k) /. (( len (F . k)) -' 1)) = (G * (i1,j1)) and

             A529: [i2, j2] in ( Indices G) and

             A530: ((F . k) /. ( len (F . k))) = (G * (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

              per cases ;

                suppose

                 A532: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C & ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) misses C;

                now

                  per cases by A531;

                    suppose

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

                    then

                     A534: (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 -' 1),j2))*>) by A441, A525, A527, A528, A529, A530, A532;

                     [(i2 -' 1), j2] in ( Indices G) by A441, A525, A527, A528, A529, A530, A532, A533;

                    hence thesis by A534;

                  end;

                    suppose

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

                    then

                     A536: (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 + 1)))*>) by A441, A525, A527, A528, A529, A530, A532;

                     [i2, (j2 + 1)] in ( Indices G) by A441, A525, A527, A528, A529, A530, A532, A535;

                    hence thesis by A536;

                  end;

                    suppose

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

                    then

                     A538: (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 -' 1)))*>) by A441, A525, A527, A528, A529, A530, A532;

                     [i2, (j2 -' 1)] in ( Indices G) by A441, A525, A527, A528, A529, A530, A532, A537;

                    hence thesis by A538;

                  end;

                    suppose

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

                    then

                     A540: (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 + 1),j2))*>) by A441, A525, A527, A528, A529, A530, A532;

                     [(i2 + 1), j2] in ( Indices G) by A441, A525, A527, A528, A529, A530, A532, A539;

                    hence thesis by A540;

                  end;

                end;

                hence thesis;

              end;

                suppose

                 A541: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C & ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) meets C;

                now

                  per cases by A531;

                    suppose

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

                    then

                     A543: (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 + 1)))*>) by A468, A525, A527, A528, A529, A530, A541;

                     [i2, (j2 + 1)] in ( Indices G) by A468, A525, A527, A528, A529, A530, A541, A542;

                    hence thesis by A543;

                  end;

                    suppose

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

                    then

                     A545: (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 + 1),j2))*>) by A468, A525, A527, A528, A529, A530, A541;

                     [(i2 + 1), j2] in ( Indices G) by A468, A525, A527, A528, A529, A530, A541, A544;

                    hence thesis by A545;

                  end;

                    suppose

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

                    then

                     A547: (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 -' 1),j2))*>) by A468, A525, A527, A528, A529, A530, A541;

                     [(i2 -' 1), j2] in ( Indices G) by A468, A525, A527, A528, A529, A530, A541, A546;

                    hence thesis by A547;

                  end;

                    suppose

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

                    then

                     A549: (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 -' 1)))*>) by A468, A525, A527, A528, A529, A530, A541;

                     [i2, (j2 -' 1)] in ( Indices G) by A468, A525, A527, A528, A529, A530, A541, A548;

                    hence thesis by A549;

                  end;

                end;

                hence thesis;

              end;

                suppose

                 A550: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) meets C;

                now

                  per cases by A531;

                    suppose

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

                    then

                     A552: (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 + 1),j2))*>) by A493, A525, A527, A528, A529, A530, A550;

                     [(i2 + 1), j2] in ( Indices G) by A493, A525, A527, A528, A529, A530, A550, A551;

                    hence thesis by A552;

                  end;

                    suppose

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

                    then

                     A554: (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 -' 1)))*>) by A493, A525, A527, A528, A529, A530, A550;

                     [i2, (j2 -' 1)] in ( Indices G) by A493, A525, A527, A528, A529, A530, A550, A553;

                    hence thesis by A554;

                  end;

                    suppose

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

                    then

                     A556: (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 + 1)))*>) by A493, A525, A527, A528, A529, A530, A550;

                     [i2, (j2 + 1)] in ( Indices G) by A493, A525, A527, A528, A529, A530, A550, A555;

                    hence thesis by A556;

                  end;

                    suppose

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

                    then

                     A558: (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 -' 1),j2))*>) by A493, A525, A527, A528, A529, A530, A550;

                     [(i2 -' 1), j2] in ( Indices G) by A493, A525, A527, A528, A529, A530, A550, A557;

                    hence thesis by A558;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        

         A559: for k st P[k] holds P[(k + 1)]

        proof

          let k such that

           A560: for m st m <= k holds ((F . k) | m) = (F . m);

          let m such that

           A561: m <= (k + 1);

          per cases by A561, XXREAL_0: 1;

            suppose m < (k + 1);

            then

             A562: m <= k by NAT_1: 13;

            

             A563: ex i, j st [i, j] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (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 thesis by A560, A562;

          end;

            suppose

             A564: m = (k + 1);

            ( len (F . (k + 1))) = (k + 1) by A177;

            hence thesis by A564, FINSEQ_1: 58;

          end;

        end;

        

         A565: for k holds P[k] from NAT_1:sch 2( A466, A559);

        

         A566: for j, k st 1 <= j & j <= k holds ((F . k) /. j) = ((F . j) /. j)

        proof

          let j, k;

          assume that

           A567: 1 <= j and

           A568: j <= k;

          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 thesis by A569, FINSEQ_4: 70;

        end;

        defpred P[ Nat] means (F . $1) is unfolded;

        

         A570: for k st P[k] holds P[(k + 1)]

        proof

          let k such that

           A571: (F . k) is unfolded;

          

           A572: (F . k) is_sequence_on G by A440;

          per cases ;

            suppose k <= 1;

            then (k + 1) <= (1 + 1) by XREAL_1: 6;

            then ( len (F . (k + 1))) <= 2 by A177;

            hence thesis by SPPOL_2: 26;

          end;

            suppose

             A573: k > 1;

            set m = (k -' 1);

            

             A574: (m + 1) = k by A573, XREAL_1: 235;

            

             A575: ( len (F . k)) = k by A177;

            

             A576: 1 <= m by A573, NAT_D: 49;

            then

            consider i1,j1,i2,j2 be Nat such that

             A577: [i1, j1] in ( Indices G) and

             A578: ((F . k) /. m) = (G * (i1,j1)) and

             A579: [i2, j2] in ( Indices G) and

             A580: ((F . k) /. ( len (F . k))) = (G * (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),m)) = ( LSeg ((G * (i1,j1)),(G * (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 G) by A577, MATRIX_0: 32;

            

             A589: j2 <= ( width G) by A579, MATRIX_0: 32;

            

             A590: 1 <= i1 by A577, MATRIX_0: 32;

            

             A591: j1 <= ( width G) by A577, MATRIX_0: 32;

            

             A592: i2 <= ( len G) by A579, MATRIX_0: 32;

            now

              per cases ;

                suppose

                 A593: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C & ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) misses C;

                now

                  per cases by A581;

                    suppose

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

                    then [(i2 -' 1), j2] in ( Indices G) by A441, A573, A575, A577, A578, A579, A580, A593;

                    then 1 <= (i2 -' 1) by MATRIX_0: 32;

                    then

                     A595: (( LSeg ((F . k),m)) /\ ( LSeg (((F . k) /. ( len (F . k))),(G * ((i2 -' 1),j2))))) = {((F . k) /. ( len (F . k)))} by A580, A588, A585, A589, A587, A582, A594, GOBOARD7: 16;

                    (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 -' 1),j2))*>) by A441, A573, A575, A577, A578, A579, A580, A593, A594;

                    hence thesis by A571, A574, A575, A595, SPPOL_2: 30;

                  end;

                    suppose

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

                    then [i2, (j2 + 1)] in ( Indices G) by A441, A573, A575, A577, A578, A579, A580, A593;

                    then (j2 + 1) <= ( width G) by MATRIX_0: 32;

                    then

                     A597: (( LSeg ((F . k),m)) /\ ( LSeg (((F . k) /. ( len (F . k))),(G * (i2,(j2 + 1)))))) = {((F . k) /. ( len (F . k)))} by A580, A590, A585, A592, A582, A596, GOBOARD7: 18;

                    (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 + 1)))*>) by A441, A573, A575, A577, A578, A579, A580, A593, A596;

                    hence thesis by A571, A574, A575, A597, SPPOL_2: 30;

                  end;

                    suppose

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

                    then [i2, (j2 -' 1)] in ( Indices G) by A441, A573, A575, A577, A578, A579, A580, A593;

                    then 1 <= (j2 -' 1) by MATRIX_0: 32;

                    then

                     A599: (( LSeg ((F . k),m)) /\ ( LSeg (((F . k) /. ( len (F . k))),(G * (i2,(j2 -' 1)))))) = {((F . k) /. ( len (F . k)))} by A580, A588, A591, A586, A584, A582, A598, GOBOARD7: 15;

                    (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 -' 1)))*>) by A441, A573, A575, A577, A578, A579, A580, A593, A598;

                    hence thesis by A571, A574, A575, A599, SPPOL_2: 30;

                  end;

                    suppose

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

                    then [(i2 + 1), j2] in ( Indices G) by A441, A573, A575, A577, A578, A579, A580, A593;

                    then (i2 + 1) <= ( len G) by MATRIX_0: 32;

                    then

                     A601: (( LSeg ((F . k),m)) /\ ( LSeg (((F . k) /. ( len (F . k))),(G * ((i2 + 1),j2))))) = {((F . k) /. ( len (F . k)))} by A580, A590, A591, A583, A582, A600, GOBOARD7: 17;

                    (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 + 1),j2))*>) by A441, A573, A575, A577, A578, A579, A580, A593, A600;

                    hence thesis by A571, A574, A575, A601, SPPOL_2: 30;

                  end;

                end;

                hence thesis;

              end;

                suppose

                 A602: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) misses C & ( front_left_cell ((F . k),(( len (F . k)) -' 1),G)) meets C;

                now

                  per cases by A581;

                    suppose

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

                    then [i2, (j2 + 1)] in ( Indices G) by A468, A573, A575, A577, A578, A579, A580, A602;

                    then

                     A604: (j2 + 1) <= ( width G) by MATRIX_0: 32;

                    (j2 + 1) = (j1 + (1 + 1)) by A603;

                    then

                     A605: (( LSeg ((F . k),m)) /\ ( LSeg (((F . k) /. ( len (F . k))),(G * (i2,(j2 + 1)))))) = {((F . k) /. ( len (F . k)))} by A580, A590, A588, A585, A582, A603, A604, GOBOARD7: 13;

                    (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 + 1)))*>) by A468, A573, A575, A577, A578, A579, A580, A602, A603;

                    hence thesis by A571, A574, A575, A605, SPPOL_2: 30;

                  end;

                    suppose

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

                    then [(i2 + 1), j2] in ( Indices G) by A468, A573, A575, A577, A578, A579, A580, A602;

                    then

                     A607: (i2 + 1) <= ( len G) by MATRIX_0: 32;

                    (i2 + 1) = (i1 + (1 + 1)) by A606;

                    then

                     A608: (( LSeg ((F . k),m)) /\ ( LSeg (((F . k) /. ( len (F . k))),(G * ((i2 + 1),j2))))) = {((F . k) /. ( len (F . k)))} by A580, A590, A585, A591, A582, A606, A607, GOBOARD7: 14;

                    (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 + 1),j2))*>) by A468, A573, A575, A577, A578, A579, A580, A602, A606;

                    hence thesis by A571, A574, A575, A608, SPPOL_2: 30;

                  end;

                    suppose

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

                    then [(i2 -' 1), j2] in ( Indices G) 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),m)) /\ ( LSeg (((F . k) /. ( len (F . k))),(G * ((i2 -' 1),j2))))) = {((F . k) /. ( len (F . k)))} by A580, A588, A585, A591, A587, A582, A609, A610, GOBOARD7: 14;

                    (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 -' 1),j2))*>) by A468, A573, A575, A577, A578, A579, A580, A602, A609;

                    hence thesis by A571, A574, A575, A611, SPPOL_2: 30;

                  end;

                    suppose

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

                    then [i2, (j2 -' 1)] in ( Indices G) 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),m)) /\ ( LSeg (((F . k) /. ( len (F . k))),(G * (i2,(j2 -' 1)))))) = {((F . k) /. ( len (F . k)))} by A580, A590, A588, A591, A584, A582, A612, A613, GOBOARD7: 13;

                    (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 -' 1)))*>) by A468, A573, A575, A577, A578, A579, A580, A602, A612;

                    hence thesis by A571, A574, A575, A614, SPPOL_2: 30;

                  end;

                end;

                hence thesis;

              end;

                suppose

                 A615: ( front_right_cell ((F . k),(( len (F . k)) -' 1),G)) meets C;

                now

                  per cases by A581;

                    suppose

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

                    then [(i2 + 1), j2] in ( Indices G) by A493, A573, A575, A577, A578, A579, A580, A615;

                    then (i2 + 1) <= ( len G) by MATRIX_0: 32;

                    then

                     A617: (( LSeg ((F . k),m)) /\ ( LSeg (((F . k) /. ( len (F . k))),(G * ((i2 + 1),j2))))) = {((F . k) /. ( len (F . k)))} by A580, A590, A585, A589, A582, A616, GOBOARD7: 15;

                    (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 + 1),j2))*>) by A493, A573, A575, A577, A578, A579, A580, A615, A616;

                    hence thesis by A571, A574, A575, A617, SPPOL_2: 30;

                  end;

                    suppose

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

                    then [i2, (j2 -' 1)] in ( Indices G) by A493, A573, A575, A577, A578, A579, A580, A615;

                    then 1 <= (j2 -' 1) by MATRIX_0: 32;

                    then

                     A619: (( LSeg ((F . k),m)) /\ ( LSeg (((F . k) /. ( len (F . k))),(G * (i2,(j2 -' 1)))))) = {((F . k) /. ( len (F . k)))} by A580, A590, A591, A592, A584, A582, A618, GOBOARD7: 16;

                    (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 -' 1)))*>) by A493, A573, A575, A577, A578, A579, A580, A615, A618;

                    hence thesis by A571, A574, A575, A619, SPPOL_2: 30;

                  end;

                    suppose

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

                    then [i2, (j2 + 1)] in ( Indices G) by A493, A573, A575, A577, A578, A579, A580, A615;

                    then (j2 + 1) <= ( width G) by MATRIX_0: 32;

                    then

                     A621: (( LSeg ((F . k),m)) /\ ( LSeg (((F . k) /. ( len (F . k))),(G * (i2,(j2 + 1)))))) = {((F . k) /. ( len (F . k)))} by A580, A588, A585, A586, A582, A620, GOBOARD7: 17;

                    (F . (k + 1)) = ((F . k) ^ <*(G * (i2,(j2 + 1)))*>) by A493, A573, A575, A577, A578, A579, A580, A615, A620;

                    hence thesis by A571, A574, A575, A621, SPPOL_2: 30;

                  end;

                    suppose

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

                    then [(i2 -' 1), j2] in ( Indices G) by A493, A573, A575, A577, A578, A579, A580, A615;

                    then 1 <= (i2 -' 1) by MATRIX_0: 32;

                    then

                     A623: (( LSeg ((F . k),m)) /\ ( LSeg (((F . k) /. ( len (F . k))),(G * ((i2 -' 1),j2))))) = {((F . k) /. ( len (F . k)))} by A580, A588, A591, A583, A587, A582, A622, GOBOARD7: 18;

                    (F . (k + 1)) = ((F . k) ^ <*(G * ((i2 -' 1),j2))*>) by A493, A573, A575, A577, A578, A579, A580, A615, A622;

                    hence thesis by A571, A574, A575, A623, SPPOL_2: 30;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        now

          defpred P[ Nat] means (F . $1) is one-to-one;

          assume

           A624: for k st k >= 1 holds for m st m in ( dom (F . k)) & m <> ( len (F . k)) holds ((F . k) /. m) <> ((F . k) /. ( len (F . k)));

          

           A625: for k st P[k] holds P[(k + 1)]

          proof

            let k;

            assume

             A626: (F . k) is one-to-one;

            now

              let n,m be Element of NAT such 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);

              

               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 st [i, j] in ( Indices G) & (F . (k + 1)) = ((F . k) ^ <*(G * (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;

                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;

              end;

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

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

              end;

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

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

              end;

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

                hence n = m;

              end;

            end;

            hence thesis by PARTFUN2: 9;

          end;

          

           A641: P[ 0 ] by A155;

          

           A642: for k holds P[k] from NAT_1:sch 2( A641, A625);

          

           A643: for k holds ( card ( rng (F . k))) = k

          proof

            let k;

            (F . k) is one-to-one by A642;

            

            hence ( card ( rng (F . k))) = ( len (F . k)) by FINSEQ_4: 62

            .= k by A177;

          end;

          reconsider k = ((( len G) * ( width G)) + 1) as Nat;

          

           A644: k > (( len G) * ( width G)) by NAT_1: 13;

          (F . k) is_sequence_on G by A440;

          then

           A645: ( card ( rng (F . k))) <= ( card ( Values G)) by GOBRD13: 8, NAT_1: 43;

          ( card ( Values G)) <= (( len G) * ( width G)) by MATRIX_0: 40;

          then ( card ( rng (F . k))) <= (( len G) * ( width G)) by A645, XXREAL_0: 2;

          hence contradiction by A643, A644;

        end;

        then

         A646: ex k be Nat st K[k];

        consider k be Nat such that

         A647: K[k] and

         A648: for l be Nat st K[l] holds k <= l from NAT_1:sch 5( A646);

        reconsider k as Nat;

        consider m 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 G 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: P[ 0 ] by A155, CARD_1: 27, SPPOL_2: 26;

        for k holds P[k] from NAT_1:sch 2( A658, A570);

        then

        reconsider f as non constant special unfolded non empty 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 be standard non constant special_circular_sequence st ( L~ h) c= ( L~ f) holds for Comp be Subset of ( TOP-REAL 2) st Comp is_a_component_of (( L~ h) ` ) holds for n st 1 <= n & (n + 1) <= ( len f) & (f /. n) in Comp & not (f /. n) in ( L~ h) holds C meets Comp

        proof

          let h be standard non constant special_circular_sequence such that

           A661: ( L~ h) c= ( L~ f);

          let Comp be Subset of ( TOP-REAL 2) such that

           A662: Comp is_a_component_of (( L~ h) ` );

          let n such that

           A663: 1 <= n and

           A664: (n + 1) <= ( len f) and

           A665: (f /. n) in Comp and

           A666: not (f /. n) in ( L~ h);

          set rc = (( left_cell (f,n,G)) \ ( L~ h));

          reconsider rc as Subset of ( TOP-REAL 2);

          

           A667: ( Int ( left_cell (f,n,G))) c= ( left_cell (f,n,G)) by TOPS_1: 16;

          (f /. n) in ( left_cell (f,n,G)) by A653, A663, A664, JORDAN9: 8;

          then (f /. n) in rc by A666, XBOOLE_0:def 5;

          then

           A668: rc meets Comp by A665, XBOOLE_0: 3;

          

           A669: rc = (( left_cell (f,n,G)) /\ (( L~ h) ` )) by SUBSET_1: 13;

          then

           A670: rc c= (( L~ h) ` ) by XBOOLE_1: 17;

          ( Int ( left_cell (f,n,G))) misses ( L~ f) by A653, A663, A664, JORDAN9: 15;

          then ( Int ( left_cell (f,n,G))) misses ( L~ h) by A661, XBOOLE_1: 63;

          then

           A671: ( Int ( left_cell (f,n,G))) c= (( L~ h) ` ) by SUBSET_1: 23;

          rc c= ( left_cell (f,n,G)) by XBOOLE_1: 36;

          then

           A672: rc c= ( Cl ( Int ( left_cell (f,n,G)))) by A653, A663, A664, JORDAN9: 11;

          

           A673: rc meets C

          proof

            ( left_cell (f,n,G)) meets C by A440, A663, A664;

            then

            consider p be object such that

             A674: p in ( left_cell (f,n,G)) and

             A675: p in C by XBOOLE_0: 3;

            reconsider p as Element of ( TOP-REAL 2) by A674;

            now

              take p;

              now

                assume p in ( L~ h);

                then

                consider j 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,G)) /\ ( left_cell (f,j,G))) by A440, A676, A677, A678, GOBRD13: 29;

                then

                 A679: p in ( right_cell (f,j,G)) by XBOOLE_0:def 4;

                ( right_cell (f,j,G)) misses C by A440, A676, A677;

                hence contradiction by A675, A679, XBOOLE_0: 3;

              end;

              hence p in rc by A674, XBOOLE_0:def 5;

              thus p in C by A675;

            end;

            hence thesis by XBOOLE_0: 3;

          end;

          ( Int ( left_cell (f,n,G))) 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 thesis by A673, XBOOLE_1: 63;

        end;

        

         A680: for i st 1 <= i & (i + 1) <= ( len f) holds ( left_cell (f,i,G)) = ( Cl ( Int ( left_cell (f,i,G))))

        proof

          let i such that

           A681: 1 <= i and

           A682: (i + 1) <= ( len f);

          consider i1, j1, i2, j2 such that

           A683: [i1, j1] in ( Indices G) and

           A684: (f /. i) = (G * (i1,j1)) and

           A685: [i2, j2] in ( Indices G) and

           A686: (f /. (i + 1)) = (G * (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 G) by A683, MATRIX_0: 32;

          

           A689: i2 <= ( len G) by A685, MATRIX_0: 32;

          

           A690: (i1 + 1) > i1 by NAT_1: 13;

          

           A691: j1 <= ( width G) by A683, MATRIX_0: 32;

          

           A692: (j1 + 1) > j1 by NAT_1: 13;

          

           A693: j2 <= ( width G) 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;

            

             A697: (i1 -' 1) <= ( len G) by A688, NAT_D: 44;

            ( left_cell (f,i,G)) = ( cell (G,(i1 -' 1),j1)) by A653, A681, A682, A683, A684, A685, A686, A692, A695, A696, GOBRD13:def 3;

            hence thesis by A691, A697, GOBRD11: 35;

          end;

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

            then ( left_cell (f,i,G)) = ( cell (G,i1,j1)) by A653, A681, A682, A683, A684, A685, A686, A690, A694, GOBRD13:def 3;

            hence thesis by A688, A691, GOBRD11: 35;

          end;

            suppose

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

            

             A699: (j2 -' 1) <= ( width G) by A693, NAT_D: 44;

            ( left_cell (f,i,G)) = ( cell (G,i2,(j2 -' 1))) by A653, A681, A682, A683, A684, A685, A686, A690, A694, A698, GOBRD13:def 3;

            hence thesis by A689, A699, GOBRD11: 35;

          end;

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

            then ( left_cell (f,i,G)) = ( cell (G,i1,j2)) by A653, A681, A682, A683, A684, A685, A686, A692, A695, GOBRD13:def 3;

            hence thesis by A688, A693, GOBRD11: 35;

          end;

        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 g) = (( len f) - (m -' 1)) by RFINSEQ:def 1;

        then ((m -' 1) - (m -' 1)) < ( len g) by A700, XREAL_1: 9;

        then

        reconsider g 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 G by A440, JORDAN8: 2;

        then

         A706: g is standard by JORDAN8: 4;

        

         A707: g is non constant

        proof

          take 1, 2;

          thus

           A708: 1 in ( dom g) by FINSEQ_5: 6;

          thus

           A709: 2 in ( dom g) by A703, FINSEQ_3: 25;

          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 thesis by A709, PARTFUN1:def 6;

        end;

        

         A710: ( len (F . k)) = k by A177;

        

         A711: for i st 1 <= i & i < ( len g) & 1 <= j & j < ( len g) & (g /. i) = (g /. j) holds i = j

        proof

          let i such 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;

          

           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;

            set l = ((m -' 1) + j), m9 = ((m -' 1) + i);

            

             A723: m9 < l by A722, XREAL_1: 6;

            

             A724: ( len (F . l)) = l by A177;

            

             A725: l < k by A710, A701, A715, XREAL_1: 20;

            then

             A726: (f | l) = (F . l) by A565;

            ( 0 + j) <= l by XREAL_1: 6;

            then

             A727: 1 <= l by A714, XXREAL_0: 2;

            then l in ( dom (F . l)) by A724, FINSEQ_3: 25;

            then

             A728: ((F . l) /. l) = (f /. l) by A726, FINSEQ_4: 70;

            ( 0 + i) <= m9 by XREAL_1: 6;

            then 1 <= m9 by A712, XXREAL_0: 2;

            then

             A729: m9 in ( dom (F . l)) by A723, A724, FINSEQ_3: 25;

            then ((F . l) /. m9) = (f /. m9) by A726, FINSEQ_4: 70;

            hence contradiction by A648, A716, A719, A720, A723, A725, A727, A724, A729, A728, FINSEQ_5: 27;

          end;

            suppose

             A730: j < i;

            set l = ((m -' 1) + i), m9 = ((m -' 1) + j);

            

             A731: m9 < l by A730, XREAL_1: 6;

            

             A732: ( len (F . l)) = l by A177;

            

             A733: l < k by A710, A701, A713, XREAL_1: 20;

            then

             A734: (f | l) = (F . l) by A565;

            ( 0 + i) <= l by XREAL_1: 6;

            then

             A735: 1 <= l by A712, XXREAL_0: 2;

            then l in ( dom (F . l)) by A732, FINSEQ_3: 25;

            then

             A736: ((F . l) /. l) = (f /. l) by A734, FINSEQ_4: 70;

            ( 0 + j) <= m9 by XREAL_1: 6;

            then 1 <= m9 by A714, XXREAL_0: 2;

            then

             A737: m9 in ( dom (F . l)) by A731, A732, FINSEQ_3: 25;

            then ((F . l) /. m9) = (f /. m9) by A734, FINSEQ_4: 70;

            hence contradiction by A648, A716, A718, A721, A731, A733, A735, A732, A737, A736, FINSEQ_5: 27;

          end;

        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 i st 1 < i & i < j & j <= ( len g) holds (g /. i) <> (g /. j)

        proof

          let i such that

           A740: 1 < i and

           A741: i < j and

           A742: j <= ( len g) and

           A743: (g /. i) = (g /. j);

          

           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);

            then j < ( len g) by A742, XXREAL_0: 1;

            hence contradiction by A711, A740, A741, A743, A744, A745;

          end;

            suppose j = ( len g);

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

          end;

        end;

        

         A747: for i st 1 <= i & i < j & j < ( len g) holds (g /. i) <> (g /. j)

        proof

          let i such that

           A748: 1 <= i and

           A749: i < j and

           A750: j < ( len g) and

           A751: (g /. i) = (g /. j);

          

           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;

        end;

        g is s.c.c.

        proof

          let i, j such that

           A753: (i + 1) < j and

           A754: i > 1 & j < ( len g) or (j + 1) < ( len g);

          

           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);

            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 such that

             A764: [i1, j1] in ( Indices G) and

             A765: (g /. i) = (G * (i1,j1)) and

             A766: [i2, j2] in ( Indices G) and

             A767: (g /. (i + 1)) = (G * (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 G) by A766, MATRIX_0: 32;

            

             A771: 1 <= i2 by A766, MATRIX_0: 32;

            

             A772: i1 <= ( len G) by A764, MATRIX_0: 32;

            

             A773: 1 <= j2 by A766, MATRIX_0: 32;

            

             A774: j1 <= ( width G) by A764, MATRIX_0: 32;

            

             A775: i2 <= ( len G) 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 be Nat such that

             A780: [i19, j19] in ( Indices G) and

             A781: (g /. j) = (G * (i19,j19)) and

             A782: [i29, j29] in ( Indices G) and

             A783: (g /. (j + 1)) = (G * (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 G) by A782, MATRIX_0: 32;

            

             A787: j19 <= ( width G) by A780, MATRIX_0: 32;

            

             A788: 1 <= j29 by A782, MATRIX_0: 32;

            

             A789: 1 <= j19 by A780, MATRIX_0: 32;

            

             A790: i29 <= ( len G) by A782, MATRIX_0: 32;

            

             A791: i19 <= ( len G) by A780, MATRIX_0: 32;

            assume (( LSeg (g,i)) /\ ( LSeg (g,j))) <> {} ;

            then

             A792: ( LSeg (g,i)) meets ( LSeg (g,j)) by XBOOLE_0:def 7;

            

             A793: 1 <= i29 by A782, MATRIX_0: 32;

            now

              per cases by A768, A784;

                suppose

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

                then

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

                now

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

                    suppose j1 = j19;

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

                  end;

                    suppose j1 = (j19 + 1);

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

                  end;

                    suppose (j1 + 1) = j19;

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                then

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

                now

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

                    suppose j1 = j29;

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

                  end;

                    suppose j1 = (j29 + 1);

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

                  end;

                    suppose (j1 + 1) = j29;

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                then

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

                now

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

                    suppose i1 = i19;

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

                  end;

                    suppose i1 = (i19 + 1);

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

                  end;

                    suppose (i1 + 1) = i19;

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                then

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

                now

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

                    suppose i1 = i29;

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

                  end;

                    suppose i1 = (i29 + 1);

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

                  end;

                    suppose (i1 + 1) = i29;

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                then

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

                now

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

                    suppose i2 = i19;

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

                  end;

                    suppose i2 = (i19 + 1);

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

                  end;

                    suppose (i2 + 1) = i19;

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                then

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

                now

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

                    suppose i2 = i29;

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

                  end;

                    suppose i2 = (i29 + 1);

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

                  end;

                    suppose (i2 + 1) = i29;

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                then

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

                now

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

                    suppose j2 = j19;

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

                  end;

                    suppose j2 = (j19 + 1);

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

                  end;

                    suppose (j2 + 1) = j19;

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                then

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

                now

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

                    suppose j2 = j29;

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

                  end;

                    suppose j2 = (j29 + 1);

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

                  end;

                    suppose (j2 + 1) = j29;

                    hence contradiction by A739, A759, A760, A765, A778, A783, A816, A817;

                  end;

                end;

                hence contradiction;

              end;

            end;

            hence contradiction;

          end;

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

            then ( LSeg (g,i)) = {} by TOPREAL1:def 3;

            hence (( LSeg (g,i)) /\ ( LSeg (g,j))) = {} ;

          end;

            suppose

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

            then

            consider i19,j19,i29,j29 be Nat such that

             A819: [i19, j19] in ( Indices G) and

             A820: (g /. j) = (G * (i19,j19)) and

             A821: [i29, j29] in ( Indices G) and

             A822: (g /. (j + 1)) = (G * (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 G) by A821, MATRIX_0: 32;

            

             A826: 1 <= i29 by A821, MATRIX_0: 32;

            

             A827: i19 <= ( len G) by A819, MATRIX_0: 32;

            

             A828: 1 <= j29 by A821, MATRIX_0: 32;

            

             A829: j19 <= ( width G) by A819, MATRIX_0: 32;

            

             A830: i29 <= ( len G) by A821, MATRIX_0: 32;

            

             A831: 1 <= j19 by A819, MATRIX_0: 32;

            assume (( LSeg (g,i)) /\ ( LSeg (g,j))) <> {} ;

            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 such that

             A838: [i1, j1] in ( Indices G) and

             A839: (g /. i) = (G * (i1,j1)) and

             A840: [i2, j2] in ( Indices G) and

             A841: (g /. (i + 1)) = (G * (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 G) by A840, MATRIX_0: 32;

            

             A845: j1 <= ( width G) by A838, MATRIX_0: 32;

            

             A846: 1 <= j2 by A840, MATRIX_0: 32;

            

             A847: 1 <= j1 by A838, MATRIX_0: 32;

            

             A848: i2 <= ( len G) by A840, MATRIX_0: 32;

            

             A849: i1 <= ( len G) 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

              per cases by A842, A823;

                suppose

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

                then

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

                now

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

                    suppose j1 = j19;

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

                  end;

                    suppose j1 = (j19 + 1);

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

                  end;

                    suppose (j1 + 1) = j19;

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                then

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

                now

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

                    suppose j1 = j29;

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

                  end;

                    suppose j1 = (j29 + 1);

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

                  end;

                    suppose (j1 + 1) = j29;

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                then

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

                now

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

                    suppose i1 = i19;

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

                  end;

                    suppose i1 = (i19 + 1);

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

                  end;

                    suppose (i1 + 1) = i19;

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                then

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

                now

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

                    suppose i1 = i29;

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

                  end;

                    suppose i1 = (i29 + 1);

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

                  end;

                    suppose (i1 + 1) = i29;

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                then

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

                now

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

                    suppose i2 = i19;

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

                  end;

                    suppose i2 = (i19 + 1);

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

                  end;

                    suppose (i2 + 1) = i19;

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                then

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

                now

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

                    suppose i2 = i29;

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

                  end;

                    suppose i2 = (i29 + 1);

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

                  end;

                    suppose (i2 + 1) = i29;

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                then

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

                now

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

                    suppose j2 = j19;

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

                  end;

                    suppose j2 = (j19 + 1);

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

                  end;

                    suppose (j2 + 1) = j19;

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                now

                  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;

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

                  end;

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

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

                  end;

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

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

                  end;

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

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

                  end;

                end;

                hence contradiction;

              end;

                suppose

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

                then

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

                now

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

                    suppose j2 = j29;

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

                  end;

                    suppose j2 = (j29 + 1);

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

                  end;

                    suppose (j2 + 1) = j29;

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

                  end;

                end;

                hence contradiction;

              end;

            end;

            hence contradiction;

          end;

        end;

        then

        reconsider g as standard non constant 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;

          assume that

           A877: c in C and

           A878: not c in Lg9;

          reconsider c as Point of ( TOP-REAL 2) by A877;

          consider i 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)),G)) /\ ( left_cell (f,(i + (m -' 1)),G))) by A440, A701, A882, A884, GOBRD13: 29;

          then c in ( right_cell (f,(i + (m -' 1)),G)) by XBOOLE_0:def 4;

          then ( right_cell (f,(i + (m -' 1)),G)) meets C by A877, XBOOLE_0: 3;

          hence contradiction by A440, A701, A882, A884;

        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,G)) meets C by A440, A652, A659;

          then

          consider p be object such that

           A888: p in ( left_cell (f,m,G)) and

           A889: p in C by XBOOLE_0: 3;

          reconsider p as Element of ( TOP-REAL 2) by A888;

          now

            reconsider u = p as Element of ( Euclid 2) by TOPREAL3: 8;

            take p;

            thus p in C by A889;

            

             A890: ( Int ( left_cell (g,1))) c= ( LeftComp g) by A704, GOBOARD9: 21;

            ( Int ( left_cell (g,1,G))) c= ( Int ( left_cell (g,1))) by A705, A704, GOBRD13: 33, TOPS_1: 19;

            then ( Int ( left_cell (g,1,G))) c= ( LeftComp g) by A890;

            then ( Int ( left_cell (f,((m -' 1) + 1),G))) c= ( LeftComp g) by A653, A700, A704, GOBRD13: 32;

            then

             A891: ( Int ( left_cell (f,m,G))) c= ( LeftComp g) by A652, XREAL_1: 235;

            consider r be Real such that

             A892: r > 0 and

             A893: ( Ball (u,r)) c= (( L~ g) ` ) by A876, A886, A889, GOBOARD6: 5;

            reconsider 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,G)) = ( Cl ( Int ( left_cell (f,m,G)))) by A652, A659, A680;

            p in ( Ball (u,r)) by A892, TBSP_1: 11;

            then

             A896: ( Int ( left_cell (f,m,G))) 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;

          end;

          hence thesis by XBOOLE_0: 3;

        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 st 1 <= n holds ((n -' 1) + 2) = (n + 1)

          proof

            let n;

            assume 1 <= n;

            

            hence ((n -' 1) + 2) = ((n + 2) -' 1) by NAT_D: 38

            .= (((n + 1) + 1) - 1) by NAT_D: 37

            .= (n + 1);

          end;

          assume m <> 1;

          then

           A901: 1 < m by A652, XXREAL_0: 1;

          

           A902: for n st 1 <= n & n <= (m -' 1) holds not (f /. n) in ( L~ g)

          proof

            

             A903: 2 <= ( len G) by A2, NAT_1: 12;

            let n such that

             A904: 1 <= n and

             A905: n <= (m -' 1);

            set p = (f /. n);

            

             A906: n <= ( len f) by A700, A905, XXREAL_0: 2;

            then

             A907: p in ( Values G) by A440, A904, JORDAN9: 6;

            assume p in ( L~ g);

            then

            consider j such that

             A908: ((m -' 1) + 1) <= j and

             A909: (j + 1) <= ( len f) and

             A910: p 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: p = (f /. j);

              

               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

              .= p 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;

            end;

              suppose

               A920: p = (f /. (j + 1));

              now

                per cases by A911, XXREAL_0: 1;

                  suppose

                   A921: (j + 1) = k;

                  

                   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

                  .= p 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;

                end;

                  suppose

                   A924: (j + 1) < k;

                  set l = (j + 1);

                  

                   A925: 1 <= l by NAT_1: 11;

                  

                   A926: n < (n + 1) by XREAL_1: 29;

                  

                   A927: (n + 1) < l by A914, XREAL_1: 6;

                  then

                   A928: n <> ( len (F . l)) by A177, A926;

                  

                   A929: n < l by A926, A927, XXREAL_0: 2;

                  then n <= ( len (F . l)) by A177;

                  then

                   A930: n in ( dom (F . l)) by A904, FINSEQ_3: 25;

                  ((F . l) /. n) = ((F . n) /. n) by A566, A904, A929

                  .= p by A710, A566, A904, A906

                  .= ((F . l) /. l) by A566, A920, A924, A925

                  .= ((F . l) /. ( len (F . l))) by A177;

                  hence contradiction by A648, A924, A930, A928, NAT_1: 11;

                end;

              end;

              hence contradiction;

            end;

          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 = (rg /. 1), q = (rg /. 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) <= l by XREAL_1: 6;

            then (m -' 1) < l by NAT_1: 13;

            then

             A936: (m -' 1) <> ( len (F . l)) by A177;

            

             A937: (1 + 1) <= ( len rg) by A703, FINSEQ_5:def 3;

            then ((1 + 1) -' 1) <= (( len rg) -' 1) by NAT_D: 42;

            then

             A938: 1 <= (( len rg) -' 1) by NAT_D: 34;

            

             A939: rg is_sequence_on G by A705, JORDAN9: 5;

            then

            consider p1,p2,q1,q2 be Nat such that

             A940: [p1, p2] in ( Indices G) and

             A941: p = (G * (p1,p2)) and

             A942: [q1, q2] in ( Indices G) and

             A943: q = (G * (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 G) by A940, MATRIX_0: 32;

            

             A947: p1 <= ( len G) by A940, MATRIX_0: 32;

            

             A948: 1 <= p2 by A940, MATRIX_0: 32;

            

             A949: p = (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: q = (g /. (( len g) -' 1)) by A931, FINSEQ_5: 66

            .= (f /. l) by A950, FINSEQ_5: 27;

            1 < ( len rg) by A937, NAT_1: 13;

            then

             A952: ((( len rg) -' 1) + 1) = ( len rg) by XREAL_1: 235;

            

             A953: l = ((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: p = (f /. (l + 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),G)) meets C by A440, A654, A955;

            (m -' 1) <= l by NAT_1: 11;

            then (m -' 1) <= ( len (F . l)) by A177;

            then

             A958: (m -' 1) in ( dom (F . l)) by A956, FINSEQ_3: 25;

             not a in ( L~ g) by A902, A956;

            then

             A959: not a in ( L~ rg) by SPPOL_2: 22;

            

             A960: k = (l + 1) by A953;

            then

             A961: l < k by XREAL_1: 29;

            (( len g) -' 1) <= l by NAT_1: 11;

            then

             A962: 1 <= l by A935, XXREAL_0: 2;

            then

             A963: ( left_cell (f,l,G)) meets C by A440, A710, A960;

            per cases by A944;

              suppose

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

              consider a1,a2,p91,p92 be Nat such that

               A965: [a1, a2] in ( Indices G) and

               A966: a = (G * (a1,a2)) and

               A967: [p91, p92] in ( Indices G) and

               A968: p = (G * (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 thesis

              proof

                per cases by A969;

                  suppose

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

                  

                   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 rg) -' 1) + 2) = (( len g) + 1) by A931, FINSEQ_5:def 3;

                  

                  then

                   A975: (rg /. (( len rg) -' 1)) = (g /. 2) by A974, FINSEQ_5: 66

                  .= (f /. (m + 1)) by A933, A974, FINSEQ_5: 27;

                  

                   A976: ( L~ rg) c= ( L~ f) by A898, SPPOL_2: 22;

                  

                   A977: p = (g /. 1) by A651, A738, A702, FINSEQ_5: 65

                  .= (rg /. ( len g)) by FINSEQ_5: 65

                  .= (rg /. ( len rg)) 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 (rg,(( len rg) -' 1),G)) \ ( L~ rg));

                  

                   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,l,G)) = ( cell (G,p1,p2)) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A964, GOBRD13: 27

                  .= ( front_right_cell ((F . m),(m -' 1),G)) by A440, A949, A955, A956, A940, A941, A965, A966, A979, A983, A981, A973, A980, GOBRD13: 35;

                  then (F . (m + 1)) turns_right ((m -' 1),G) by A514, A901, A963;

                  then

                   A985: f turns_right ((m -' 1),G) by A956, A933, A978, GOBRD13: 43;

                  

                   A986: (p2 + 1) > (a2 + 1) by A983, NAT_1: 13;

                  then

                   A987: [(p1 + 1), p2] in ( Indices G) by A949, A955, A940, A941, A965, A966, A982, A985, GOBRD13:def 6;

                  then

                   A988: (p1 + 1) <= ( len G) by MATRIX_0: 32;

                  (f /. (m + 1)) = (G * ((p1 + 1),p2)) by A949, A955, A933, A940, A941, A965, A966, A986, A982, A985, GOBRD13:def 6;

                  then ( left_cell (rg,(( len rg) -' 1),G)) = ( cell (G,p1,a2)) by A939, A938, A952, A940, A941, A987, A984, A975, A977, GOBRD13: 25;

                  then a in ( left_cell (rg,(( len rg) -' 1),G)) by A945, A946, A966, A970, A979, A983, A988, JORDAN9: 20;

                  then

                   A989: a in rc by A959, XBOOLE_0:def 5;

                  

                   A990: ( LeftComp rg) is_a_component_of (( L~ rg) ` ) by GOBOARD9:def 1;

                  rc c= ( LeftComp rg) by A939, A938, A952, JORDAN9: 27;

                  hence thesis by A654, A660, A955, A956, A959, A989, A976, A990;

                end;

                  suppose

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

                  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,l,G)) = ( cell (G,a1,a2)) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A964, A992, GOBRD13: 28

                  .= ( left_cell (f,(m -' 1),G)) by A440, A654, A949, A955, A956, A965, A966, A967, A968, A991, GOBRD13: 23;

                  hence thesis by A440, A710, A960, A962, A957;

                end;

                  suppose

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

                  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),G)) = ( cell (G,p1,p2)) by A651, A653, A654, A702, A955, A956, A940, A941, A965, A966, A994, FINSEQ_5: 65, GOBRD13: 26

                  .= ( left_cell (f,l,G)) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A964, GOBRD13: 27;

                  hence thesis by A440, A654, A955, A956, A963;

                end;

                  suppose

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

                  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 . l) /. (m -' 1)) = ((F . (m -' 1)) /. (m -' 1)) by A566, A956, NAT_1: 11

                  .= q by A710, A700, A566, A956, A943, A966, A997, A996

                  .= ((F . l) /. l) by A566, A961, A962, A951

                  .= ((F . l) /. ( len (F . l))) by A177;

                  hence thesis by A648, A961, A962, A958, A936;

                end;

              end;

            end;

              suppose

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

              consider a1,a2,p91,p92 be Nat such that

               A999: [a1, a2] in ( Indices G) and

               A1000: a = (G * (a1,a2)) and

               A1001: [p91, p92] in ( Indices G) and

               A1002: p = (G * (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 G) by A999, MATRIX_0: 32;

              

               A1006: 1 <= a1 by A999, MATRIX_0: 32;

              thus thesis

              proof

                per cases by A1003;

                  suppose

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

                  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),G)) = ( cell (G,a1,a2)) by A440, A654, A949, A955, A956, A999, A1000, A1001, A1002, A1007, GOBRD13: 22

                  .= ( left_cell (f,l,G)) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A998, A1009, A1008, GOBRD13: 25;

                  hence thesis by A440, A654, A955, A956, A963;

                end;

                  suppose

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

                  

                   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 rg) -' 1) + 2) = (( len g) + 1) by A931, FINSEQ_5:def 3;

                  

                  then

                   A1014: (rg /. (( len rg) -' 1)) = (g /. 2) by A1013, FINSEQ_5: 66

                  .= (f /. (m + 1)) by A933, A1013, FINSEQ_5: 27;

                  

                   A1015: ( L~ rg) 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: p = (g /. 1) by A651, A738, A702, FINSEQ_5: 65

                  .= (rg /. ( len g)) by FINSEQ_5: 65

                  .= (rg /. ( len rg)) by FINSEQ_5:def 3;

                  set rc = (( left_cell (rg,(( len rg) -' 1),G)) \ ( L~ rg));

                  

                   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,l,G)) = ( cell (G,p1,(p2 -' 1))) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A998, GOBRD13: 25

                  .= ( front_right_cell ((F . m),(m -' 1),G)) by A440, A949, A955, A956, A940, A941, A999, A1000, A1023, A1018, A1017, A1012, A1021, GOBRD13: 37;

                  then (F . (m + 1)) turns_right ((m -' 1),G) by A514, A901, A963;

                  then

                   A1025: f turns_right ((m -' 1),G) by A956, A933, A1016, GOBRD13: 43;

                  

                   A1026: a1 < (a1 + 1) by XREAL_1: 29;

                  then

                   A1027: [p1, (p2 -' 1)] in ( Indices G) 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)) = (G * (p1,(p2 -' 1))) by A949, A955, A933, A940, A941, A999, A1000, A1023, A1026, A1020, A1025, GOBRD13:def 6;

                  then ( left_cell (rg,(( len rg) -' 1),G)) = ( cell (G,a1,(a2 -' 1))) by A939, A938, A952, A940, A941, A1018, A1027, A1024, A1014, A1022, A1019, GOBRD13: 21;

                  then a in ( left_cell (rg,(( len rg) -' 1),G)) by A947, A1000, A1006, A1005, A1023, A1022, A1028, JORDAN9: 20;

                  then

                   A1029: a in rc by A959, XBOOLE_0:def 5;

                  

                   A1030: ( LeftComp rg) is_a_component_of (( L~ rg) ` ) by GOBOARD9:def 1;

                  rc c= ( LeftComp rg) by A939, A938, A952, JORDAN9: 27;

                  hence thesis by A654, A660, A955, A956, A959, A1029, A1015, A1030;

                end;

                  suppose

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

                  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 . l) /. (m -' 1)) = ((F . (m -' 1)) /. (m -' 1)) by A566, A956, NAT_1: 11

                  .= q by A710, A700, A566, A956, A943, A1000, A1033, A1032

                  .= ((F . l) /. l) by A566, A961, A962, A951

                  .= ((F . l) /. ( len (F . l))) by A177;

                  hence thesis by A648, A961, A962, A958, A936;

                end;

                  suppose

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

                  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,l,G)) = ( cell (G,p1,p2)) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A998, GOBRD13: 26

                  .= ( left_cell (f,(m -' 1),G)) by A651, A653, A654, A702, A955, A956, A940, A941, A999, A1000, A1036, A1035, FINSEQ_5: 65, GOBRD13: 27;

                  hence thesis by A440, A710, A960, A962, A957;

                end;

              end;

            end;

              suppose

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

              consider a1,a2,p91,p92 be Nat such that

               A1038: [a1, a2] in ( Indices G) and

               A1039: a = (G * (a1,a2)) and

               A1040: [p91, p92] in ( Indices G) and

               A1041: p = (G * (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 G) by A1038, MATRIX_0: 32;

              thus thesis

              proof

                per cases by A1042;

                  suppose

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

                  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,l,G)) = ( cell (G,q1,(q2 -' 1))) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A1037, GOBRD13: 24

                  .= ( left_cell (f,(m -' 1),G)) by A440, A654, A949, A955, A956, A1038, A1039, A1040, A1041, A1044, A1046, A1045, GOBRD13: 21;

                  hence thesis by A440, A710, A960, A962, A957;

                end;

                  suppose

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

                  then

                   A1048: a2 = p2 by A940, A941, A1040, A1041, GOBOARD1: 5;

                  

                   A1049: (a1 + 1) = p1 by A940, A941, A1040, A1041, A1047, GOBOARD1: 5;

                  ((F . l) /. (m -' 1)) = ((F . (m -' 1)) /. (m -' 1)) by A566, A956, NAT_1: 11

                  .= q by A710, A700, A566, A956, A943, A1037, A1039, A1049, A1048

                  .= ((F . l) /. l) by A566, A961, A962, A951

                  .= ((F . l) /. ( len (F . l))) by A177;

                  hence thesis by A648, A961, A962, A958, A936;

                end;

                  suppose

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

                  

                   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 rg) -' 1) + 2) = (( len g) + 1) by A931, FINSEQ_5:def 3;

                  

                  then

                   A1054: (rg /. (( len rg) -' 1)) = (g /. 2) by A1053, FINSEQ_5: 66

                  .= (f /. (m + 1)) by A933, A1053, FINSEQ_5: 27;

                  

                   A1055: ( L~ rg) c= ( L~ f) by A898, SPPOL_2: 22;

                  set rc = (( left_cell (rg,(( len rg) -' 1),G)) \ ( L~ rg));

                  

                   A1056: ( LeftComp rg) is_a_component_of (( L~ rg) ` ) 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,l,G)) = ( cell (G,q1,q2)) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A1037, GOBRD13: 23

                  .= ( front_right_cell ((F . m),(m -' 1),G)) 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),G) by A514, A901, A963;

                  then

                   A1063: f turns_right ((m -' 1),G) 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 G) by A949, A955, A940, A941, A1038, A1039, A1062, A1063, GOBRD13:def 6;

                  then

                   A1066: (p2 + 1) <= ( width G) by MATRIX_0: 32;

                  (a2 + 1) > p2 by A1062, NAT_1: 13;

                  then

                   A1067: (f /. (m + 1)) = (G * (p1,(p2 + 1))) by A949, A955, A933, A940, A941, A1038, A1039, A1062, A1064, A1063, GOBRD13:def 6;

                  p = (g /. 1) by A651, A738, A702, FINSEQ_5: 65

                  .= (rg /. ( len g)) by FINSEQ_5: 65

                  .= (rg /. ( len rg)) by FINSEQ_5:def 3;

                  then ( left_cell (rg,(( len rg) -' 1),G)) = ( cell (G,p1,p2)) by A939, A938, A952, A940, A941, A1067, A1065, A1054, GOBRD13: 27;

                  then a in ( left_cell (rg,(( len rg) -' 1),G)) by A945, A948, A1039, A1043, A1059, A1062, A1066, JORDAN9: 20;

                  then

                   A1068: a in rc by A959, XBOOLE_0:def 5;

                  rc c= ( LeftComp rg) by A939, A938, A952, JORDAN9: 27;

                  hence thesis by A654, A660, A955, A956, A959, A1068, A1055, A1056;

                end;

                  suppose

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

                  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),G)) = ( cell (G,q1,q2)) by A651, A653, A654, A702, A955, A956, A1037, A1038, A1039, A1040, A1041, A1069, A1070, FINSEQ_5: 65, GOBRD13: 28

                  .= ( left_cell (f,l,G)) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A1037, GOBRD13: 23;

                  hence thesis by A440, A654, A955, A956, A963;

                end;

              end;

            end;

              suppose

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

              consider a1,a2,p91,p92 be Nat such that

               A1072: [a1, a2] in ( Indices G) and

               A1073: a = (G * (a1,a2)) and

               A1074: [p91, p92] in ( Indices G) and

               A1075: p = (G * (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 G) by A1072, MATRIX_0: 32;

              thus thesis

              proof

                per cases by A1076;

                  suppose

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

                  then

                   A1079: (a2 + 1) = p2 by A940, A941, A1074, A1075, GOBOARD1: 5;

                  

                   A1080: a1 = p1 by A940, A941, A1074, A1075, A1078, GOBOARD1: 5;

                  ((F . l) /. (m -' 1)) = ((F . (m -' 1)) /. (m -' 1)) by A566, A956, NAT_1: 11

                  .= q by A710, A700, A566, A956, A943, A1071, A1073, A1080, A1079

                  .= ((F . l) /. l) by A566, A961, A962, A951

                  .= ((F . l) /. ( len (F . l))) by A177;

                  hence thesis by A648, A961, A962, A958, A936;

                end;

                  suppose

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

                  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),G)) = ( cell (G,a1,(a2 -' 1))) by A440, A654, A949, A955, A956, A1072, A1073, A1074, A1075, A1081, GOBRD13: 24

                  .= ( left_cell (f,l,G)) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A1071, A1083, A1082, GOBRD13: 21;

                  hence thesis by A440, A654, A955, A956, A963;

                end;

                  suppose

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

                  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,l,G)) = ( cell (G,q1,q2)) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A1071, GOBRD13: 22

                  .= ( left_cell (f,(m -' 1),G)) by A651, A653, A654, A702, A955, A956, A1071, A1072, A1073, A1074, A1075, A1084, A1086, A1085, FINSEQ_5: 65, GOBRD13: 25;

                  hence thesis by A440, A710, A960, A962, A957;

                end;

                  suppose

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

                  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 rg) -' 1) + 2) = (( len g) + 1) by A931, FINSEQ_5:def 3;

                  

                  then

                   A1091: (rg /. (( len rg) -' 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 (rg,(( len rg) -' 1),G)) \ ( L~ rg));

                  

                   A1096: (p2 + 1) > p2 by NAT_1: 13;

                  

                   A1097: p = (g /. 1) by A651, A738, A702, FINSEQ_5: 65

                  .= (rg /. ( len g)) by FINSEQ_5: 65

                  .= (rg /. ( len rg)) 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~ rg) c= ( L~ f) by A898, SPPOL_2: 22;

                  

                   A1101: a1 = p1 by A940, A941, A1074, A1075, A1087, GOBOARD1: 5;

                  ( left_cell (f,l,G)) = ( cell (G,(q1 -' 1),q2)) by A440, A710, A953, A962, A951, A954, A940, A941, A942, A943, A1071, GOBRD13: 21

                  .= ( front_right_cell ((F . m),(m -' 1),G)) 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),G) by A514, A901, A963;

                  then

                   A1102: f turns_right ((m -' 1),G) by A956, A933, A1099, GOBRD13: 43;

                  

                   A1103: (a2 + 1) > (p2 + 1) by A1088, NAT_1: 13;

                  then

                   A1104: [(p1 -' 1), p2] in ( Indices G) by A949, A955, A940, A941, A1072, A1073, A1096, A1102, GOBRD13:def 6;

                  then

                   A1105: 1 <= (p1 -' 1) by MATRIX_0: 32;

                  (f /. (m + 1)) = (G * ((p1 -' 1),p2)) by A949, A955, A933, A940, A941, A1072, A1073, A1103, A1096, A1102, GOBRD13:def 6;

                  then ( left_cell (rg,(( len rg) -' 1),G)) = ( cell (G,(p1 -' 1),p2)) by A939, A938, A952, A940, A941, A1104, A1091, A1097, A1092, GOBRD13: 23;

                  then a in ( left_cell (rg,(( len rg) -' 1),G)) by A947, A948, A1073, A1077, A1101, A1088, A1105, A1092, JORDAN9: 20;

                  then

                   A1106: a in rc by A959, XBOOLE_0:def 5;

                  

                   A1107: ( LeftComp rg) is_a_component_of (( L~ rg) ` ) by GOBOARD9:def 1;

                  rc c= ( LeftComp rg) by A939, A938, A952, JORDAN9: 27;

                  hence thesis by A654, A660, A955, A956, A959, A1106, A1100, A1107;

                end;

              end;

            end;

          end;

          then C meets ( RightComp g) by GOBOARD9: 23;

          hence contradiction by A876, A885, A899, A887, JORDAN9: 1, SPRECT_4: 6;

        end;

        

        then

         A1108: g = (f /^ 0 ) by XREAL_1: 232

        .= f by FINSEQ_5: 28;

        then

        reconsider f as standard non constant special_circular_sequence;

        (F . ( 0 + 1)) = <*(G * (XS,YS))*> by A156;

        

        then

         A1109: (G * (XS,YS)) = ((F . 1) /. 1) by FINSEQ_4: 16

        .= (f /. 1) by A647, A566;

        (F . (1 + 1)) = <*(G * (XS,YS)), (G * ((XS -' 1),YS))*> by A156;

        

        then

         A1110: (G * ((XS -' 1),YS)) = ((F . 2) /. 2) by FINSEQ_4: 17

        .= (f /. 2) by A657, A566;

        

         A1111: 2 < XS 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: ((XS -' 1) + 1) = XS by A1111, XREAL_1: 235, XXREAL_0: 2;

          set W = { B where B be Subset of ( TOP-REAL 2) : B is_inside_component_of C };

          

           A1115: ( Int ( right_cell (f,1,G))) c= ( right_cell (f,1,G)) by TOPS_1: 16;

          

           A1116: ( BDD C) = ( union W) by JORDAN2C:def 4;

          

           A1117: ( Int ( right_cell (f,1,G))) <> {} by A653, A656, JORDAN9: 9;

          

           A1118: [(XS -' 1), YS] in ( Indices G) by A1, JORDAN11: 9;

          ( cell (G,(XS -' 1),YS)) c= ( BDD C) by A1, JORDAN11: 6;

          then ( right_cell (f,1,G)) c= ( BDD C) by A5, A440, A656, A1109, A1110, A1114, A1118, GOBRD13: 26;

          then

           A1119: ( Int ( right_cell (f,1,G))) c= ( BDD C) by A1115;

          ( Int ( right_cell (f,1,G))) c= ( RightComp f) by A653, A656, JORDAN1H: 25;

          then ( BDD C) meets ( RightComp f) by A1119, A1117, XBOOLE_1: 68;

          then

          consider e be set such that

           A1120: e in W and

           A1121: ( RightComp f) meets e by A1116, ZFMISC_1: 80;

          consider B be 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 thesis by A1113, JORDAN1H: 39, JORDAN1H: 41;

        end;

        then

        reconsider f as clockwise_oriented standard non constant special_circular_sequence;

        take f;

        thus f is_sequence_on G by A440;

        thus (f /. 1) = (G * (XS,YS)) by A1109;

        thus (f /. 2) = (G * ((XS -' 1),YS)) by A1110;

        let m such that

         A1125: 1 <= m and

         A1126: (m + 2) <= ( len f);

        

         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,G)) = ( front_right_cell (f,m,G)) 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,G)) = ( front_left_cell (f,m,G)) by A653, A1125, A1130, A1129, GOBRD13: 42;

        hereby

          assume that

           A1135: ( front_right_cell (f,m,G)) misses C and

           A1136: ( front_left_cell (f,m,G)) misses C;

          (F . ((m + 1) + 1)) turns_left (m,G) by A514, A1133, A1132, A1131, A1134, A1135, A1136;

          hence f turns_left (m,G) by A1125, A1126, A1127, GOBRD13: 44;

        end;

        hereby

          assume that

           A1137: ( front_right_cell (f,m,G)) misses C and

           A1138: ( front_left_cell (f,m,G)) meets C;

          (F . ((m + 1) + 1)) goes_straight (m,G) by A514, A1133, A1132, A1131, A1134, A1137, A1138;

          hence f goes_straight (m,G) by A1125, A1126, A1127, GOBRD13: 45;

        end;

        assume ( front_right_cell (f,m,G)) meets C;

        then (F . ((m + 1) + 1)) turns_right (m,G) by A514, A1133, A1132, A1131;

        hence thesis by A1125, A1126, A1127, GOBRD13: 43;

      end;

      uniqueness

      proof

        let f1,f2 be clockwise_oriented standard non constant special_circular_sequence such that

         A1139: f1 is_sequence_on ( Gauge (C,n)) and

         A1140: (f1 /. 1) = (( Gauge (C,n)) * (( X-SpanStart (C,n)),( Y-SpanStart (C,n)))) and

         A1141: (f1 /. 2) = (( Gauge (C,n)) * ((( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n)))) and

         A1142: for k st 1 <= k & (k + 2) <= ( len f1) holds (( front_right_cell (f1,k,( Gauge (C,n)))) misses C & ( front_left_cell (f1,k,( Gauge (C,n)))) misses C implies f1 turns_left (k,( Gauge (C,n)))) & (( front_right_cell (f1,k,( Gauge (C,n)))) misses C & ( front_left_cell (f1,k,( Gauge (C,n)))) meets C implies f1 goes_straight (k,( Gauge (C,n)))) & (( front_right_cell (f1,k,( Gauge (C,n)))) meets C implies f1 turns_right (k,( Gauge (C,n)))) and

         A1143: f2 is_sequence_on ( Gauge (C,n)) and

         A1144: (f2 /. 1) = (( Gauge (C,n)) * (( X-SpanStart (C,n)),( Y-SpanStart (C,n)))) and

         A1145: (f2 /. 2) = (( Gauge (C,n)) * ((( X-SpanStart (C,n)) -' 1),( Y-SpanStart (C,n)))) and

         A1146: for k st 1 <= k & (k + 2) <= ( len f2) holds (( front_right_cell (f2,k,( Gauge (C,n)))) misses C & ( front_left_cell (f2,k,( Gauge (C,n)))) misses C implies f2 turns_left (k,( Gauge (C,n)))) & (( front_right_cell (f2,k,( Gauge (C,n)))) misses C & ( front_left_cell (f2,k,( Gauge (C,n)))) meets C implies f2 goes_straight (k,( Gauge (C,n)))) & (( front_right_cell (f2,k,( Gauge (C,n)))) meets C implies f2 turns_right (k,( Gauge (C,n))));

        defpred P[ Nat] means (f1 | $1) = (f2 | $1);

        

         A1147: for k st P[k] holds P[(k + 1)]

        proof

          

           A1148: ( len f2) > 4 by GOBOARD7: 34;

          

           A1149: ( len f1) > 4 by GOBOARD7: 34;

          let k such that

           A1151: (f1 | k) = (f2 | k);

          per cases by NAT_1: 25;

            suppose

             W: k = 0 ;

            1 <= ( len f1) & 1 <= ( len f2) by A1148, A1149, XXREAL_0: 2;

            then 1 in ( dom f1) & 1 in ( dom f2) by FINSEQ_3: 25;

            then

             W2: <*(f1 . 1)*> = <*(f1 /. 1)*> & <*(f2 . 1)*> = <*(f2 /. 1)*> by PARTFUN1:def 6;

            

             W1: <*(f1 . 1)*> = (f1 | 1) & <*(f2 . 1)*> = (f2 | 1) by FINSEQ_5: 20;

             <*(f1 . 1)*> = <*(f2 . 1)*> by A1140, A1144, W2;

            then (f1 | 1) = (f2 | 1) by W1;

            hence thesis by W;

          end;

            suppose

             A1152: k = 1;

            (f1 | 2) = <*(f1 /. 1), (f1 /. 2)*> by A1149, FINSEQ_5: 81, XXREAL_0: 2;

            hence thesis by A1140, A1141, A1144, A1145, A1148, A1152, FINSEQ_5: 81, XXREAL_0: 2;

          end;

            suppose

             A1153: k > 1;

            

             A1154: (f2 /. 1) = (f2 /. ( len f2)) by FINSEQ_6:def 1;

            

             A1155: (f1 /. 1) = (f1 /. ( len f1)) by FINSEQ_6:def 1;

            now

              per cases ;

                suppose

                 A1156: ( len f1) > k;

                set m = (k -' 1);

                

                 A1157: 1 <= m by A1153, NAT_D: 49;

                then

                 A1158: (m + 1) = k by NAT_D: 43;

                then

                 A1159: ( front_right_cell (f1,m,( Gauge (C,n)))) = ( front_right_cell ((f1 | k),m,( Gauge (C,n)))) by A1139, A1156, A1157, GOBRD13: 42;

                

                 A1160: (k + 1) <= ( len f1) by A1156, NAT_1: 13;

                 A1161:

                now

                  

                   A1162: 1 < ( len f2) by GOBOARD7: 34, XXREAL_0: 2;

                  assume

                   A1163: ( len f2) <= k;

                  then

                   A1164: f2 = (f2 | k) by FINSEQ_1: 58;

                  then

                   A1165: 1 in ( dom (f2 | k)) by FINSEQ_5: 6;

                  ( len f2) in ( dom (f2 | k)) by A1164, FINSEQ_5: 6;

                  then

                   A1166: ((f1 | k) /. ( len f2)) = (f1 /. ( len f2)) by A1151, FINSEQ_4: 70;

                  ( len f2) <= ( len f1) by A1151, A1164, FINSEQ_5: 16;

                  hence contradiction by A1151, A1155, A1154, A1156, A1163, A1164, A1165, A1166, A1162, FINSEQ_4: 70, GOBOARD7: 38;

                end;

                then

                 A1167: (k + 1) <= ( len f2) by NAT_1: 13;

                

                 A1168: ( front_left_cell (f2,m,( Gauge (C,n)))) = ( front_left_cell ((f2 | k),m,( Gauge (C,n)))) by A1143, A1157, A1158, A1161, GOBRD13: 42;

                

                 A1169: ( front_right_cell (f2,m,( Gauge (C,n)))) = ( front_right_cell ((f2 | k),m,( Gauge (C,n)))) by A1143, A1157, A1158, A1161, GOBRD13: 42;

                

                 A1170: (m + (1 + 1)) = (k + 1) by A1158;

                

                 A1171: ( front_left_cell (f1,m,( Gauge (C,n)))) = ( front_left_cell ((f1 | k),m,( Gauge (C,n)))) by A1139, A1156, A1157, A1158, GOBRD13: 42;

                now

                  per cases ;

                    suppose

                     A1172: ( front_right_cell (f1,m,( Gauge (C,n)))) misses C & ( front_left_cell (f1,m,( Gauge (C,n)))) misses C;

                    then

                     A1173: f1 turns_left (m,( Gauge (C,n))) by A1142, A1157, A1160, A1170;

                    f2 turns_left (m,( Gauge (C,n))) by A1146, A1151, A1157, A1167, A1159, A1171, A1169, A1168, A1170, A1172;

                    hence thesis by A1143, A1151, A1153, A1167, A1160, A1173, GOBRD13: 47;

                  end;

                    suppose

                     A1174: ( front_right_cell (f1,m,( Gauge (C,n)))) misses C & ( front_left_cell (f1,m,( Gauge (C,n)))) meets C;

                    then

                     A1175: f1 goes_straight (m,( Gauge (C,n))) by A1142, A1157, A1160, A1170;

                    f2 goes_straight (m,( Gauge (C,n))) by A1146, A1151, A1157, A1167, A1159, A1171, A1169, A1168, A1170, A1174;

                    hence thesis by A1143, A1151, A1153, A1167, A1160, A1175, GOBRD13: 48;

                  end;

                    suppose

                     A1176: ( front_right_cell (f1,m,( Gauge (C,n)))) meets C;

                    then

                     A1177: f1 turns_right (m,( Gauge (C,n))) by A1142, A1157, A1160, A1170;

                    f2 turns_right (m,( Gauge (C,n))) by A1146, A1151, A1157, A1167, A1159, A1169, A1170, A1176;

                    hence thesis by A1143, A1151, A1153, A1167, A1160, A1177, GOBRD13: 46;

                  end;

                end;

                hence thesis;

              end;

                suppose

                 A1178: k >= ( len f1);

                

                 A1179: 1 < ( len f1) by GOBOARD7: 34, XXREAL_0: 2;

                

                 A1180: f1 = (f1 | k) by A1178, FINSEQ_1: 58;

                then

                 A1181: 1 in ( dom (f1 | k)) by FINSEQ_5: 6;

                ( len f1) in ( dom (f1 | k)) by A1180, FINSEQ_5: 6;

                then

                 A1182: ((f2 | k) /. ( len f1)) = (f2 /. ( len f1)) by A1151, FINSEQ_4: 70;

                ( len f1) <= ( len f2) by A1151, A1180, FINSEQ_5: 16;

                then ( len f2) = ( len f1) by A1151, A1155, A1154, A1180, A1181, A1182, A1179, FINSEQ_4: 70, GOBOARD7: 38;

                hence thesis by A1151, A1178, A1180, FINSEQ_1: 58;

              end;

            end;

            hence thesis;

          end;

        end;

        

         A1183: P[ 0 ];

        for k holds P[k] from NAT_1:sch 2( A1183, A1147);

        hence thesis by JORDAN9: 2;

      end;

    end