goboard4.miz



    begin

    reserve p,p1,p2,q1,q2 for Point of ( TOP-REAL 2),

P1,P2 for Subset of ( TOP-REAL 2),

f,f1,f2,g1,g2 for FinSequence of ( TOP-REAL 2),

n,m,i,j,k for Nat,

G,G1 for Go-board,

x,y for set;

    theorem :: GOBOARD4:1

    

     Th1: for G, f1, f2 st 1 <= ( len f1) & 1 <= ( len f2) & f1 is_sequence_on G & f2 is_sequence_on G & (f1 /. 1) in ( rng ( Line (G,1))) & (f1 /. ( len f1)) in ( rng ( Line (G,( len G)))) & (f2 /. 1) in ( rng ( Col (G,1))) & (f2 /. ( len f2)) in ( rng ( Col (G,( width G)))) holds ( rng f1) meets ( rng f2)

    proof

      defpred P[ Nat] means for G1, g1, g2 st $1 = ( width G1) & $1 > 0 & 1 <= ( len g1) & 1 <= ( len g2) & g1 is_sequence_on G1 & g2 is_sequence_on G1 & (g1 /. 1) in ( rng ( Line (G1,1))) & (g1 /. ( len g1)) in ( rng ( Line (G1,( len G1)))) & (g2 /. 1) in ( rng ( Col (G1,1))) & (g2 /. ( len g2)) in ( rng ( Col (G1,( width G1)))) holds (( rng g1) /\ ( rng g2)) <> {} ;

      let G, f1, f2;

      

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

      proof

        let k such that

         A2: P[k];

        let G1, g1, g2 such that

         A3: (k + 1) = ( width G1) and (k + 1) > 0 and

         A4: 1 <= ( len g1) and

         A5: 1 <= ( len g2) and

         A6: g1 is_sequence_on G1 and

         A7: g2 is_sequence_on G1 and

         A8: (g1 /. 1) in ( rng ( Line (G1,1))) and

         A9: (g1 /. ( len g1)) in ( rng ( Line (G1,( len G1)))) and

         A10: (g2 /. 1) in ( rng ( Col (G1,1))) and

         A11: (g2 /. ( len g2)) in ( rng ( Col (G1,( width G1))));

        defpred P[ Nat] means $1 in ( dom g2) & (g2 /. $1) in ( rng ( Col (G1,( width G1))));

        

         A12: ex m be Nat st P[m] by A5, A11, FINSEQ_3: 25;

        consider m be Nat such that

         A13: P[m] & for i be Nat st P[i] holds m <= i from NAT_1:sch 5( A12);

        reconsider m as Nat;

        set g = (g2 | m);

        

         A14: (g /. 1) in ( rng ( Col (G1,1))) by A10, A13, FINSEQ_4: 92;

        

         A15: g is_sequence_on G1 by A7, GOBOARD1: 22;

        

         A16: m <= ( len g2) by A13, FINSEQ_3: 25;

        then

         A17: ( len g) = m by FINSEQ_1: 59;

        

         A18: ( rng g) c= ( rng g2)

        proof

          let x be object;

          assume x in ( rng g);

          then

          consider n be Element of NAT such that

           A19: n in ( dom g) and

           A20: x = (g /. n) by PARTFUN2: 2;

          

           A21: n in ( Seg m) by A17, A19, FINSEQ_1:def 3;

          then

           A22: n in ( dom g2) by A13, FINSEQ_4: 71;

          x = (g2 /. n) by A13, A20, A21, FINSEQ_4: 71;

          hence thesis by A22, PARTFUN2: 2;

        end;

        reconsider L1 = ( Line (G1,1)), Ll = ( Line (G1,( len G1))) as FinSequence of ( TOP-REAL 2);

        

         A23: ( dom g2) = ( Seg ( len g2)) by FINSEQ_1:def 3;

        

         A24: ( dom g) = ( Seg ( len g)) by FINSEQ_1:def 3;

         0 <> ( len G1) by MATRIX_0:def 10;

        then

         A25: ( 0 + 1) <= ( len G1) by NAT_1: 14;

        then

         A26: 1 in ( dom G1) by FINSEQ_3: 25;

        

         A27: ( len G1) in ( dom G1) by A25, FINSEQ_3: 25;

        

         A28: (g /. ( len g)) in ( rng ( Col (G1,( width G1)))) by A13, FINSEQ_4: 93;

        defpred P[ Nat] means $1 in ( dom G1) & (( rng g) /\ ( rng ( Line (G1,$1)))) <> {} ;

        

         A29: for n be Nat st P[n] holds n <= ( len G1) by FINSEQ_3: 25;

         0 <> ( width G1) by MATRIX_0:def 10;

        then

         A30: ( 0 + 1) <= ( width G1) by NAT_1: 14;

        then

         A31: 1 in ( Seg ( width G1)) by FINSEQ_1: 1;

        

         A32: 1 <= ( len g) by A13, GOBOARD1: 22;

        then

         A33: 1 in ( dom g) by FINSEQ_3: 25;

        

         A34: ex n be Nat st P[n]

        proof

          m in ( dom g2) implies (g2 /. 1) = ((g2 | m) /. 1) by FINSEQ_4: 92;

          then

          consider i be Nat such that

           A35: i in ( dom ( Col (G1,1))) and

           A36: (g /. 1) = (( Col (G1,1)) . i) by A10, A13, FINSEQ_2: 10;

          reconsider i as Nat;

          take i;

          i in ( Seg ( len ( Col (G1,1)))) by A35, FINSEQ_1:def 3;

          then i in ( Seg ( len G1)) by MATRIX_0:def 8;

          hence i in ( dom G1) by FINSEQ_1:def 3;

          then

           A37: (g /. 1) = (( Line (G1,i)) . 1) by A31, A36, MATRIX_0: 42;

          

           A38: (g /. 1) in ( rng g) by A33, PARTFUN2: 2;

          ( len ( Line (G1,i))) = ( width G1) by MATRIX_0:def 7;

          then ( dom ( Line (G1,i))) = ( Seg ( width G1)) by FINSEQ_1:def 3;

          then (g /. 1) in ( rng ( Line (G1,i))) by A31, A37, FUNCT_1:def 3;

          hence thesis by A38, XBOOLE_0:def 4;

        end;

        consider mi be Nat such that

         A39: P[mi] & for n be Nat st P[n] holds mi <= n from NAT_1:sch 5( A34);

        

         A40: ex n be Nat st P[n] by A34;

        consider ma be Nat such that

         A41: P[ma] & for n be Nat st P[n] holds n <= ma from NAT_1:sch 6( A29, A40);

        reconsider mi, ma as Nat;

        

         A42: 1 <= mi by A39, FINSEQ_3: 25;

        reconsider Lmi = ( Line (G1,mi)) as FinSequence of ( TOP-REAL 2);

        defpred P[ Nat] means $1 in ( dom g1) & (g1 /. $1) in ( rng ( Line (G1,mi)));

        

         A43: for n be Nat st P[n] holds n <= ( len g1) by FINSEQ_3: 25;

        

         A44: mi <= ( len G1) by A39, FINSEQ_3: 25;

        then ex n st P[n] by A4, A6, A8, A9, A42, GOBOARD1: 29;

        then

         A45: ex n be Nat st P[n];

        consider ma1 be Nat such that

         A46: P[ma1] & for n be Nat st P[n] holds n <= ma1 from NAT_1:sch 6( A43, A45);

        

         A47: ma <= ( len G1) by A41, FINSEQ_3: 25;

        1 <= mi by A39, FINSEQ_3: 25;

        then

        reconsider l1 = (mi - 1), l2 = (( len G1) - ma) as Element of NAT by A47, INT_1: 5;

        

         A48: ma <= ( len G1) by A41, FINSEQ_3: 25;

        reconsider ma1 as Nat;

        consider k1 be Element of NAT such that

         A49: k1 in ( dom Lmi) and

         A50: (g1 /. ma1) = (Lmi /. k1) by A46, PARTFUN2: 2;

        ( Seg ( len Lmi)) = ( dom Lmi) by FINSEQ_1:def 3;

        then

         A51: k1 in ( Seg ( width G1)) by A49, MATRIX_0:def 7;

        

         A52: ( dom G1) = ( Seg ( len G1)) by FINSEQ_1:def 3;

        

         A53: mi = ma implies (( rng g1) /\ ( rng g2)) <> {}

        proof

          consider n such that

           A54: n in ( dom g1) and

           A55: (g1 /. n) in ( rng ( Line (G1,mi))) by A4, A6, A8, A9, A42, A44, GOBOARD1: 29;

          consider i be Element of NAT such that

           A56: i in ( dom ( Line (G1,mi))) and

           A57: (g1 /. n) = (Lmi /. i) by A55, PARTFUN2: 2;

          

           A58: 1 <= i by A56, FINSEQ_3: 25;

          

           A59: ( len ( Line (G1,mi))) = ( width G1) by MATRIX_0:def 7;

          then i <= ( width G1) by A56, FINSEQ_3: 25;

          then

          consider m such that

           A60: m in ( dom g) and

           A61: (g /. m) in ( rng ( Col (G1,i))) by A32, A15, A14, A28, A58, GOBOARD1: 33;

          

           A62: (g /. m) in ( rng g) by A60, PARTFUN2: 2;

          reconsider Ci = ( Col (G1,i)) as FinSequence of ( TOP-REAL 2);

          

           A63: ( len ( Col (G1,i))) = ( len G1) by MATRIX_0:def 8;

          

          then

           A64: ( dom ( Col (G1,i))) = ( Seg ( len G1)) by FINSEQ_1:def 3

          .= ( dom G1) by FINSEQ_1:def 3;

          assume

           A65: mi = ma;

          

           A66: ( dom ( Line (G1,mi))) = ( Seg ( len ( Line (G1,mi)))) by FINSEQ_1:def 3;

          consider j be Element of NAT such that

           A67: j in ( dom Ci) and

           A68: (g /. m) = (Ci /. j) by A61, PARTFUN2: 2;

          reconsider Lj = ( Line (G1,j)) as FinSequence of ( TOP-REAL 2);

          ( len ( Line (G1,mi))) = ( width G1) by MATRIX_0:def 7

          .= ( len Lj) by MATRIX_0:def 7;

          then

           A69: ( dom ( Line (G1,mi))) = ( dom Lj) by A66, FINSEQ_1:def 3;

          

           A70: (g /. m) = (Ci . j) by A67, A68, PARTFUN1:def 6

          .= (Lj . i) by A56, A66, A59, A64, A67, MATRIX_0: 42

          .= (Lj /. i) by A56, A69, PARTFUN1:def 6;

          ( len Lj) = ( width G1) by MATRIX_0:def 7;

          then i in ( dom Lj) by A56, A66, A59, FINSEQ_1:def 3;

          then (g /. m) in ( rng Lj) by A70, PARTFUN2: 2;

          then

           A71: ( dom Ci) = ( Seg ( len Ci)) & (( rng g) /\ ( rng ( Line (G1,j)))) <> {} by A62, FINSEQ_1:def 3, XBOOLE_0:def 4;

           A72:

          now

            assume j <> mi;

            then j < mi or j > mi by XXREAL_0: 1;

            hence contradiction by A39, A52, A41, A65, A63, A67, A71;

          end;

          (g1 /. n) in ( rng g1) by A54, PARTFUN2: 2;

          hence thesis by A18, A57, A62, A70, A72, XBOOLE_0:def 4;

        end;

        

         A73: ( width G1) in ( Seg ( width G1)) by A30, FINSEQ_1: 1;

        deffunc F( Nat) = (G1 * ($1,k1));

        reconsider Ck1 = ( Col (G1,k1)) as FinSequence of ( TOP-REAL 2);

        consider h1 be FinSequence of ( TOP-REAL 2) such that

         A74: ( len h1) = l1 & for n be Nat st n in ( dom h1) holds (h1 /. n) = F(n) from FINSEQ_4:sch 2;

        

         A75: ( dom g1) = ( Seg ( len g1)) by FINSEQ_1:def 3;

        now

          per cases ;

            suppose

             A76: k = 0 ;

            reconsider c1 = ( Col (G1,1)) as FinSequence of ( TOP-REAL 2);

            consider x be Element of NAT such that

             A77: x in ( dom c1) and

             A78: (g2 /. 1) = (c1 /. x) by A10, PARTFUN2: 2;

            reconsider lx = ( Line (G1,x)) as FinSequence of ( TOP-REAL 2);

            

             A79: 1 <= x by A77, FINSEQ_3: 25;

            

             A80: ( len c1) = ( len G1) by MATRIX_0:def 8;

            then x <= ( len G1) by A77, FINSEQ_3: 25;

            then

            consider m such that

             A81: m in ( dom g1) and

             A82: (g1 /. m) in ( rng lx) by A4, A6, A8, A9, A79, GOBOARD1: 29;

            

             A83: (g1 /. m) in ( rng g1) by A81, PARTFUN2: 2;

            ( Seg ( len c1)) = ( dom c1) by FINSEQ_1:def 3;

            then

             A84: x in ( dom G1) by A77, A80, FINSEQ_1:def 3;

            

             A85: (c1 /. x) = (c1 . x) by A77, PARTFUN1:def 6;

            consider y be Element of NAT such that

             A86: y in ( dom lx) and

             A87: (lx /. y) = (g1 /. m) by A82, PARTFUN2: 2;

            ( Seg ( len lx)) = ( dom lx) & ( len lx) = ( width G1) by FINSEQ_1:def 3, MATRIX_0:def 7;

            then

             A88: y = 1 by A3, A76, A86, FINSEQ_1: 2, TARSKI:def 1;

             0 <> ( width G1) by MATRIX_0:def 10;

            then ( 0 + 1) <= ( width G1) by NAT_1: 14;

            then

             A89: 1 in ( Seg ( width G1)) by FINSEQ_1: 1;

            1 in ( dom g2) by A5, FINSEQ_3: 25;

            then

             A90: (g2 /. 1) in ( rng g2) by PARTFUN2: 2;

            (lx /. y) = (lx . y) by A86, PARTFUN1:def 6;

            then (g1 /. m) = (g2 /. 1) by A78, A89, A84, A87, A85, A88, MATRIX_0: 42;

            hence thesis by A83, A90, XBOOLE_0:def 4;

          end;

            suppose

             A91: k <> 0 ;

            then

             A92: 0 < k;

            then

             A93: ( width G1) > (1 + 0 ) by A3, XREAL_1: 8;

            then

             A94: ( width G1) in ( Seg ( width G1)) by FINSEQ_1: 1;

            now

              per cases ;

                suppose mi = ma;

                hence thesis by A53;

              end;

                suppose

                 A95: mi <> ma;

                1 <= ma1 by A46, FINSEQ_3: 25;

                then

                reconsider w = (ma1 - 1) as Element of NAT by INT_1: 5;

                reconsider Lma = ( Line (G1,ma)) as FinSequence of ( TOP-REAL 2);

                

                 A96: ( Indices G1) = [:( dom G1), ( Seg ( width G1)):] by MATRIX_0:def 4;

                 A97:

                now

                  let n;

                  

                   A98: l1 <= mi by XREAL_1: 43;

                  assume

                   A99: n in ( dom h1);

                  then

                   A100: 1 <= n by FINSEQ_3: 25;

                  n <= l1 by A74, A99, FINSEQ_3: 25;

                  then

                   A101: n <= mi by A98, XXREAL_0: 2;

                  mi <= ( len G1) by A39, FINSEQ_3: 25;

                  then n <= ( len G1) by A101, XXREAL_0: 2;

                  hence n in ( dom G1) by A100, FINSEQ_3: 25;

                end;

                 A102:

                now

                  let n;

                  assume that

                   A103: n in ( dom h1) and

                   A104: (n + 1) in ( dom h1);

                  (n + 1) in ( dom G1) by A97, A104;

                  then

                   A105: [(n + 1), k1] in ( Indices G1) by A51, A96, ZFMISC_1: 87;

                  let i1,i2,j1,j2 be Nat;

                  assume that

                   A106: [i1, i2] in ( Indices G1) and

                   A107: [j1, j2] in ( Indices G1) and

                   A108: (h1 /. n) = (G1 * (i1,i2)) and

                   A109: (h1 /. (n + 1)) = (G1 * (j1,j2));

                  (h1 /. (n + 1)) = (G1 * ((n + 1),k1)) by A74, A104;

                  then

                   A110: j1 = (n + 1) & j2 = k1 by A105, A107, A109, GOBOARD1: 5;

                  n in ( dom G1) by A97, A103;

                  then

                   A111: [n, k1] in ( Indices G1) by A51, A96, ZFMISC_1: 87;

                  (h1 /. n) = (G1 * (n,k1)) by A74, A103;

                  then i1 = n & i2 = k1 by A111, A106, A108, GOBOARD1: 5;

                  

                  hence ( |.(i1 - j1).| + |.(i2 - j2).|) = ( |.((n - n) + ( - 1)).| + 0 ) by A110, ABSVALUE: 2

                  .= |.1.| by COMPLEX1: 52

                  .= 1 by ABSVALUE:def 1;

                end;

                

                 A112: (( rng h1) /\ ( rng g)) = {}

                proof

                  set x = the Element of (( rng h1) /\ ( rng g));

                  assume

                   A113: not thesis;

                  then x in ( rng h1) by XBOOLE_0:def 4;

                  then

                  consider n1 be Element of NAT such that

                   A114: n1 in ( dom h1) and

                   A115: x = (h1 /. n1) by PARTFUN2: 2;

                  

                   A116: n1 <= l1 by A74, A114, FINSEQ_3: 25;

                  n1 in ( dom G1) by A97, A114;

                  then

                   A117: [n1, k1] in ( Indices G1) by A51, A96, ZFMISC_1: 87;

                  x in ( rng g) by A113, XBOOLE_0:def 4;

                  then

                  consider n2 be Element of NAT such that

                   A118: n2 in ( dom g) and

                   A119: x = (g /. n2) by PARTFUN2: 2;

                  

                   A120: (g /. n2) in ( rng g) by A118, PARTFUN2: 2;

                  consider i1,i2 be Nat such that

                   A121: [i1, i2] in ( Indices G1) and

                   A122: (g /. n2) = (G1 * (i1,i2)) by A15, A118, GOBOARD1:def 9;

                  reconsider L = ( Line (G1,i1)) as FinSequence of ( TOP-REAL 2);

                  

                   A123: i2 in ( Seg ( width G1)) by A96, A121, ZFMISC_1: 87;

                  

                   A124: ( Seg ( len L)) = ( dom L) & ( len L) = ( width G1) by FINSEQ_1:def 3, MATRIX_0:def 7;

                  then (L /. i2) = (L . i2) by A123, PARTFUN1:def 6;

                  then (g /. n2) = (L /. i2) by A122, A123, MATRIX_0:def 7;

                  then (g /. n2) in ( rng L) by A123, A124, PARTFUN2: 2;

                  then

                   A125: (( rng g) /\ ( rng L)) <> {} by A120, XBOOLE_0:def 4;

                  i1 in ( dom G1) by A96, A121, ZFMISC_1: 87;

                  then

                   A126: mi <= i1 by A39, A125;

                  x = (G1 * (n1,k1)) by A74, A114, A115;

                  then i1 = n1 by A119, A121, A122, A117, GOBOARD1: 5;

                  then mi <= (mi - 1) by A116, A126, XXREAL_0: 2;

                  hence contradiction by XREAL_1: 44;

                end;

                defpred P[ Nat] means $1 in ( dom g1) & ma1 < $1 & (g1 /. $1) in ( rng ( Line (G1,ma)));

                

                 A127: mi <= ma by A39, A41;

                then

                 A128: mi < ma by A95, XXREAL_0: 1;

                then ex n st P[n] by A6, A9, A39, A48, A46, GOBOARD1: 37;

                then

                 A129: ex n be Nat st P[n];

                consider mi1 be Nat such that

                 A130: P[mi1] & for n be Nat st P[n] holds mi1 <= n from NAT_1:sch 5( A129);

                consider k2 be Element of NAT such that

                 A131: k2 in ( dom Lma) and

                 A132: (g1 /. mi1) = (Lma /. k2) by A130, PARTFUN2: 2;

                deffunc F( Nat) = (G1 * ((ma + $1),k2));

                consider h2 be FinSequence of ( TOP-REAL 2) such that

                 A133: ( len h2) = l2 & for n be Nat st n in ( dom h2) holds (h2 /. n) = F(n) from FINSEQ_4:sch 2;

                reconsider Ck2 = ( Col (G1,k2)) as FinSequence of ( TOP-REAL 2);

                ( dom Lma) = ( Seg ( len Lma)) by FINSEQ_1:def 3;

                then

                 A134: k2 in ( Seg ( width G1)) by A131, MATRIX_0:def 7;

                 A135:

                now

                  let n;

                  

                   A136: n <= (n + ma) by NAT_1: 11;

                  assume

                   A137: n in ( dom h2);

                  then n <= l2 by A133, FINSEQ_3: 25;

                  then

                   A138: (ma + n) <= (ma + l2) by XREAL_1: 7;

                  1 <= n by A137, FINSEQ_3: 25;

                  then 1 <= (n + ma) by A136, XXREAL_0: 2;

                  hence (ma + n) in ( dom G1) by A138, FINSEQ_3: 25;

                end;

                 A139:

                now

                  let n;

                  assume

                   A140: n in ( dom h2);

                  reconsider m = (ma + n), k2 as Nat;

                  take m, k2;

                  (ma + n) in ( dom G1) by A135, A140;

                  hence [m, k2] in ( Indices G1) & (h2 /. n) = (G1 * (m,k2)) by A134, A133, A96, A140, ZFMISC_1: 87;

                end;

                 A141:

                now

                  let n;

                  assume that

                   A142: n in ( dom h2) and

                   A143: (n + 1) in ( dom h2);

                  (ma + (n + 1)) in ( dom G1) by A135, A143;

                  then

                   A144: [((ma + n) + 1), k2] in ( Indices G1) by A134, A96, ZFMISC_1: 87;

                  let i1,i2,j1,j2 be Nat;

                  assume that

                   A145: [i1, i2] in ( Indices G1) and

                   A146: [j1, j2] in ( Indices G1) and

                   A147: (h2 /. n) = (G1 * (i1,i2)) and

                   A148: (h2 /. (n + 1)) = (G1 * (j1,j2));

                  (h2 /. (n + 1)) = (G1 * ((ma + (n + 1)),k2)) by A133, A143;

                  then

                   A149: j1 = ((ma + n) + 1) & j2 = k2 by A144, A146, A148, GOBOARD1: 5;

                  (ma + n) in ( dom G1) by A135, A142;

                  then

                   A150: [(ma + n), k2] in ( Indices G1) by A134, A96, ZFMISC_1: 87;

                  (h2 /. n) = (G1 * ((ma + n),k2)) by A133, A142;

                  then i1 = (ma + n) & i2 = k2 by A150, A145, A147, GOBOARD1: 5;

                  

                  hence ( |.(i1 - j1).| + |.(i2 - j2).|) = ( |.(((ma + n) - (ma + n)) + ( - 1)).| + 0 ) by A149, ABSVALUE: 2

                  .= |.1.| by COMPLEX1: 52

                  .= 1 by ABSVALUE:def 1;

                end;

                

                 A151: mi1 <= (mi1 + 1) by NAT_1: 11;

                

                 A152: ( 0 + 1) < ( width G1) by A3, A92, XREAL_1: 6;

                

                 A153: ( len ( DelCol (G1,( width G1)))) = ( len G1) by MATRIX_0:def 13;

                ma1 <= mi1 by A130;

                then

                reconsider l = ((mi1 + 1) - ma1) as Element of NAT by A151, INT_1: 5, XXREAL_0: 2;

                set f1 = (g1 | mi1);

                defpred P[ Nat, Element of ( TOP-REAL 2)] means $2 = (f1 /. (w + $1));

                

                 A154: for n be Nat st n in ( Seg l) holds ex p st P[n, p];

                consider f such that

                 A155: ( len f) = l & for n be Nat st n in ( Seg l) holds P[n, (f /. n)] from FINSEQ_4:sch 1( A154);

                

                 A156: (w + l) = mi1;

                

                 A157: ( dom f) = ( Seg l) by A155, FINSEQ_1:def 3;

                set ff = ((h1 ^ f) ^ h2);

                (ma1 + 1) <= mi1 by A130, NAT_1: 13;

                then (ma1 + 1) <= (mi1 + 1) by NAT_1: 13;

                then

                 A158: 1 <= l by XREAL_1: 19;

                 A159:

                now

                  per cases ;

                    suppose

                     A160: mi = 1;

                    1 <= ma1 by A75, A46, FINSEQ_1: 1;

                    then

                     A161: ma1 in ( Seg mi1) by A130, FINSEQ_1: 1;

                    

                     A162: (w + 1) = ma1;

                    

                     A163: 1 in ( Seg l) by A158, FINSEQ_1: 1;

                    h1 = {} by A74, A160;

                    then ff = (f ^ h2) by FINSEQ_1: 34;

                    

                    then (ff /. 1) = (f /. 1) by A157, A163, FINSEQ_4: 68

                    .= (f1 /. ma1) by A155, A163, A162

                    .= (g1 /. ma1) by A130, A161, FINSEQ_4: 71;

                    hence (ff /. 1) in ( rng ( Line (G1,1))) by A46, A160;

                  end;

                    suppose

                     A164: mi <> 1;

                    1 <= mi by A39, FINSEQ_3: 25;

                    then 1 < mi by A164, XXREAL_0: 1;

                    then (1 + 1) <= mi by NAT_1: 13;

                    then

                     A165: 1 <= l1 by XREAL_1: 19;

                    then

                     A166: 1 in ( dom h1) by A74, FINSEQ_3: 25;

                    

                     A167: ( len ( Line (G1,1))) = ( width G1) by MATRIX_0:def 7;

                    then

                     A168: k1 in ( dom L1) by A51, FINSEQ_1:def 3;

                    ( dom ( Line (G1,1))) = ( Seg ( width G1)) by A167, FINSEQ_1:def 3;

                    then

                     A169: (L1 /. k1) = (L1 . k1) by A51, PARTFUN1:def 6;

                    ( len (h1 ^ f)) = (( len h1) + ( len f)) & 0 <= ( len f) by FINSEQ_1: 22;

                    then ( 0 + 1) <= ( len (h1 ^ f)) by A74, A165, XREAL_1: 7;

                    then 1 in ( dom (h1 ^ f)) by FINSEQ_3: 25;

                    

                    then (ff /. 1) = ((h1 ^ f) /. 1) by FINSEQ_4: 68

                    .= (h1 /. 1) by A166, FINSEQ_4: 68

                    .= (G1 * (1,k1)) by A74, A166

                    .= (L1 /. k1) by A51, A169, MATRIX_0:def 7;

                    hence (ff /. 1) in ( rng ( Line (G1,1))) by A168, PARTFUN2: 2;

                  end;

                end;

                

                 A170: for n st n in ( Seg l) holds (f1 /. (w + n)) = (g1 /. (w + n)) & (w + n) in ( dom g1)

                proof

                  ( 0 + 1) <= ma1 by A46, FINSEQ_3: 25;

                  then

                   A171: 0 <= (ma1 - 1) by XREAL_1: 19;

                  let n such that

                   A172: n in ( Seg l);

                  n <= l by A172, FINSEQ_1: 1;

                  then (n + ma1) <= (l + ma1) by XREAL_1: 7;

                  then

                   A173: ((n + ma1) - 1) <= mi1 by XREAL_1: 20;

                  1 <= n by A172, FINSEQ_1: 1;

                  then ( 0 + 1) <= ((ma1 - 1) + n) by A171, XREAL_1: 7;

                  then (w + n) in ( Seg mi1) by A173, FINSEQ_1: 1;

                  hence thesis by A130, FINSEQ_4: 71;

                end;

                 A174:

                now

                  let n;

                  assume

                   A175: n in ( dom f);

                  then (w + n) in ( dom g1) by A170, A157;

                  then

                  consider i, j such that

                   A176: [i, j] in ( Indices G1) & (g1 /. (w + n)) = (G1 * (i,j)) by A6, GOBOARD1:def 9;

                  take i, j;

                  (f /. n) = (f1 /. (w + n)) by A155, A157, A175;

                  hence [i, j] in ( Indices G1) & (f /. n) = (G1 * (i,j)) by A170, A157, A175, A176;

                end;

                

                 A177: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

                

                 A178: ( rng f) c= ( rng g1)

                proof

                  let x be object;

                  assume x in ( rng f);

                  then

                  consider n be Element of NAT such that

                   A179: n in ( dom f) and

                   A180: x = (f /. n) by PARTFUN2: 2;

                  (f /. n) = (f1 /. (w + n)) by A155, A177, A179;

                  then

                   A181: (f /. n) = (g1 /. (w + n)) by A170, A155, A177, A179;

                  (w + n) in ( dom g1) by A170, A155, A177, A179;

                  hence thesis by A180, A181, PARTFUN2: 2;

                end;

                

                 A182: ( dom h2) = ( Seg ( len h2)) by FINSEQ_1:def 3;

                 A183:

                now

                  per cases ;

                    suppose

                     A184: ma = ( len G1);

                    1 <= mi1 by A130, FINSEQ_3: 25;

                    then

                     A185: mi1 in ( Seg mi1) by FINSEQ_1: 1;

                    

                     A186: ( len f) in ( dom f) by A155, A177, A158, FINSEQ_1: 1;

                    h2 = {} by A133, A184;

                    then

                     A187: ff = (h1 ^ f) by FINSEQ_1: 34;

                    

                    then (ff /. ( len ff)) = (ff /. (( len h1) + ( len f))) by FINSEQ_1: 22

                    .= (f /. l) by A155, A187, A186, FINSEQ_4: 69

                    .= (f1 /. mi1) by A155, A157, A156, A186

                    .= (g1 /. mi1) by A130, A185, FINSEQ_4: 71;

                    hence (ff /. ( len ff)) in ( rng ( Line (G1,( len G1)))) by A130, A184;

                  end;

                    suppose

                     A188: ma <> ( len G1);

                    ma <= ( len G1) by A41, FINSEQ_3: 25;

                    then ma < ( len G1) by A188, XXREAL_0: 1;

                    then (ma + 1) <= ( len G1) by NAT_1: 13;

                    then

                     A189: 1 <= l2 by XREAL_1: 19;

                    then

                     A190: l2 in ( Seg l2) by FINSEQ_1: 1;

                    

                     A191: ( len h2) in ( dom h2) by A133, A189, FINSEQ_3: 25;

                    

                     A192: ( len ( Line (G1,( len G1)))) = ( width G1) by MATRIX_0:def 7;

                    then

                     A193: k2 in ( dom Ll) by A134, FINSEQ_1:def 3;

                    k2 in ( dom Ll) by A134, A192, FINSEQ_1:def 3;

                    then

                     A194: (Ll /. k2) = (Ll . k2) by PARTFUN1:def 6;

                    (ff /. ( len ff)) = (ff /. (( len (h1 ^ f)) + ( len h2))) by FINSEQ_1: 22

                    .= (h2 /. l2) by A133, A191, FINSEQ_4: 69

                    .= (G1 * ((ma + l2),k2)) by A133, A182, A190

                    .= (Ll /. k2) by A134, A194, MATRIX_0:def 7;

                    hence (ff /. ( len ff)) in ( rng ( Line (G1,( len G1)))) by A193, PARTFUN2: 2;

                  end;

                end;

                

                 A195: ( 0 + 1) <= (( len f) + (( len h1) + ( len h2))) by A155, A158, XREAL_1: 7;

                

                 A196: ( rng ff) = (( rng (h1 ^ f)) \/ ( rng h2)) by FINSEQ_1: 31

                .= ((( rng h1) \/ ( rng f)) \/ ( rng h2)) by FINSEQ_1: 31;

                

                 A197: for k st k in ( Seg ( width G1)) & (( rng f) /\ ( rng ( Col (G1,k)))) = {} holds (( rng ff) /\ ( rng ( Col (G1,k)))) = {}

                proof

                  

                   A198: ( len ( Col (G1,k2))) = ( len G1) by MATRIX_0:def 8;

                  

                   A199: ( len ( Col (G1,k1))) = ( len G1) by MATRIX_0:def 8;

                  

                   A200: (w + 1) = ma1;

                  let k;

                  assume that

                   A201: k in ( Seg ( width G1)) and

                   A202: (( rng f) /\ ( rng ( Col (G1,k)))) = {} ;

                  set gg = ( Col (G1,k));

                  assume

                   A203: (( rng ff) /\ ( rng gg)) <> {} ;

                  set x = the Element of (( rng ff) /\ ( rng gg));

                  ( rng ff) = (( rng f) \/ (( rng h1) \/ ( rng h2))) by A196, XBOOLE_1: 4;

                  

                  then

                   A204: (( rng ff) /\ ( rng gg)) = ( {} \/ ((( rng h1) \/ ( rng h2)) /\ ( rng gg))) by A202, XBOOLE_1: 23

                  .= ((( rng h1) /\ ( rng gg)) \/ (( rng h2) /\ ( rng gg))) by XBOOLE_1: 23;

                  now

                    per cases by A203, A204, XBOOLE_0:def 3;

                      suppose

                       A205: x in (( rng h1) /\ ( rng gg));

                      then x in ( rng h1) by XBOOLE_0:def 4;

                      then

                      consider i be Element of NAT such that

                       A206: i in ( dom h1) and

                       A207: x = (h1 /. i) by PARTFUN2: 2;

                      

                       A208: x = (G1 * (i,k1)) by A74, A206, A207;

                      reconsider y = x as Point of ( TOP-REAL 2) by A207;

                      

                       A209: (Lmi /. k1) = (Lmi . k1) by A49, PARTFUN1:def 6;

                      

                       A210: x in ( rng gg) by A205, XBOOLE_0:def 4;

                      

                       A211: ( dom ( Col (G1,k1))) = ( Seg ( len G1)) by A199, FINSEQ_1:def 3

                      .= ( dom G1) by FINSEQ_1:def 3;

                      then

                       A212: (Ck1 /. mi) = (Ck1 . mi) by A39, PARTFUN1:def 6;

                      

                       A213: i in ( dom Ck1) by A97, A206, A211;

                      (Ck1 /. i) = (Ck1 . i) by A97, A206, A211, PARTFUN1:def 6;

                      then y = (Ck1 /. i) by A208, A211, A213, MATRIX_0:def 8;

                      then y in ( rng Ck1) by A213, PARTFUN2: 2;

                      then

                       A214: k1 = k by A51, A201, A210, GOBOARD1: 4;

                      

                       A215: 1 in ( Seg l) by A158, FINSEQ_1: 1;

                      then (f /. 1) = (f1 /. ma1) & (f1 /. ma1) = (g1 /. (w + 1)) by A170, A155, A200;

                      then (f /. 1) = (Ck1 /. mi) by A39, A50, A51, A209, A212, MATRIX_0: 42;

                      then

                       A216: (f /. 1) in ( rng ( Col (G1,k))) by A39, A211, A214, PARTFUN2: 2;

                      (f /. 1) in ( rng f) by A157, A215, PARTFUN2: 2;

                      hence contradiction by A202, A216, XBOOLE_0:def 4;

                    end;

                      suppose

                       A217: x in (( rng h2) /\ ( rng gg));

                      then x in ( rng h2) by XBOOLE_0:def 4;

                      then

                      consider i be Element of NAT such that

                       A218: i in ( dom h2) and

                       A219: x = (h2 /. i) by PARTFUN2: 2;

                      

                       A220: x = (G1 * ((ma + i),k2)) by A133, A218, A219;

                      reconsider y = x as Point of ( TOP-REAL 2) by A219;

                      

                       A221: (Lma /. k2) = (Lma . k2) by A131, PARTFUN1:def 6;

                      

                       A222: x in ( rng gg) by A217, XBOOLE_0:def 4;

                      

                       A223: ( dom ( Col (G1,k2))) = ( Seg ( len G1)) by A198, FINSEQ_1:def 3

                      .= ( dom G1) by FINSEQ_1:def 3;

                      then

                       A224: (Ck2 /. ma) = (Ck2 . ma) by A41, PARTFUN1:def 6;

                      

                       A225: (ma + i) in ( dom Ck2) by A135, A218, A223;

                      (Ck2 /. (ma + i)) = (Ck2 . (ma + i)) by A135, A218, A223, PARTFUN1:def 6;

                      then y = (Ck2 /. (ma + i)) by A220, A223, A225, MATRIX_0:def 8;

                      then y in ( rng Ck2) by A225, PARTFUN2: 2;

                      then

                       A226: k2 = k by A134, A201, A222, GOBOARD1: 4;

                      

                       A227: l in ( Seg l) by A158, FINSEQ_1: 1;

                      then (f /. l) = (f1 /. (w + l)) & (f1 /. (w + l)) = (g1 /. (w + l)) by A170, A155;

                      then (f /. l) = (Ck2 /. ma) by A41, A132, A134, A221, A224, MATRIX_0: 42;

                      then

                       A228: (f /. l) in ( rng ( Col (G1,k))) by A41, A223, A226, PARTFUN2: 2;

                      (f /. l) in ( rng f) by A157, A227, PARTFUN2: 2;

                      hence contradiction by A202, A228, XBOOLE_0:def 4;

                    end;

                  end;

                  hence contradiction;

                end;

                (( rng h2) /\ ( rng g)) = {}

                proof

                  set x = the Element of (( rng h2) /\ ( rng g));

                  assume

                   A229: not thesis;

                  then x in ( rng h2) by XBOOLE_0:def 4;

                  then

                  consider n1 be Element of NAT such that

                   A230: n1 in ( dom h2) and

                   A231: x = (h2 /. n1) by PARTFUN2: 2;

                  

                   A232: 1 <= n1 by A230, FINSEQ_3: 25;

                  (ma + n1) in ( dom G1) by A135, A230;

                  then

                   A233: [(ma + n1), k2] in ( Indices G1) by A134, A96, ZFMISC_1: 87;

                  x in ( rng g) by A229, XBOOLE_0:def 4;

                  then

                  consider n2 be Element of NAT such that

                   A234: n2 in ( dom g) and

                   A235: x = (g /. n2) by PARTFUN2: 2;

                  consider i1,i2 be Nat such that

                   A236: [i1, i2] in ( Indices G1) and

                   A237: (g /. n2) = (G1 * (i1,i2)) by A15, A234, GOBOARD1:def 9;

                  reconsider L = ( Line (G1,i1)) as FinSequence of ( TOP-REAL 2);

                  

                   A238: i2 in ( Seg ( width G1)) by A96, A236, ZFMISC_1: 87;

                  

                   A239: ( Seg ( len L)) = ( dom L) & ( len L) = ( width G1) by FINSEQ_1:def 3, MATRIX_0:def 7;

                  then (L /. i2) = (L . i2) by A238, PARTFUN1:def 6;

                  then (g /. n2) = (L /. i2) by A237, A238, MATRIX_0:def 7;

                  then

                   A240: (g /. n2) in ( rng L) by A238, A239, PARTFUN2: 2;

                  (g /. n2) in ( rng g) by A234, PARTFUN2: 2;

                  then

                   A241: (( rng g) /\ ( rng L)) <> {} by A240, XBOOLE_0:def 4;

                  

                   A242: i1 in ( dom G1) by A96, A236, ZFMISC_1: 87;

                  x = (G1 * ((ma + n1),k2)) by A133, A230, A231;

                  then i1 = (ma + n1) by A235, A236, A237, A233, GOBOARD1: 5;

                  then n1 <= 0 by A41, A242, A241, XREAL_1: 29;

                  hence contradiction by A232;

                end;

                

                then (( rng ff) /\ ( rng g)) = (((( rng h1) \/ ( rng f)) /\ ( rng g)) \/ {} ) by A196, XBOOLE_1: 23

                .= ( {} \/ (( rng f) /\ ( rng g))) by A112, XBOOLE_1: 23

                .= (( rng f) /\ ( rng g));

                then

                 A243: (( rng ff) /\ ( rng g)) c= (( rng g1) /\ ( rng g2)) by A18, A178, XBOOLE_1: 27;

                

                 A244: ( len ( DelCol (G1,1))) = ( len G1) by MATRIX_0:def 13;

                

                then

                 A245: ( dom ( DelCol (G1,1))) = ( Seg ( len G1)) by FINSEQ_1:def 3

                .= ( dom G1) by FINSEQ_1:def 3;

                 A246:

                now

                  let n;

                  assume that

                   A247: n in ( dom f) and

                   A248: (n + 1) in ( dom f);

                  (f /. n) = (f1 /. (w + n)) by A155, A157, A247;

                  then

                   A249: (f /. n) = (g1 /. (w + n)) by A170, A157, A247;

                  (f /. (n + 1)) = (f1 /. (w + (n + 1))) by A155, A157, A248;

                  then

                   A250: ((w + n) + 1) in ( dom g1) & (f /. (n + 1)) = (g1 /. ((w + n) + 1)) by A170, A157, A248;

                  let i1,i2,j1,j2 be Nat;

                  assume

                   A251: [i1, i2] in ( Indices G1) & [j1, j2] in ( Indices G1) & (f /. n) = (G1 * (i1,i2)) & (f /. (n + 1)) = (G1 * (j1,j2));

                  (w + n) in ( dom g1) by A170, A157, A247;

                  hence ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A6, A249, A250, A251, GOBOARD1:def 9;

                end;

                set hf = (h1 ^ f);

                

                 A252: ( len ff) = (( len (h1 ^ f)) + ( len h2)) by FINSEQ_1: 22

                .= ((( len h1) + ( len f)) + ( len h2)) by FINSEQ_1: 22;

                 A253:

                now

                  let i1,i2,j1,j2 be Nat;

                  assume that

                   A254: [i1, i2] in ( Indices G1) and

                   A255: [j1, j2] in ( Indices G1) and

                   A256: (hf /. ( len hf)) = (G1 * (i1,i2)) and

                   A257: (h2 /. 1) = (G1 * (j1,j2)) and ( len hf) in ( dom hf) and

                   A258: 1 in ( dom h2);

                  (ma + 1) in ( dom G1) by A135, A258;

                  then

                   A259: [(ma + 1), k2] in ( Indices G1) by A134, A96, ZFMISC_1: 87;

                  

                   A260: [ma, k2] in ( Indices G1) by A41, A134, A96, ZFMISC_1: 87;

                  

                   A261: (Lma /. k2) = (Lma . k2) by A131, PARTFUN1:def 6;

                  

                   A262: ( len f) in ( dom f) by A155, A157, A158, FINSEQ_1: 1;

                  (hf /. ( len hf)) = (hf /. (( len h1) + ( len f))) by FINSEQ_1: 22

                  .= (f /. ( len f)) by A262, FINSEQ_4: 69

                  .= (f1 /. (w + l)) by A155, A157, A262

                  .= (g1 /. mi1) by A170, A155, A157, A262

                  .= (G1 * (ma,k2)) by A132, A134, A261, MATRIX_0:def 7;

                  then

                   A263: i1 = ma & i2 = k2 by A254, A256, A260, GOBOARD1: 5;

                  (h2 /. 1) = (G1 * ((ma + 1),k2)) by A133, A258;

                  then j1 = (ma + 1) & j2 = k2 by A255, A257, A259, GOBOARD1: 5;

                  

                  hence ( |.(i1 - j1).| + |.(i2 - j2).|) = ( |.(ma - (ma + 1)).| + 0 ) by A263, ABSVALUE: 2

                  .= |.( - ((ma + 1) - ma)).|

                  .= |.1.| by COMPLEX1: 52

                  .= 1 by ABSVALUE:def 1;

                end;

                now

                  

                   A264: [mi, k1] in ( Indices G1) by A39, A51, A96, ZFMISC_1: 87;

                  

                   A265: (Lmi /. k1) = (Lmi . k1) by A49, PARTFUN1:def 6;

                  let i1,i2,j1,j2 be Nat;

                  assume that

                   A266: [i1, i2] in ( Indices G1) and

                   A267: [j1, j2] in ( Indices G1) and

                   A268: (h1 /. ( len h1)) = (G1 * (i1,i2)) and

                   A269: (f /. 1) = (G1 * (j1,j2)) and

                   A270: ( len h1) in ( dom h1) and

                   A271: 1 in ( dom f);

                  l1 in ( dom G1) by A74, A97, A270;

                  then

                   A272: [l1, k1] in ( Indices G1) by A51, A96, ZFMISC_1: 87;

                  

                   A273: (w + 1) = ma1;

                  then (f /. 1) = (f1 /. ma1) by A155, A157, A271;

                  

                  then (f /. 1) = (g1 /. ma1) by A170, A157, A271, A273

                  .= (G1 * (mi,k1)) by A50, A51, A265, MATRIX_0:def 7;

                  then

                   A274: j1 = mi & j2 = k1 by A267, A269, A264, GOBOARD1: 5;

                  (h1 /. ( len h1)) = (G1 * (l1,k1)) by A74, A270;

                  then i1 = l1 & i2 = k1 by A266, A268, A272, GOBOARD1: 5;

                  

                  hence ( |.(i1 - j1).| + |.(i2 - j2).|) = ( |.((mi - 1) - mi).| + 0 ) by A274, ABSVALUE: 2

                  .= |.( - 1).|

                  .= |.1.| by COMPLEX1: 52

                  .= 1 by ABSVALUE:def 1;

                end;

                then for n st n in ( dom (h1 ^ f)) & (n + 1) in ( dom (h1 ^ f)) holds for i1,i2,j1,j2 be Nat st [i1, i2] in ( Indices G1) & [j1, j2] in ( Indices G1) & ((h1 ^ f) /. n) = (G1 * (i1,i2)) & ((h1 ^ f) /. (n + 1)) = (G1 * (j1,j2)) holds ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A102, A246, GOBOARD1: 24;

                then

                 A275: for n st n in ( dom ff) & (n + 1) in ( dom ff) holds for m, k, i, j st [m, k] in ( Indices G1) & [i, j] in ( Indices G1) & (ff /. n) = (G1 * (m,k)) & (ff /. (n + 1)) = (G1 * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1 by A141, A253, GOBOARD1: 24;

                now

                  let n;

                  assume

                   A276: n in ( dom h1);

                  reconsider k1 as Nat;

                  take i = n, k1;

                  n in ( dom G1) by A97, A276;

                  hence [i, k1] in ( Indices G1) & (h1 /. n) = (G1 * (i,k1)) by A74, A51, A96, A276, ZFMISC_1: 87;

                end;

                then for n st n in ( dom (h1 ^ f)) holds ex i, j st [i, j] in ( Indices G1) & ((h1 ^ f) /. n) = (G1 * (i,j)) by A174, GOBOARD1: 23;

                then for n st n in ( dom ff) holds ex i, j st [i, j] in ( Indices G1) & (ff /. n) = (G1 * (i,j)) by A139, GOBOARD1: 23;

                then

                 A277: ff is_sequence_on G1 by A275, GOBOARD1:def 9;

                

                 A278: ( Seg ( len ff)) = ( dom ff) by FINSEQ_1:def 3;

                then

                 A279: ( len ff) in ( dom ff) by A252, A195, FINSEQ_1: 1;

                

                 A280: 1 in ( dom ff) by A252, A195, A278, FINSEQ_1: 1;

                thus thesis

                proof

                  per cases ;

                    suppose

                     A281: (( rng f) /\ ( rng ( Col (G1,1)))) = {} ;

                    set D = ( DelCol (G1,1));

                    

                     A282: 1 in ( Seg ( width G1)) by A152, FINSEQ_1: 1;

                    

                     A283: not D is empty-yielding by A152, A282, MATRIX_0: 65;

                    (( rng ff) /\ ( rng ( Col (G1,1)))) = {} by A31, A197, A281;

                    then

                     A284: ( rng ff) misses ( rng ( Col (G1,1))) by XBOOLE_0:def 7;

                    then

                     A285: ff is_sequence_on D & (ff /. 1) in ( rng ( Line (D,1))) by A31, A26, A277, A159, A152, A280, GOBOARD1: 25, MATRIX_0: 75;

                    

                     A286: (ff /. ( len ff)) in ( rng ( Line (D,( len D)))) by A31, A27, A183, A152, A244, A279, A284, MATRIX_0: 75;

                    defpred P[ Nat] means $1 in ( dom g) & (g /. $1) in ( rng ( Col (G1,1)));

                    

                     A287: ex m be Nat st P[m]

                    proof

                      take 1;

                      thus thesis by A10, A13, A32, FINSEQ_3: 25, FINSEQ_4: 92;

                    end;

                    

                     A288: for m be Nat st P[m] holds m <= ( len g) by FINSEQ_3: 25;

                    consider m be Nat such that

                     A289: P[m] & for k be Nat st P[k] holds k <= m from NAT_1:sch 6( A288, A287);

                    reconsider m as Nat;

                    reconsider p = (g /. m) as Point of ( TOP-REAL 2);

                     A290:

                    now

                      assume

                       A291: m >= ( len g);

                      m <= ( len g) by A289, FINSEQ_3: 25;

                      then p in ( rng ( Col (G1,( width G1)))) by A28, A291, XXREAL_0: 1;

                      then 1 = (k + 1) by A3, A31, A73, A289, GOBOARD1: 4;

                      hence contradiction by A91;

                    end;

                    then

                    reconsider ll = (( len g) - m) as Element of NAT by INT_1: 5;

                    deffunc F( Nat) = (g /. (m + $1));

                    consider t be FinSequence of ( TOP-REAL 2) such that

                     A292: ( len t) = ll & for n be Nat st n in ( dom t) holds (t /. n) = F(n) from FINSEQ_4:sch 2;

                    

                     A293: ( dom t) = ( Seg ll) by A292, FINSEQ_1:def 3;

                    

                     A294: ( rng t) c= ( rng g)

                    proof

                      let y be object;

                      assume y in ( rng t);

                      then

                      consider x be Element of NAT such that

                       A295: x in ( dom t) and

                       A296: (t /. x) = y by PARTFUN2: 2;

                      x <= ll by A293, A295, FINSEQ_1: 1;

                      then

                       A297: (m + x) <= (m + ll) by XREAL_1: 7;

                      

                       A298: x <= (x + m) by NAT_1: 11;

                      1 <= x by A293, A295, FINSEQ_1: 1;

                      then 1 <= (x + m) by A298, XXREAL_0: 2;

                      then (m + x) in ( dom g) by A297, FINSEQ_3: 25;

                      then (g /. (m + x)) in ( rng g) by PARTFUN2: 2;

                      hence thesis by A292, A295, A296;

                    end;

                    

                     A299: for n st n in ( dom t) holds (m + n) in ( dom g)

                    proof

                      let n;

                      

                       A300: n <= (n + m) by NAT_1: 11;

                      assume

                       A301: n in ( dom t);

                      then n <= ll by A293, FINSEQ_1: 1;

                      then

                       A302: (m + n) <= (m + ll) by XREAL_1: 7;

                      1 <= n by A293, A301, FINSEQ_1: 1;

                      then 1 <= (n + m) by A300, XXREAL_0: 2;

                      hence thesis by A302, FINSEQ_3: 25;

                    end;

                    

                     A303: ( Seg ( len t)) = ( dom t) by FINSEQ_1:def 3;

                    reconsider t as FinSequence of ( TOP-REAL 2);

                    

                     A304: ( width D) = k by A3, A31, MATRIX_0: 63;

                    

                     A305: ( Indices D) = [:( dom D), ( Seg ( width D)):] by MATRIX_0:def 4;

                     A306:

                    now

                      let n;

                      assume

                       A307: n in ( dom t);

                      then (m + n) in ( dom g) by A299;

                      then

                      consider i1,i2 be Nat such that

                       A308: [i1, i2] in ( Indices G1) and

                       A309: (g /. (m + n)) = (G1 * (i1,i2)) by A15, GOBOARD1:def 9;

                      

                       A310: i2 in ( Seg ( width G1)) by A96, A308, ZFMISC_1: 87;

                      then

                       A311: 1 <= i2 by FINSEQ_1: 1;

                      then

                      reconsider l = (i2 - 1) as Element of NAT by INT_1: 5;

                      reconsider Ci2 = ( Col (G1,i2)) as FinSequence of ( TOP-REAL 2);

                      

                       A312: i1 in ( dom G1) by A96, A308, ZFMISC_1: 87;

                      ( len Ci2) = ( len G1) by MATRIX_0:def 8;

                      

                      then

                       A313: ( dom Ci2) = ( Seg ( len G1)) by FINSEQ_1:def 3

                      .= ( dom G1) by FINSEQ_1:def 3;

                      then (Ci2 /. i1) = (Ci2 . i1) by A312, PARTFUN1:def 6;

                      then (Ci2 /. i1) = (G1 * (i1,i2)) by A312, MATRIX_0:def 8;

                      then

                       A314: (g /. (m + n)) in ( rng ( Col (G1,i2))) by A309, A312, A313, PARTFUN2: 2;

                      now

                        1 <= n by A293, A307, FINSEQ_1: 1;

                        then

                         A315: (m + 1) <= (m + n) by XREAL_1: 7;

                        assume i2 = 1;

                        then (m + n) <= m by A289, A299, A307, A314;

                        then (m + 1) <= m by A315, XXREAL_0: 2;

                        then 1 <= (m - m) by XREAL_1: 19;

                        then 1 <= 0 ;

                        hence contradiction;

                      end;

                      then 1 < i2 by A311, XXREAL_0: 1;

                      then (1 + 1) <= i2 by NAT_1: 13;

                      then

                       A316: 1 <= l by XREAL_1: 19;

                      reconsider i1, l as Nat;

                      take i1;

                      take l;

                      

                       A317: (t /. n) = (g /. (m + n)) by A292, A307;

                      i2 <= ( width G1) by A310, FINSEQ_1: 1;

                      then

                       A318: l <= ( width D) by A3, A304, XREAL_1: 20;

                      then l in ( Seg ( width D)) by A316, FINSEQ_1: 1;

                      hence [i1, l] in ( Indices D) by A245, A305, A312, ZFMISC_1: 87;

                      (l + 1) = i2;

                      hence (t /. n) = (D * (i1,l)) by A3, A31, A304, A309, A312, A317, A316, A318, MATRIX_0: 70;

                    end;

                     0 < ( width D) by A283, MATRIX_0:def 10, NAT_1: 3;

                    then

                     A319: ( 0 + 1) <= ( width D) by NAT_1: 13;

                    then

                     A320: ( Col (D,1)) = ( Col (G1,(1 + 1))) & (1 + 1) in ( Seg ( width G1)) by A3, A31, A304, MATRIX_0: 68;

                    (m + 1) <= ( len g) by A290, NAT_1: 13;

                    then

                     A321: 1 <= ( len t) by A292, XREAL_1: 19;

                    then (t /. 1) = (g /. (m + 1)) by A292, A303, FINSEQ_1: 1;

                    then

                     A322: (t /. 1) in ( rng ( Col (D,1))) by A32, A15, A28, A31, A289, A320, GOBOARD1: 32;

                    now

                      let n;

                      assume that

                       A323: n in ( dom t) and

                       A324: (n + 1) in ( dom t);

                      let i1,i2,j1,j2 be Nat;

                      assume that

                       A325: [i1, i2] in ( Indices D) and

                       A326: [j1, j2] in ( Indices D) and

                       A327: (t /. n) = (D * (i1,i2)) and

                       A328: (t /. (n + 1)) = (D * (j1,j2));

                      

                       A329: i1 in ( dom D) by A305, A325, ZFMISC_1: 87;

                      i2 in ( Seg k) by A304, A305, A325, ZFMISC_1: 87;

                      then

                       A330: 1 <= i2 & i2 <= k by FINSEQ_1: 1;

                      then (i2 + 1) in ( Seg ( width G1)) by A3, A31, A245, A329, MATRIX_0: 70;

                      then

                       A331: [i1, (i2 + 1)] in ( Indices G1) by A96, A245, A329, ZFMISC_1: 87;

                      (t /. n) = (g /. (m + n)) by A292, A323;

                      then

                       A332: (g /. (m + n)) = (G1 * (i1,(i2 + 1))) by A3, A31, A245, A327, A329, A330, MATRIX_0: 70;

                      (m + (n + 1)) = ((m + n) + 1);

                      then

                       A333: ((m + n) + 1) in ( dom g) by A299, A324;

                      

                       A334: j1 in ( dom D) by A305, A326, ZFMISC_1: 87;

                      j2 in ( Seg k) by A304, A305, A326, ZFMISC_1: 87;

                      then

                       A335: 1 <= j2 & j2 <= k by FINSEQ_1: 1;

                      then (j2 + 1) in ( Seg ( width G1)) by A3, A31, A245, A329, MATRIX_0: 70;

                      then

                       A336: [j1, (j2 + 1)] in ( Indices G1) by A96, A245, A334, ZFMISC_1: 87;

                      (t /. (n + 1)) = (g /. (m + (n + 1))) by A292, A324;

                      then

                       A337: (g /. ((m + n) + 1)) = (G1 * (j1,(j2 + 1))) by A3, A31, A245, A328, A334, A335, MATRIX_0: 70;

                      (m + n) in ( dom g) by A299, A323;

                      

                      hence 1 = ( |.(i1 - j1).| + |.((i2 + 1) - (j2 + 1)).|) by A15, A332, A337, A331, A336, A333, GOBOARD1:def 9

                      .= ( |.(i1 - j1).| + |.(i2 - j2).|);

                    end;

                    then

                     A338: t is_sequence_on D by A306, GOBOARD1:def 9;

                    set x = the Element of (( rng ff) /\ ( rng t));

                    

                     A339: (( rng ff) /\ ( rng t)) c= (( rng ff) /\ ( rng g)) by A294, XBOOLE_1: 26;

                    ( len t) in ( Seg ll) by A292, A321, FINSEQ_1: 1;

                    

                    then (t /. ( len t)) = (g /. (m + ll)) by A292, A303

                    .= (g /. ( len g));

                    then (t /. ( len t)) in ( rng ( Col (D,( width D)))) by A3, A28, A31, A304, A319, MATRIX_0: 68;

                    then (( rng ff) /\ ( rng t)) <> {} by A2, A92, A252, A195, A304, A321, A322, A338, A285, A286, A283;

                    then x in (( rng ff) /\ ( rng g)) by A339;

                    hence thesis by A243;

                  end;

                    suppose

                     A340: (( rng f) /\ ( rng ( Col (G1,1)))) <> {} ;

                    set D = ( DelCol (G1,( width G1)));

                    

                     A341: not D is empty-yielding by A93, A94, MATRIX_0: 65;

                    

                     A342: ( 0 + 1) < (k + 1) by A92, XREAL_1: 6;

                    now

                      per cases ;

                        suppose (( rng f) /\ ( rng ( Col (G1,( width G1))))) = {} ;

                        then (( rng ff) /\ ( rng ( Col (G1,( width G1))))) = {} by A73, A197;

                        then

                         A343: ( rng ff) misses ( rng ( Col (G1,( width G1)))) by XBOOLE_0:def 7;

                        then

                         A344: ff is_sequence_on D by A73, A277, A152, GOBOARD1: 25;

                        consider t be FinSequence of ( TOP-REAL 2) such that

                         A345: (t /. 1) in ( rng ( Col (D,1))) & (t /. ( len t)) in ( rng ( Col (D,( width D)))) & 1 <= ( len t) & t is_sequence_on D and

                         A346: ( rng t) c= ( rng g) by A3, A32, A15, A14, A28, A342, GOBOARD1: 35;

                        set x = the Element of (( rng ff) /\ ( rng t));

                        

                         A347: (( rng ff) /\ ( rng t)) c= (( rng ff) /\ ( rng g)) by A346, XBOOLE_1: 26;

                        

                         A348: ( width D) = k by A3, A73, MATRIX_0: 63;

                        (ff /. 1) in ( rng ( Line (D,1))) & (ff /. ( len ff)) in ( rng ( Line (D,( len D)))) by A73, A26, A27, A159, A183, A152, A153, A280, A279, A343, MATRIX_0: 75;

                        then (( rng ff) /\ ( rng t)) <> {} by A2, A92, A252, A195, A345, A348, A344, A341;

                        then x in (( rng ff) /\ ( rng g)) by A347;

                        hence thesis by A243;

                      end;

                        suppose

                         A349: (( rng f) /\ ( rng ( Col (G1,( width G1))))) <> {} ;

                        

                         A350: f is_sequence_on G1 by A174, A246, GOBOARD1:def 9;

                        then

                        consider t be FinSequence of ( TOP-REAL 2) such that

                         A351: ( rng t) c= ( rng f) and

                         A352: (t /. 1) in ( rng ( Col (G1,1))) & (t /. ( len t)) in ( rng ( Col (G1,( width G1)))) & 1 <= ( len t) & t is_sequence_on G1 by A340, A349, GOBOARD1: 36;

                        consider tt be FinSequence of ( TOP-REAL 2) such that

                         A353: (tt /. 1) in ( rng ( Col (D,1))) & (tt /. ( len tt)) in ( rng ( Col (D,( width D)))) & 1 <= ( len tt) & tt is_sequence_on D and

                         A354: ( rng tt) c= ( rng t) by A3, A342, A352, GOBOARD1: 35;

                        

                         A355: ( Seg ( len Lma)) = ( dom Lma) & ( len Lma) = ( width G1) by FINSEQ_1:def 3, MATRIX_0:def 7;

                        reconsider lg = (( len g) - 1) as Element of NAT by A32, INT_1: 5;

                        defpred P[ Nat] means $1 in ( dom g) & (g /. $1) in ( rng ( Line (G1,mi)));

                        defpred R[ Nat] means $1 in ( dom g) & (g /. $1) in ( rng ( Line (G1,ma)));

                        

                         A356: lg <= ( len g) by XREAL_1: 43;

                         A357:

                        now

                          set x = the Element of (( rng g) /\ ( rng ( Line (G1,mi))));

                          x in ( rng g) by A39, XBOOLE_0:def 4;

                          then

                          consider n be Element of NAT such that

                           A358: n in ( dom g) & x = (g /. n) by PARTFUN2: 2;

                          reconsider n as Nat;

                          take n;

                          thus P[n] by A39, A358, XBOOLE_0:def 4;

                        end;

                        consider pf be Nat such that

                         A359: P[pf] & for n be Nat st P[n] holds pf <= n from NAT_1:sch 5( A357);

                        defpred PP[ Nat] means $1 in ( dom f) implies for m st m in ( dom G1) & (f /. $1) in ( rng ( Line (G1,m))) holds mi <= m;

                        reconsider C = ( Col (G1,( width G1))), Li = ( Line (G1,mi)), La = ( Line (G1,ma)) as FinSequence of ( TOP-REAL 2);

                        

                         A360: (lg + 1) = ( len g);

                         A361:

                        now

                          set x = the Element of (( rng g) /\ ( rng ( Line (G1,ma))));

                          x in ( rng g) by A41, XBOOLE_0:def 4;

                          then

                          consider n be Element of NAT such that

                           A362: n in ( dom g) & x = (g /. n) by PARTFUN2: 2;

                          reconsider n as Nat;

                          take n;

                          thus R[n] by A41, A362, XBOOLE_0:def 4;

                        end;

                        consider pl be Nat such that

                         A363: R[pl] & for n be Nat st R[n] holds pl <= n from NAT_1:sch 5( A361);

                        reconsider pf, pl as Nat;

                        

                         A364: 1 <= pf by A359, FINSEQ_3: 25;

                        consider K2 be Element of NAT such that

                         A365: K2 in ( dom Lma) and

                         A366: (g /. pl) = (Lma /. K2) by A363, PARTFUN2: 2;

                        reconsider CK2 = ( Col (G1,K2)) as FinSequence of ( TOP-REAL 2);

                        consider K1 be Element of NAT such that

                         A367: K1 in ( dom Li) and

                         A368: (g /. pf) = (Li /. K1) by A359, PARTFUN2: 2;

                        reconsider CK1 = ( Col (G1,K1)) as FinSequence of ( TOP-REAL 2);

                        deffunc F( Nat) = (G1 * ($1,K1));

                        consider h1 be FinSequence of ( TOP-REAL 2) such that

                         A369: ( len h1) = l1 & for n be Nat st n in ( dom h1) holds (h1 /. n) = F(n) from FINSEQ_4:sch 2;

                        

                         A370: for k st PP[k] holds PP[(k + 1)]

                        proof

                          let k such that

                           A371: PP[k];

                          assume

                           A372: (k + 1) in ( dom f);

                          let m such that

                           A373: m in ( dom G1) & (f /. (k + 1)) in ( rng ( Line (G1,m)));

                          now

                            per cases ;

                              suppose

                               A374: k = 0 ;

                              (w + 1) = ma1 & 1 in ( Seg l) by A158, FINSEQ_1: 1;

                              then (f /. 1) = (f1 /. ma1) & (f1 /. ma1) = (g1 /. ma1) by A170, A155;

                              then (f /. (k + 1)) in ( rng Li) by A49, A50, A374, PARTFUN2: 2;

                              hence thesis by A39, A373, GOBOARD1: 3;

                            end;

                              suppose k <> 0 ;

                              then 0 < k;

                              then

                               A375: ( 0 + 1) <= k by NAT_1: 13;

                              (k + 1) <= ( len f) by A372, FINSEQ_3: 25;

                              then

                               A376: k <= ( len f) by NAT_1: 13;

                              then

                               A377: k in ( dom f) by A375, FINSEQ_3: 25;

                              then

                              consider i1,i2 be Nat such that

                               A378: [i1, i2] in ( Indices G1) and

                               A379: (f /. k) = (G1 * (i1,i2)) by A174;

                              

                               A380: i2 in ( Seg ( width G1)) by A96, A378, ZFMISC_1: 87;

                              consider j1,j2 be Nat such that

                               A381: [j1, j2] in ( Indices G1) and

                               A382: (f /. (k + 1)) = (G1 * (j1,j2)) by A174, A372;

                              reconsider Lj1 = ( Line (G1,j1)) as FinSequence of ( TOP-REAL 2);

                              

                               A383: j2 in ( Seg ( width G1)) by A96, A381, ZFMISC_1: 87;

                              

                               A384: ( Seg ( len Lj1)) = ( dom Lj1) & ( len Lj1) = ( width G1) by FINSEQ_1:def 3, MATRIX_0:def 7;

                              then (Lj1 /. j2) = (Lj1 . j2) by A383, PARTFUN1:def 6;

                              then (f /. (k + 1)) = (Lj1 /. j2) by A382, A383, MATRIX_0:def 7;

                              then

                               A385: (f /. (k + 1)) in ( rng Lj1) by A383, A384, PARTFUN2: 2;

                              

                               A386: j1 in ( dom G1) by A96, A381, ZFMISC_1: 87;

                              reconsider Li1 = ( Line (G1,i1)) as FinSequence of ( TOP-REAL 2);

                              

                               A387: i1 in ( dom G1) by A96, A378, ZFMISC_1: 87;

                              

                               A388: ( Seg ( len Li1)) = ( dom Li1) & ( len Li1) = ( width G1) by FINSEQ_1:def 3, MATRIX_0:def 7;

                              then

                               A389: (Li1 /. i2) = (Li1 . i2) by A380, PARTFUN1:def 6;

                              then (f /. k) = (Li1 /. i2) by A379, A380, MATRIX_0:def 7;

                              then

                               A390: (f /. k) in ( rng Li1) by A380, A388, PARTFUN2: 2;

                              then

                               A391: mi <= i1 by A371, A375, A376, A387, FINSEQ_3: 25;

                              now

                                per cases by A391, XXREAL_0: 1;

                                  suppose

                                   A392: mi = i1;

                                  (g1 /. (w + k)) = (f1 /. (w + k)) by A170, A157, A377

                                  .= (f /. k) by A155, A157, A377

                                  .= (Li1 /. i2) by A379, A380, A389, MATRIX_0:def 7;

                                  then (g1 /. (w + k)) in ( rng ( Line (G1,mi))) by A380, A388, A392, PARTFUN2: 2;

                                  then

                                   A393: (w + k) <= ma1 by A46, A170, A157, A377;

                                  (w + 1) <= (w + k) by A375, XREAL_1: 7;

                                  then (w + k) = ma1 by A393, XXREAL_0: 1;

                                  then

                                   A394: (ma1 + 1) = (w + (k + 1));

                                  (mi + 1) <= ma by A128, NAT_1: 13;

                                  then

                                   A395: (mi + 1) <= ( len G1) by A48, XXREAL_0: 2;

                                  1 <= (mi + 1) by A42, NAT_1: 13;

                                  then

                                   A396: (mi + 1) in ( dom G1) by A395, FINSEQ_3: 25;

                                  (f /. (k + 1)) = (f1 /. (w + (k + 1))) & (f1 /. (w + (k + 1))) = (g1 /. (w + (k + 1))) by A170, A155, A157, A372;

                                  then (f /. (k + 1)) in ( rng ( Line (G1,(mi + 1)))) by A4, A6, A9, A39, A46, A394, A396, GOBOARD1: 28;

                                  then m = (mi + 1) by A373, A396, GOBOARD1: 3;

                                  hence thesis by NAT_1: 11;

                                end;

                                  suppose

                                   A397: mi < i1;

                                  now

                                    per cases by A350, A372, A377, A387, A390, GOBOARD1: 27;

                                      suppose (f /. (k + 1)) in ( rng ( Line (G1,i1)));

                                      hence thesis by A373, A387, A397, GOBOARD1: 3;

                                    end;

                                      suppose for l be Nat st (f /. (k + 1)) in ( rng ( Line (G1,l))) & l in ( dom G1) holds |.(i1 - l).| = 1;

                                      then

                                       A398: |.(i1 - j1).| = 1 by A386, A385;

                                      now

                                        per cases by A398, SEQM_3: 41;

                                          suppose

                                           A399: j1 < i1 & i1 = (j1 + 1);

                                          then mi <= (i1 - 1) by A397, NAT_1: 13;

                                          hence thesis by A373, A386, A385, A399, GOBOARD1: 3;

                                        end;

                                          suppose i1 < j1 & j1 = (i1 + 1);

                                          then mi < j1 by A397, XXREAL_0: 2;

                                          hence thesis by A373, A386, A385, GOBOARD1: 3;

                                        end;

                                      end;

                                      hence thesis;

                                    end;

                                  end;

                                  hence thesis;

                                end;

                              end;

                              hence thesis;

                            end;

                          end;

                          hence thesis;

                        end;

                        

                         A400: ( Seg ( len Li)) = ( dom Li) & ( len Li) = ( width G1) by FINSEQ_1:def 3, MATRIX_0:def 7;

                         A401:

                        now

                          let n;

                          

                           A402: l1 <= mi by XREAL_1: 43;

                          assume

                           A403: n in ( dom h1);

                          then

                           A404: 1 <= n by FINSEQ_3: 25;

                          n <= l1 by A369, A403, FINSEQ_3: 25;

                          then

                           A405: n <= mi by A402, XXREAL_0: 2;

                          mi <= ( len G1) by A39, FINSEQ_3: 25;

                          then n <= ( len G1) by A405, XXREAL_0: 2;

                          hence n in ( dom G1) by A404, FINSEQ_3: 25;

                        end;

                         A406:

                        now

                          let n;

                          assume

                           A407: n in ( dom h1);

                          reconsider i = n, K1 as Nat;

                          take i, K1;

                          n in ( dom G1) by A401, A407;

                          hence [i, K1] in ( Indices G1) & (h1 /. n) = (G1 * (i,K1)) by A96, A367, A400, A369, A407, ZFMISC_1: 87;

                        end;

                         A408:

                        now

                          let n;

                          assume that

                           A409: n in ( dom h1) and

                           A410: (n + 1) in ( dom h1);

                          (n + 1) in ( dom G1) by A401, A410;

                          then

                           A411: [(n + 1), K1] in ( Indices G1) by A96, A367, A400, ZFMISC_1: 87;

                          let i1,i2,j1,j2 be Nat;

                          assume that

                           A412: [i1, i2] in ( Indices G1) and

                           A413: [j1, j2] in ( Indices G1) and

                           A414: (h1 /. n) = (G1 * (i1,i2)) and

                           A415: (h1 /. (n + 1)) = (G1 * (j1,j2));

                          (h1 /. (n + 1)) = (G1 * ((n + 1),K1)) by A369, A410;

                          then

                           A416: j1 = (n + 1) & j2 = K1 by A411, A413, A415, GOBOARD1: 5;

                          n in ( dom G1) by A401, A409;

                          then

                           A417: [n, K1] in ( Indices G1) by A96, A367, A400, ZFMISC_1: 87;

                          (h1 /. n) = (G1 * (n,K1)) by A369, A409;

                          then i1 = n & i2 = K1 by A417, A412, A414, GOBOARD1: 5;

                          

                          hence ( |.(i1 - j1).| + |.(i2 - j2).|) = ( |.((n - n) + ( - 1)).| + 0 ) by A416, ABSVALUE: 2

                          .= |.1.| by COMPLEX1: 52

                          .= 1 by ABSVALUE:def 1;

                        end;

                        

                         A418: pf <= ( len g) by A359, FINSEQ_3: 25;

                        

                         A419: (Lma /. K2) = (Lma . K2) by A365, PARTFUN1:def 6;

                        then

                         A420: (g /. pl) = (G1 * (ma,K2)) by A365, A366, A355, MATRIX_0:def 7;

                        deffunc F( Nat) = (G1 * ((ma + $1),K2));

                        consider h2 be FinSequence of ( TOP-REAL 2) such that

                         A421: ( len h2) = l2 & for n be Nat st n in ( dom h2) holds (h2 /. n) = F(n) from FINSEQ_4:sch 2;

                        

                         A422: PP[ 0 ] by FINSEQ_3: 25;

                        

                         A423: for n holds PP[n] from NAT_1:sch 2( A422, A370);

                        

                         A424: (( rng h1) /\ ( rng tt)) = {}

                        proof

                          set x = the Element of (( rng h1) /\ ( rng tt));

                          assume

                           A425: not thesis;

                          then x in ( rng h1) by XBOOLE_0:def 4;

                          then

                          consider i2 be Element of NAT such that

                           A426: i2 in ( dom h1) and

                           A427: (h1 /. i2) = x by PARTFUN2: 2;

                          ( Seg ( len h1)) = ( dom h1) by FINSEQ_1:def 3;

                          then

                           A428: l1 < mi & i2 <= l1 by A369, A426, FINSEQ_1: 1, XREAL_1: 44;

                          i2 in ( dom G1) by A401, A426;

                          then

                           A429: [i2, K1] in ( Indices G1) by A96, A367, A400, ZFMISC_1: 87;

                          x in ( rng tt) by A425, XBOOLE_0:def 4;

                          then x in ( rng t) by A354;

                          then

                          consider i1 be Element of NAT such that

                           A430: i1 in ( dom f) and

                           A431: (f /. i1) = x by A351, PARTFUN2: 2;

                          consider n1,n2 be Nat such that

                           A432: [n1, n2] in ( Indices G1) and

                           A433: (f /. i1) = (G1 * (n1,n2)) by A174, A430;

                          reconsider Ln1 = ( Line (G1,n1)) as FinSequence of ( TOP-REAL 2);

                          

                           A434: n2 in ( Seg ( width G1)) by A96, A432, ZFMISC_1: 87;

                          

                           A435: ( Seg ( len Ln1)) = ( dom Ln1) & ( len Ln1) = ( width G1) by FINSEQ_1:def 3, MATRIX_0:def 7;

                          then (Ln1 /. n2) = (Ln1 . n2) by A434, PARTFUN1:def 6;

                          then (f /. i1) = (Ln1 /. n2) by A433, A434, MATRIX_0:def 7;

                          then

                           A436: (f /. i1) in ( rng Ln1) by A434, A435, PARTFUN2: 2;

                          n1 in ( dom G1) by A96, A432, ZFMISC_1: 87;

                          then

                           A437: mi <= n1 by A423, A430, A436;

                          x = (G1 * (i2,K1)) by A369, A426, A427;

                          then i2 = n1 by A431, A432, A433, A429, GOBOARD1: 5;

                          hence contradiction by A437, A428, XXREAL_0: 2;

                        end;

                        defpred PP[ Nat] means $1 in ( dom f) implies for m st m in ( dom G1) & (f /. $1) in ( rng ( Line (G1,m))) holds m <= ma;

                        

                         A438: for k st PP[k] holds PP[(k + 1)]

                        proof

                          let k such that

                           A439: PP[k];

                          assume

                           A440: (k + 1) in ( dom f);

                          let m such that

                           A441: m in ( dom G1) & (f /. (k + 1)) in ( rng ( Line (G1,m)));

                          now

                            per cases ;

                              suppose

                               A442: k = 0 ;

                              1 in ( Seg l) by A158, FINSEQ_1: 1;

                              then (f /. 1) = (f1 /. (w + 1)) & (f1 /. (w + 1)) = (g1 /. (w + 1)) by A170, A155;

                              then (f /. (k + 1)) in ( rng Li) by A49, A50, A442, PARTFUN2: 2;

                              hence thesis by A39, A127, A441, GOBOARD1: 3;

                            end;

                              suppose

                               A443: k <> 0 ;

                              

                               A444: (k + 1) <= ( len f) by A177, A440, FINSEQ_1: 1;

                              then

                               A445: k <= ( len f) by NAT_1: 13;

                              consider j1,j2 be Nat such that

                               A446: [j1, j2] in ( Indices G1) and

                               A447: (f /. (k + 1)) = (G1 * (j1,j2)) by A174, A440;

                              reconsider Lj1 = ( Line (G1,j1)) as FinSequence of ( TOP-REAL 2);

                              

                               A448: j2 in ( Seg ( width G1)) by A96, A446, ZFMISC_1: 87;

                              

                               A449: ( Seg ( len Lj1)) = ( dom Lj1) & ( len Lj1) = ( width G1) by FINSEQ_1:def 3, MATRIX_0:def 7;

                              then (Lj1 /. j2) = (Lj1 . j2) by A448, PARTFUN1:def 6;

                              then (f /. (k + 1)) = (Lj1 /. j2) by A447, A448, MATRIX_0:def 7;

                              then

                               A450: (f /. (k + 1)) in ( rng Lj1) by A448, A449, PARTFUN2: 2;

                              

                               A451: j1 in ( dom G1) by A96, A446, ZFMISC_1: 87;

                              then

                               A452: j1 = m by A441, A450, GOBOARD1: 3;

                               0 < k by A443;

                              then

                               A453: ( 0 + 1) <= k by NAT_1: 13;

                              then

                               A454: k in ( dom f) by A445, FINSEQ_3: 25;

                              then

                              consider i1,i2 be Nat such that

                               A455: [i1, i2] in ( Indices G1) and

                               A456: (f /. k) = (G1 * (i1,i2)) by A174;

                              reconsider Li1 = ( Line (G1,i1)) as FinSequence of ( TOP-REAL 2);

                              

                               A457: i2 in ( Seg ( width G1)) by A96, A455, ZFMISC_1: 87;

                              

                               A458: ( Seg ( len Li1)) = ( dom Li1) & ( len Li1) = ( width G1) by FINSEQ_1:def 3, MATRIX_0:def 7;

                              then (Li1 /. i2) = (Li1 . i2) by A457, PARTFUN1:def 6;

                              then (f /. k) = (Li1 /. i2) by A456, A457, MATRIX_0:def 7;

                              then

                               A459: (f /. k) in ( rng Li1) by A457, A458, PARTFUN2: 2;

                              

                               A460: i1 in ( dom G1) by A96, A455, ZFMISC_1: 87;

                              then

                               A461: i1 <= ma by A439, A453, A445, A459, FINSEQ_3: 25;

                              now

                                per cases by A461, XXREAL_0: 1;

                                  case

                                   A462: ma = i1;

                                  

                                   A463: (w + 1) <= (w + k) by A453, XREAL_1: 7;

                                  

                                   A464: (f /. k) = (f1 /. (w + k)) & (f1 /. (w + k)) = (g1 /. (w + k)) by A170, A155, A157, A454;

                                  then ma1 <> (w + k) by A39, A41, A46, A95, A459, A462, GOBOARD1: 3;

                                  then ma1 < (w + k) by A463, XXREAL_0: 1;

                                  then

                                   A465: mi1 <= (w + k) by A130, A170, A157, A454, A459, A462, A464;

                                  (w + k) <= mi1 by A155, A156, A445, XREAL_1: 7;

                                  then (w + k) = mi1 by A465, XXREAL_0: 1;

                                  hence contradiction by A155, A444, NAT_1: 13;

                                end;

                                  case

                                   A466: i1 < ma;

                                  now

                                    per cases by A350, A440, A454, A460, A459, GOBOARD1: 27;

                                      suppose (f /. (k + 1)) in ( rng ( Line (G1,i1)));

                                      hence thesis by A441, A460, A466, GOBOARD1: 3;

                                    end;

                                      suppose for l be Nat st (f /. (k + 1)) in ( rng ( Line (G1,l))) & l in ( dom G1) holds |.(i1 - l).| = 1;

                                      then

                                       A467: |.(i1 - j1).| = 1 by A451, A450;

                                      now

                                        per cases by A467, SEQM_3: 41;

                                          suppose j1 < i1 & i1 = (j1 + 1);

                                          hence thesis by A452, A466, XXREAL_0: 2;

                                        end;

                                          suppose i1 < j1 & j1 = (i1 + 1);

                                          hence thesis by A452, A466, NAT_1: 13;

                                        end;

                                      end;

                                      hence thesis;

                                    end;

                                  end;

                                  hence thesis;

                                end;

                              end;

                              hence thesis;

                            end;

                          end;

                          hence thesis;

                        end;

                        

                         A468: ( Seg ( len h1)) = ( dom h1) by FINSEQ_1:def 3;

                         A469:

                        now

                          let n;

                          

                           A470: n <= (n + ma) by NAT_1: 11;

                          assume

                           A471: n in ( dom h2);

                          then n <= l2 by A421, FINSEQ_3: 25;

                          then

                           A472: (ma + n) <= (ma + l2) by XREAL_1: 7;

                          1 <= n by A471, FINSEQ_3: 25;

                          then 1 <= (n + ma) by A470, XXREAL_0: 2;

                          hence (ma + n) in ( dom G1) by A472, FINSEQ_3: 25;

                        end;

                         A473:

                        now

                          let n;

                          assume

                           A474: n in ( dom h2);

                          reconsider m = (ma + n), K2 as Nat;

                          take m, K2;

                          (ma + n) in ( dom G1) by A469, A474;

                          hence [m, K2] in ( Indices G1) & (h2 /. n) = (G1 * (m,K2)) by A96, A365, A355, A421, A474, ZFMISC_1: 87;

                        end;

                         A475:

                        now

                          let n;

                          assume that

                           A476: n in ( dom h2) and

                           A477: (n + 1) in ( dom h2);

                          (ma + (n + 1)) in ( dom G1) by A469, A477;

                          then

                           A478: [((ma + n) + 1), K2] in ( Indices G1) by A96, A365, A355, ZFMISC_1: 87;

                          let i1,i2,j1,j2 be Nat;

                          assume that

                           A479: [i1, i2] in ( Indices G1) and

                           A480: [j1, j2] in ( Indices G1) and

                           A481: (h2 /. n) = (G1 * (i1,i2)) and

                           A482: (h2 /. (n + 1)) = (G1 * (j1,j2));

                          (h2 /. (n + 1)) = (G1 * ((ma + (n + 1)),K2)) by A421, A477;

                          then

                           A483: j1 = ((ma + n) + 1) & j2 = K2 by A478, A480, A482, GOBOARD1: 5;

                          (ma + n) in ( dom G1) by A469, A476;

                          then

                           A484: [(ma + n), K2] in ( Indices G1) by A96, A365, A355, ZFMISC_1: 87;

                          (h2 /. n) = (G1 * ((ma + n),K2)) by A421, A476;

                          then i1 = (ma + n) & i2 = K2 by A484, A479, A481, GOBOARD1: 5;

                          

                          hence ( |.(i1 - j1).| + |.(i2 - j2).|) = ( |.(((ma + n) - (ma + n)) + ( - 1)).| + 0 ) by A483, ABSVALUE: 2

                          .= |.1.| by COMPLEX1: 52

                          .= 1 by ABSVALUE:def 1;

                        end;

                        

                         A485: ( Seg ( len h2)) = ( dom h2) by FINSEQ_1:def 3;

                        

                         A486: pl <= ( len g) by A363, FINSEQ_3: 25;

                        

                         A487: 1 <= pl by A363, FINSEQ_3: 25;

                        

                         A488: pl <> pf by A39, A41, A95, A359, A363, GOBOARD1: 3;

                        now

                          per cases by A488, XXREAL_0: 1;

                            suppose pf < pl;

                            then pf < ( len g) by A486, XXREAL_0: 2;

                            then 1 < ( len g) by A364, XXREAL_0: 2;

                            hence (1 + 1) <= ( len g) by NAT_1: 13;

                          end;

                            suppose pf > pl;

                            then pl < ( len g) by A418, XXREAL_0: 2;

                            then 1 < ( len g) by A487, XXREAL_0: 2;

                            hence (1 + 1) <= ( len g) by NAT_1: 13;

                          end;

                        end;

                        then 1 <= (( len g) - 1) by XREAL_1: 19;

                        then

                         A489: lg in ( dom g) by A356, FINSEQ_3: 25;

                        

                         A490: PP[ 0 ] by FINSEQ_3: 25;

                        

                         A491: for n holds PP[n] from NAT_1:sch 2( A490, A438);

                        

                         A492: (( rng h2) /\ ( rng tt)) = {}

                        proof

                          set x = the Element of (( rng h2) /\ ( rng tt));

                          assume

                           A493: not thesis;

                          then x in ( rng h2) by XBOOLE_0:def 4;

                          then

                          consider i2 be Element of NAT such that

                           A494: i2 in ( dom h2) and

                           A495: (h2 /. i2) = x by PARTFUN2: 2;

                          ( 0 + 1) <= i2 by A494, FINSEQ_3: 25;

                          then

                           A496: 0 < i2;

                          (ma + i2) in ( dom G1) by A469, A494;

                          then

                           A497: [(ma + i2), K2] in ( Indices G1) by A96, A365, A355, ZFMISC_1: 87;

                          x in ( rng tt) by A493, XBOOLE_0:def 4;

                          then x in ( rng t) by A354;

                          then

                          consider i1 be Element of NAT such that

                           A498: i1 in ( dom f) and

                           A499: (f /. i1) = x by A351, PARTFUN2: 2;

                          consider n1,n2 be Nat such that

                           A500: [n1, n2] in ( Indices G1) and

                           A501: (f /. i1) = (G1 * (n1,n2)) by A174, A498;

                          reconsider Ln1 = ( Line (G1,n1)) as FinSequence of ( TOP-REAL 2);

                          

                           A502: n2 in ( Seg ( width G1)) by A96, A500, ZFMISC_1: 87;

                          

                           A503: ( Seg ( len Ln1)) = ( dom Ln1) & ( len Ln1) = ( width G1) by FINSEQ_1:def 3, MATRIX_0:def 7;

                          then (Ln1 /. n2) = (Ln1 . n2) by A502, PARTFUN1:def 6;

                          then (f /. i1) = (Ln1 /. n2) by A501, A502, MATRIX_0:def 7;

                          then

                           A504: (f /. i1) in ( rng Ln1) by A502, A503, PARTFUN2: 2;

                          

                           A505: n1 in ( dom G1) by A96, A500, ZFMISC_1: 87;

                          x = (G1 * ((ma + i2),K2)) by A421, A494, A495;

                          then (ma + i2) = n1 by A499, A500, A501, A497, GOBOARD1: 5;

                          hence contradiction by A491, A498, A505, A504, A496, XREAL_1: 29;

                        end;

                        1 <= ( len g) by A13, GOBOARD1: 22;

                        then

                         A506: ( len g) in ( dom g) by FINSEQ_3: 25;

                        

                         A507: ( dom g) c= ( dom g2) by A23, A24, A16, A17, FINSEQ_1: 5;

                        now

                          consider i2 be Element of NAT such that

                           A508: i2 in ( dom C) and

                           A509: (C /. i2) = (g /. ( len g)) by A28, PARTFUN2: 2;

                          

                           A510: ( dom C) = ( Seg ( len C)) by FINSEQ_1:def 3

                          .= ( Seg ( len G1)) by MATRIX_0:def 8

                          .= ( dom G1) by FINSEQ_1:def 3;

                          then

                           A511: [i2, ( width G1)] in ( Indices G1) by A73, A96, A508, ZFMISC_1: 87;

                          (C /. i2) = (C . i2) by A508, PARTFUN1:def 6;

                          then

                           A512: (g /. ( len g)) = (G1 * (i2,( width G1))) by A508, A509, A510, MATRIX_0:def 8;

                          assume

                           A513: pl = ( len g);

                          consider n1,n2 be Nat such that

                           A514: [n1, n2] in ( Indices G1) and

                           A515: (g /. lg) = (G1 * (n1,n2)) by A15, A489, GOBOARD1:def 9;

                          

                           A516: n1 in ( dom G1) by A96, A514, ZFMISC_1: 87;

                          

                           A517: n2 in ( Seg ( width G1)) by A96, A514, ZFMISC_1: 87;

                           [ma, K2] in ( Indices G1) by A41, A96, A365, A355, ZFMISC_1: 87;

                          then i2 = ma by A420, A513, A512, A511, GOBOARD1: 5;

                          then

                           A518: ( |.(n1 - ma).| + |.(n2 - ( width G1)).|) = 1 by A15, A489, A506, A360, A512, A511, A514, A515, GOBOARD1:def 9;

                          now

                            per cases by A518, SEQM_3: 42;

                              suppose

                               A519: |.(n1 - ma).| = 1 & n2 = ( width G1);

                              

                               A520: ( dom C) = ( Seg ( len C)) by FINSEQ_1:def 3

                              .= ( Seg ( len G1)) by MATRIX_0:def 8

                              .= ( dom G1) by FINSEQ_1:def 3;

                              then (C /. n1) = (C . n1) by A516, PARTFUN1:def 6;

                              then (g /. lg) = (C /. n1) by A515, A516, A519, MATRIX_0:def 8;

                              then

                               A521: (g /. lg) in ( rng C) by A516, A520, PARTFUN2: 2;

                              (g /. lg) = (g2 /. lg) by A13, A24, A17, A489, FINSEQ_4: 71;

                              hence contradiction by A13, A17, A489, A507, A521, XREAL_1: 44;

                            end;

                              suppose

                               A522: |.(n2 - ( width G1)).| = 1 & n1 = ma;

                              ( len Lma) = ( width G1) by MATRIX_0:def 7;

                              then

                               A523: n2 in ( dom Lma) by A517, FINSEQ_1:def 3;

                              then (La /. n2) = (Lma . n2) by PARTFUN1:def 6;

                              then (g /. lg) = (Lma /. n2) by A515, A517, A522, MATRIX_0:def 7;

                              then (g /. lg) in ( rng Lma) by A523, PARTFUN2: 2;

                              hence contradiction by A363, A489, A513, XREAL_1: 44;

                            end;

                          end;

                          hence contradiction;

                        end;

                        then

                         A524: pl < ( len g) by A486, XXREAL_0: 1;

                        ( len C) = ( len G1) by MATRIX_0:def 8;

                        

                        then

                         A525: ( dom C) = ( Seg ( len G1)) by FINSEQ_1:def 3

                        .= ( dom G1) by FINSEQ_1:def 3;

                        

                         A526: (Li /. K1) = (Li . K1) by A367, PARTFUN1:def 6;

                        then

                         A527: (g /. pf) = (G1 * (mi,K1)) by A367, A368, A400, MATRIX_0:def 7;

                        now

                          consider i2 be Element of NAT such that

                           A528: i2 in ( dom C) and

                           A529: (C /. i2) = (g /. ( len g)) by A28, PARTFUN2: 2;

                          (C /. i2) = (C . i2) by A528, PARTFUN1:def 6;

                          then

                           A530: (g /. ( len g)) = (G1 * (i2,( width G1))) by A525, A528, A529, MATRIX_0:def 8;

                          

                           A531: [i2, ( width G1)] in ( Indices G1) by A73, A96, A525, A528, ZFMISC_1: 87;

                          assume

                           A532: pf = ( len g);

                          consider n1,n2 be Nat such that

                           A533: [n1, n2] in ( Indices G1) and

                           A534: (g /. lg) = (G1 * (n1,n2)) by A15, A489, GOBOARD1:def 9;

                          

                           A535: n1 in ( dom G1) by A96, A533, ZFMISC_1: 87;

                          

                           A536: n2 in ( Seg ( width G1)) by A96, A533, ZFMISC_1: 87;

                           [mi, K1] in ( Indices G1) by A39, A96, A367, A400, ZFMISC_1: 87;

                          then i2 = mi by A527, A532, A530, A531, GOBOARD1: 5;

                          then

                           A537: ( |.(n1 - mi).| + |.(n2 - ( width G1)).|) = 1 by A15, A489, A506, A360, A530, A531, A533, A534, GOBOARD1:def 9;

                          now

                            per cases by A537, SEQM_3: 42;

                              suppose

                               A538: |.(n1 - mi).| = 1 & n2 = ( width G1);

                              

                               A539: ( dom C) = ( Seg ( len C)) by FINSEQ_1:def 3

                              .= ( Seg ( len G1)) by MATRIX_0:def 8

                              .= ( dom G1) by FINSEQ_1:def 3;

                              then (C /. n1) = (C . n1) by A535, PARTFUN1:def 6;

                              then (g /. lg) = (C /. n1) by A534, A535, A538, MATRIX_0:def 8;

                              then

                               A540: (g /. lg) in ( rng C) by A535, A539, PARTFUN2: 2;

                              (g /. lg) = (g2 /. lg) by A13, A24, A17, A489, FINSEQ_4: 71;

                              hence contradiction by A13, A17, A489, A507, A540, XREAL_1: 44;

                            end;

                              suppose

                               A541: |.(n2 - ( width G1)).| = 1 & n1 = mi;

                              ( len Li) = ( width G1) by MATRIX_0:def 7;

                              then

                               A542: n2 in ( dom Li) by A536, FINSEQ_1:def 3;

                              then (Li /. n2) = (Li . n2) by PARTFUN1:def 6;

                              then (g /. lg) = (Li /. n2) by A534, A536, A541, MATRIX_0:def 7;

                              then (g /. lg) in ( rng Li) by A542, PARTFUN2: 2;

                              hence contradiction by A359, A489, A532, XREAL_1: 44;

                            end;

                          end;

                          hence contradiction;

                        end;

                        then

                         A543: pf < ( len g) by A418, XXREAL_0: 1;

                        now

                          per cases by A488, XXREAL_0: 1;

                            suppose

                             A544: pf < pl;

                            pl <= (pl + 1) by NAT_1: 11;

                            then

                            reconsider LL = ((pl + 1) - pf) as Element of NAT by A544, INT_1: 5, XXREAL_0: 2;

                            reconsider w1 = (pf - 1) as Element of NAT by A364, INT_1: 5;

                            set F1 = (g | pl);

                            defpred P[ Nat, Element of ( TOP-REAL 2)] means $2 = (F1 /. (w1 + $1));

                            

                             A545: for n be Nat st n in ( Seg LL) holds ex p st P[n, p];

                            consider F be FinSequence of ( TOP-REAL 2) such that

                             A546: ( len F) = LL & for n be Nat st n in ( Seg LL) holds P[n, (F /. n)] from FINSEQ_4:sch 1( A545);

                            set hf = (h1 ^ F);

                            set FF = ((h1 ^ F) ^ h2);

                            

                             A547: ( Seg ( len F)) = ( dom F) by FINSEQ_1:def 3;

                            

                             A548: for n st n in ( Seg LL) holds (F1 /. (w1 + n)) = (g /. (w1 + n)) & (w1 + n) in ( dom g)

                            proof

                              let n such that

                               A549: n in ( Seg LL);

                              n <= LL by A549, FINSEQ_1: 1;

                              then (n + pf) <= (LL + pf) by XREAL_1: 7;

                              then

                               A550: ((n + pf) - 1) <= pl by XREAL_1: 20;

                              1 <= n by A549, FINSEQ_1: 1;

                              then ( 0 + 1) <= (w1 + n) by XREAL_1: 7;

                              then (w1 + n) in ( Seg pl) by A550, FINSEQ_1: 1;

                              hence thesis by A363, FINSEQ_4: 71;

                            end;

                            

                             A551: ( rng F) c= ( rng g2)

                            proof

                              let x be object;

                              assume x in ( rng F);

                              then

                              consider n be Element of NAT such that

                               A552: n in ( dom F) and

                               A553: x = (F /. n) by PARTFUN2: 2;

                              (F /. n) = (F1 /. (w1 + n)) by A546, A547, A552;

                              then

                               A554: (F /. n) = (g /. (w1 + n)) by A548, A546, A547, A552;

                              (w1 + n) in ( dom g) by A548, A546, A547, A552;

                              then x in ( rng g) by A553, A554, PARTFUN2: 2;

                              hence thesis by A18;

                            end;

                            (pf + 1) <= pl by A544, NAT_1: 13;

                            then (pf + 1) <= (pl + 1) by NAT_1: 13;

                            then

                             A555: 1 <= LL by XREAL_1: 19;

                             A556:

                            now

                              let i1,i2,j1,j2 be Nat;

                              assume that

                               A557: [i1, i2] in ( Indices G1) and

                               A558: [j1, j2] in ( Indices G1) and

                               A559: (hf /. ( len hf)) = (G1 * (i1,i2)) and

                               A560: (h2 /. 1) = (G1 * (j1,j2)) and ( len hf) in ( dom hf) and

                               A561: 1 in ( dom h2);

                              (ma + 1) in ( dom G1) by A469, A561;

                              then

                               A562: [(ma + 1), K2] in ( Indices G1) by A96, A365, A355, ZFMISC_1: 87;

                              

                               A563: [ma, K2] in ( Indices G1) by A41, A96, A365, A355, ZFMISC_1: 87;

                              

                               A564: ( len F) in ( dom F) by A546, A547, A555, FINSEQ_1: 1;

                              (hf /. ( len hf)) = (hf /. (( len h1) + ( len F))) by FINSEQ_1: 22

                              .= (F /. ( len F)) by A564, FINSEQ_4: 69

                              .= (F1 /. (w1 + LL)) by A546, A547, A564

                              .= (G1 * (ma,K2)) by A420, A548, A546, A547, A564;

                              then

                               A565: i1 = ma & i2 = K2 by A557, A559, A563, GOBOARD1: 5;

                              (h2 /. 1) = (G1 * ((ma + 1),K2)) by A421, A561;

                              then j1 = (ma + 1) & j2 = K2 by A558, A560, A562, GOBOARD1: 5;

                              

                              hence ( |.(i1 - j1).| + |.(i2 - j2).|) = ( |.(ma - (ma + 1)).| + 0 ) by A565, ABSVALUE: 2

                              .= |.( - ((ma + 1) - ma)).|

                              .= |.1.| by COMPLEX1: 52

                              .= 1 by ABSVALUE:def 1;

                            end;

                            

                             A566: ( rng FF) = (( rng (h1 ^ F)) \/ ( rng h2)) by FINSEQ_1: 31

                            .= ((( rng h1) \/ ( rng F)) \/ ( rng h2)) by FINSEQ_1: 31;

                            

                             A567: for k st k in ( Seg ( width G1)) & (( rng F) /\ ( rng ( Col (G1,k)))) = {} holds (( rng FF) /\ ( rng ( Col (G1,k)))) = {}

                            proof

                              

                               A568: ( len ( Col (G1,K2))) = ( len G1) by MATRIX_0:def 8;

                              

                               A569: ( len ( Col (G1,K1))) = ( len G1) by MATRIX_0:def 8;

                              let k;

                              assume that

                               A570: k in ( Seg ( width G1)) and

                               A571: (( rng F) /\ ( rng ( Col (G1,k)))) = {} ;

                              set gg = ( Col (G1,k));

                              assume

                               A572: (( rng FF) /\ ( rng gg)) <> {} ;

                              set x = the Element of (( rng FF) /\ ( rng gg));

                              ( rng FF) = (( rng F) \/ (( rng h1) \/ ( rng h2))) by A566, XBOOLE_1: 4;

                              

                              then

                               A573: (( rng FF) /\ ( rng gg)) = ( {} \/ ((( rng h1) \/ ( rng h2)) /\ ( rng gg))) by A571, XBOOLE_1: 23

                              .= ((( rng h1) /\ ( rng gg)) \/ (( rng h2) /\ ( rng gg))) by XBOOLE_1: 23;

                              now

                                per cases by A572, A573, XBOOLE_0:def 3;

                                  suppose

                                   A574: x in (( rng h1) /\ ( rng gg));

                                  then x in ( rng h1) by XBOOLE_0:def 4;

                                  then

                                  consider i be Element of NAT such that

                                   A575: i in ( dom h1) and

                                   A576: x = (h1 /. i) by PARTFUN2: 2;

                                  

                                   A577: x = (G1 * (i,K1)) by A369, A575, A576;

                                  reconsider y = x as Point of ( TOP-REAL 2) by A576;

                                  

                                   A578: (Lmi /. K1) = (Lmi . K1) by A367, PARTFUN1:def 6;

                                  

                                   A579: x in ( rng gg) by A574, XBOOLE_0:def 4;

                                  

                                   A580: ( dom CK1) = ( Seg ( len G1)) by A569, FINSEQ_1:def 3

                                  .= ( dom G1) by FINSEQ_1:def 3;

                                  then

                                   A581: (CK1 /. mi) = (CK1 . mi) by A39, PARTFUN1:def 6;

                                  

                                   A582: i in ( dom CK1) by A401, A575, A580;

                                  (CK1 /. i) = (CK1 . i) by A401, A575, A580, PARTFUN1:def 6;

                                  then y = (CK1 /. i) by A577, A580, A582, MATRIX_0:def 8;

                                  then y in ( rng CK1) by A582, PARTFUN2: 2;

                                  then

                                   A583: K1 = k by A367, A400, A570, A579, GOBOARD1: 4;

                                  

                                   A584: 1 in ( Seg LL) by A555, FINSEQ_1: 1;

                                  then (F /. 1) = (F1 /. (w1 + 1)) & (F1 /. (w1 + 1)) = (g /. (w1 + 1)) by A548, A546;

                                  then (F /. 1) = (CK1 /. mi) by A39, A367, A368, A400, A578, A581, MATRIX_0: 42;

                                  then

                                   A585: (F /. 1) in ( rng ( Col (G1,k))) by A39, A580, A583, PARTFUN2: 2;

                                  (F /. 1) in ( rng F) by A546, A547, A584, PARTFUN2: 2;

                                  hence contradiction by A571, A585, XBOOLE_0:def 4;

                                end;

                                  suppose

                                   A586: x in (( rng h2) /\ ( rng gg));

                                  then x in ( rng h2) by XBOOLE_0:def 4;

                                  then

                                  consider i be Element of NAT such that

                                   A587: i in ( dom h2) and

                                   A588: x = (h2 /. i) by PARTFUN2: 2;

                                  

                                   A589: x = (G1 * ((ma + i),K2)) by A421, A587, A588;

                                  reconsider y = x as Point of ( TOP-REAL 2) by A588;

                                  

                                   A590: (Lma /. K2) = (Lma . K2) by A365, PARTFUN1:def 6;

                                  

                                   A591: x in ( rng gg) by A586, XBOOLE_0:def 4;

                                  

                                   A592: ( dom CK2) = ( Seg ( len G1)) by A568, FINSEQ_1:def 3

                                  .= ( dom G1) by FINSEQ_1:def 3;

                                  then

                                   A593: (CK2 /. ma) = (CK2 . ma) by A41, PARTFUN1:def 6;

                                  

                                   A594: (ma + i) in ( dom CK2) by A469, A587, A592;

                                  (CK2 /. (ma + i)) = (CK2 . (ma + i)) by A469, A587, A592, PARTFUN1:def 6;

                                  then y = (CK2 /. (ma + i)) by A589, A592, A594, MATRIX_0:def 8;

                                  then y in ( rng CK2) by A594, PARTFUN2: 2;

                                  then

                                   A595: K2 = k by A365, A355, A570, A591, GOBOARD1: 4;

                                  

                                   A596: LL in ( Seg LL) by A555, FINSEQ_1: 1;

                                  then (F /. LL) = (F1 /. (w1 + LL)) & (F1 /. (w1 + LL)) = (g /. (w1 + LL)) by A548, A546;

                                  then (F /. LL) = (CK2 /. ma) by A41, A365, A366, A355, A590, A593, MATRIX_0: 42;

                                  then

                                   A597: (F /. LL) in ( rng ( Col (G1,k))) by A41, A592, A595, PARTFUN2: 2;

                                  (F /. LL) in ( rng F) by A546, A547, A596, PARTFUN2: 2;

                                  hence contradiction by A571, A597, XBOOLE_0:def 4;

                                end;

                              end;

                              hence contradiction;

                            end;

                            (( rng F) /\ ( rng C)) = {}

                            proof

                              reconsider w = w1 as Nat;

                              set x = the Element of (( rng F) /\ ( rng C));

                              assume

                               A598: not thesis;

                              then

                               A599: x in ( rng C) by XBOOLE_0:def 4;

                              x in ( rng F) by A598, XBOOLE_0:def 4;

                              then

                              consider i1 be Element of NAT such that

                               A600: i1 in ( dom F) and

                               A601: (F /. i1) = x by PARTFUN2: 2;

                              

                               A602: ( Seg ( len F)) = ( dom F) by FINSEQ_1:def 3;

                              then i1 <= LL by A546, A600, FINSEQ_1: 1;

                              then

                               A603: (w + i1) <= (w + LL) by XREAL_1: 7;

                              

                               A604: (w1 + i1) in ( dom g) by A548, A546, A600, A602;

                              then

                               A605: (w + i1) in ( dom g2) by A13, A24, A17, FINSEQ_4: 71;

                              (F /. i1) = (F1 /. (w1 + i1)) & (F1 /. (w1 + i1)) = (g /. (w1 + i1)) by A548, A546, A600, A602;

                              then (g2 /. (w + i1)) in ( rng C) by A13, A24, A17, A599, A601, A604, FINSEQ_4: 71;

                              then m <= (w + i1) by A13, A605;

                              hence contradiction by A17, A524, A603, XXREAL_0: 2;

                            end;

                            then (( rng FF) /\ ( rng ( Col (G1,( width G1))))) = {} by A73, A567;

                            then

                             A606: ( rng FF) misses ( rng ( Col (G1,( width G1)))) by XBOOLE_0:def 7;

                            now

                              reconsider w = w1 as Nat;

                              let n;

                              assume

                               A607: n in ( dom F);

                              then (w1 + n) in ( dom g) by A548, A546, A547;

                              then

                              consider i, j such that

                               A608: [i, j] in ( Indices G1) & (g /. (w + n)) = (G1 * (i,j)) by A15, GOBOARD1:def 9;

                              take i, j;

                              (F /. n) = (F1 /. (w1 + n)) by A546, A547, A607;

                              hence [i, j] in ( Indices G1) & (F /. n) = (G1 * (i,j)) by A548, A546, A547, A607, A608;

                            end;

                            then for n st n in ( dom (h1 ^ F)) holds ex i, j st [i, j] in ( Indices G1) & ((h1 ^ F) /. n) = (G1 * (i,j)) by A406, GOBOARD1: 23;

                            then

                             A609: for n st n in ( dom FF) holds ex i, j st [i, j] in ( Indices G1) & (FF /. n) = (G1 * (i,j)) by A473, GOBOARD1: 23;

                             A610:

                            now

                              

                               A611: [mi, K1] in ( Indices G1) by A39, A96, A367, A400, ZFMISC_1: 87;

                              let i1,i2,j1,j2 be Nat;

                              assume that

                               A612: [i1, i2] in ( Indices G1) and

                               A613: [j1, j2] in ( Indices G1) and

                               A614: (h1 /. ( len h1)) = (G1 * (i1,i2)) and

                               A615: (F /. 1) = (G1 * (j1,j2)) and

                               A616: ( len h1) in ( dom h1) and

                               A617: 1 in ( dom F);

                              (F /. 1) = (F1 /. (w1 + 1)) by A546, A547, A617;

                              

                              then (F /. 1) = (g /. (w1 + 1)) by A548, A546, A547, A617

                              .= (G1 * (mi,K1)) by A367, A368, A400, A526, MATRIX_0:def 7;

                              then

                               A618: j1 = mi & j2 = K1 by A613, A615, A611, GOBOARD1: 5;

                              l1 in ( dom G1) by A369, A401, A616;

                              then

                               A619: [l1, K1] in ( Indices G1) by A96, A367, A400, ZFMISC_1: 87;

                              (h1 /. ( len h1)) = (G1 * (l1,K1)) by A369, A616;

                              then i1 = l1 & i2 = K1 by A612, A614, A619, GOBOARD1: 5;

                              

                              hence ( |.(i1 - j1).| + |.(i2 - j2).|) = ( |.((mi - 1) - mi).| + 0 ) by A618, ABSVALUE: 2

                              .= |.( - 1).|

                              .= |.1.| by COMPLEX1: 52

                              .= 1 by ABSVALUE:def 1;

                            end;

                            now

                              let n;

                              assume that

                               A620: n in ( dom F) and

                               A621: (n + 1) in ( dom F);

                              (F /. n) = (F1 /. (w1 + n)) by A546, A547, A620;

                              then

                               A622: (F /. n) = (g /. (w1 + n)) by A548, A546, A547, A620;

                              (F /. (n + 1)) = (F1 /. (w1 + (n + 1))) by A546, A547, A621;

                              then

                               A623: ((w1 + n) + 1) in ( dom g) & (F /. (n + 1)) = (g /. ((w1 + n) + 1)) by A548, A546, A547, A621;

                              let i1,i2,j1,j2 be Nat;

                              assume

                               A624: [i1, i2] in ( Indices G1) & [j1, j2] in ( Indices G1) & (F /. n) = (G1 * (i1,i2)) & (F /. (n + 1)) = (G1 * (j1,j2));

                              (w1 + n) in ( dom g) by A548, A546, A547, A620;

                              hence ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A15, A622, A623, A624, GOBOARD1:def 9;

                            end;

                            then for n st n in ( dom (h1 ^ F)) & (n + 1) in ( dom (h1 ^ F)) holds for i1,i2,j1,j2 be Nat st [i1, i2] in ( Indices G1) & [j1, j2] in ( Indices G1) & ((h1 ^ F) /. n) = (G1 * (i1,i2)) & ((h1 ^ F) /. (n + 1)) = (G1 * (j1,j2)) holds ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A408, A610, GOBOARD1: 24;

                            then for n st n in ( dom FF) & (n + 1) in ( dom FF) holds for i1,i2,j1,j2 be Nat st [i1, i2] in ( Indices G1) & [j1, j2] in ( Indices G1) & (FF /. n) = (G1 * (i1,i2)) & (FF /. (n + 1)) = (G1 * (j1,j2)) holds ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A475, A556, GOBOARD1: 24;

                            then FF is_sequence_on G1 by A609, GOBOARD1:def 9;

                            then

                             A625: FF is_sequence_on D by A73, A152, A606, GOBOARD1: 25;

                            set x = the Element of (( rng FF) /\ ( rng tt));

                            

                             A626: ( 0 + 1) <= (( len F) + (( len h1) + ( len h2))) by A546, A555, XREAL_1: 7;

                             A627:

                            now

                              per cases ;

                                suppose

                                 A628: mi = 1;

                                

                                 A629: pf in ( Seg pl) by A364, A544, FINSEQ_1: 1;

                                

                                 A630: 1 in ( Seg LL) by A555, FINSEQ_1: 1;

                                h1 = {} by A369, A628;

                                then FF = (F ^ h2) by FINSEQ_1: 34;

                                

                                then (FF /. 1) = (F /. 1) by A546, A547, A630, FINSEQ_4: 68

                                .= (F1 /. (w1 + 1)) by A546, A630

                                .= (g /. pf) by A363, A629, FINSEQ_4: 71;

                                hence (FF /. 1) in ( rng ( Line (G1,1))) by A359, A628;

                              end;

                                suppose

                                 A631: mi <> 1;

                                1 <= mi by A39, FINSEQ_3: 25;

                                then 1 < mi by A631, XXREAL_0: 1;

                                then (1 + 1) <= mi by NAT_1: 13;

                                then

                                 A632: 1 <= l1 by XREAL_1: 19;

                                then

                                 A633: 1 in ( Seg l1) by FINSEQ_1: 1;

                                ( len ( Line (G1,1))) = ( width G1) by MATRIX_0:def 7;

                                then

                                 A634: K1 in ( dom L1) by A367, A400, FINSEQ_1:def 3;

                                then

                                 A635: (L1 /. K1) = (L1 . K1) by PARTFUN1:def 6;

                                ( len (h1 ^ F)) = (( len h1) + ( len F)) & 0 <= ( len F) by FINSEQ_1: 22;

                                then ( 0 + 1) <= ( len (h1 ^ F)) by A369, A632, XREAL_1: 7;

                                then 1 in ( dom (h1 ^ F)) by FINSEQ_3: 25;

                                

                                then (FF /. 1) = ((h1 ^ F) /. 1) by FINSEQ_4: 68

                                .= (h1 /. 1) by A369, A468, A633, FINSEQ_4: 68

                                .= (G1 * (1,K1)) by A369, A468, A633

                                .= (L1 /. K1) by A367, A400, A635, MATRIX_0:def 7;

                                hence (FF /. 1) in ( rng ( Line (G1,1))) by A634, PARTFUN2: 2;

                              end;

                            end;

                            

                             A636: (w1 + LL) = pl;

                             A637:

                            now

                              per cases ;

                                suppose

                                 A638: ma = ( len G1);

                                1 <= pl by A24, A363, FINSEQ_1: 1;

                                then

                                 A639: pl in ( Seg pl) by FINSEQ_1: 1;

                                

                                 A640: ( len F) in ( dom F) by A546, A555, FINSEQ_3: 25;

                                h2 = {} by A421, A638;

                                then

                                 A641: FF = (h1 ^ F) by FINSEQ_1: 34;

                                

                                then (FF /. ( len FF)) = (FF /. (( len h1) + ( len F))) by FINSEQ_1: 22

                                .= (F /. LL) by A546, A641, A640, FINSEQ_4: 69

                                .= (F1 /. pl) by A546, A547, A636, A640

                                .= (g /. pl) by A363, A639, FINSEQ_4: 71;

                                hence (FF /. ( len FF)) in ( rng ( Line (G1,( len G1)))) by A363, A638;

                              end;

                                suppose

                                 A642: ma <> ( len G1);

                                ma <= ( len G1) by A41, FINSEQ_3: 25;

                                then ma < ( len G1) by A642, XXREAL_0: 1;

                                then (ma + 1) <= ( len G1) by NAT_1: 13;

                                then

                                 A643: 1 <= l2 by XREAL_1: 19;

                                then

                                 A644: l2 in ( Seg l2) by FINSEQ_1: 1;

                                ( len ( Line (G1,( len G1)))) = ( width G1) by MATRIX_0:def 7;

                                then

                                 A645: K2 in ( dom Ll) by A365, A355, FINSEQ_1:def 3;

                                then

                                 A646: (Ll /. K2) = (Ll . K2) by PARTFUN1:def 6;

                                

                                 A647: ( len h2) in ( dom h2) by A421, A643, FINSEQ_3: 25;

                                (FF /. ( len FF)) = (FF /. (( len (h1 ^ F)) + ( len h2))) by FINSEQ_1: 22

                                .= (h2 /. l2) by A421, A647, FINSEQ_4: 69

                                .= (G1 * ((ma + l2),K2)) by A421, A485, A644

                                .= (Ll /. K2) by A365, A355, A646, MATRIX_0:def 7;

                                hence (FF /. ( len FF)) in ( rng ( Line (G1,( len G1)))) by A645, PARTFUN2: 2;

                              end;

                            end;

                            ( rng tt) c= ( rng f) by A351, A354;

                            then

                             A648: ( rng tt) c= ( rng g1) by A178;

                            

                             A649: ( len FF) = (( len (h1 ^ F)) + ( len h2)) by FINSEQ_1: 22

                            .= ((( len h1) + ( len F)) + ( len h2)) by FINSEQ_1: 22;

                            then 1 in ( dom FF) by A626, FINSEQ_3: 25;

                            then

                             A650: (FF /. 1) in ( rng ( Line (D,1))) by A73, A26, A152, A627, A606, MATRIX_0: 75;

                            ( len FF) in ( dom FF) by A649, A626, FINSEQ_3: 25;

                            then

                             A651: (FF /. ( len FF)) in ( rng ( Line (D,( len D)))) by A73, A27, A152, A153, A637, A606, MATRIX_0: 75;

                            ( width D) = k by A3, A73, MATRIX_0: 63;

                            then (( rng FF) /\ ( rng tt)) <> {} by A2, A92, A353, A649, A626, A625, A650, A651, A341;

                            then

                             A652: x in (( rng FF) /\ ( rng tt));

                            (( rng tt) /\ ( rng FF)) = (((( rng h1) \/ ( rng F)) /\ ( rng tt)) \/ {} ) by A492, A566, XBOOLE_1: 23

                            .= ( {} \/ (( rng F) /\ ( rng tt))) by A424, XBOOLE_1: 23

                            .= (( rng tt) /\ ( rng F));

                            then (( rng FF) /\ ( rng tt)) c= (( rng g1) /\ ( rng g2)) by A648, A551, XBOOLE_1: 27;

                            hence thesis by A652;

                          end;

                            suppose

                             A653: pl < pf;

                            pf <= (pf + 1) by NAT_1: 11;

                            then

                            reconsider LL = ((pf + 1) - pl) as Element of NAT by A653, INT_1: 5, XXREAL_0: 2;

                            set F1 = (g | pf);

                            defpred P[ Nat, Element of ( TOP-REAL 2)] means for k st k = ((pf + 1) - $1) holds $2 = (F1 /. k);

                            

                             A654: for n, k st n in ( Seg LL) & k = ((pf + 1) - n) holds (F1 /. k) = (g /. k) & k in ( dom g)

                            proof

                              let n, k;

                              assume that

                               A655: n in ( Seg LL) and

                               A656: k = ((pf + 1) - n);

                              

                               A657: n <= LL by A655, FINSEQ_1: 1;

                              1 <= n by A655, FINSEQ_1: 1;

                              then

                               A658: ((pf + 1) - n) <= ((pf + 1) - 1) by XREAL_1: 13;

                              LL <= ((pf + 1) - 0 ) by XREAL_1: 13;

                              then

                              reconsider w = ((pf + 1) - n) as Element of NAT by A657, INT_1: 5, XXREAL_0: 2;

                              ((pf + 1) - LL) <= ((pf + 1) - n) by A657, XREAL_1: 13;

                              then 1 <= ((pf + 1) - n) by A487, XXREAL_0: 2;

                              then w in ( Seg pf) by A658, FINSEQ_1: 1;

                              hence thesis by A359, A656, FINSEQ_4: 71;

                            end;

                            

                             A659: for n st n in ( Seg LL) holds ((pf + 1) - n) is Element of NAT

                            proof

                              let n;

                              

                               A660: LL <= ((pf + 1) - 0 ) by XREAL_1: 13;

                              assume n in ( Seg LL);

                              then n <= LL by FINSEQ_1: 1;

                              hence thesis by A660, INT_1: 5, XXREAL_0: 2;

                            end;

                            

                             A661: for n be Nat st n in ( Seg LL) holds ex p st P[n, p]

                            proof

                              let n be Nat;

                              assume

                               A662: n in ( Seg LL);

                              then

                              reconsider k = ((pf + 1) - n) as Nat by A659;

                              take (g /. k);

                              thus thesis by A654, A662;

                            end;

                            consider F be FinSequence of ( TOP-REAL 2) such that

                             A663: ( len F) = LL & for n be Nat st n in ( Seg LL) holds P[n, (F /. n)] from FINSEQ_4:sch 1( A661);

                            set hf = (h1 ^ F);

                            set FF = ((h1 ^ F) ^ h2);

                            

                             A664: ( Seg ( len F)) = ( dom F) by FINSEQ_1:def 3;

                            

                             A665: ( rng F) c= ( rng g2)

                            proof

                              let x be object;

                              assume x in ( rng F);

                              then

                              consider n be Element of NAT such that

                               A666: n in ( dom F) and

                               A667: x = (F /. n) by PARTFUN2: 2;

                              reconsider u = ((pf + 1) - n) as Nat by A659, A663, A664, A666;

                              (F /. n) = (F1 /. u) by A663, A664, A666;

                              then ((pf + 1) - n) in ( dom g) & (F /. n) = (g /. u) by A654, A663, A664, A666;

                              then x in ( rng g) by A667, PARTFUN2: 2;

                              hence thesis by A18;

                            end;

                            (pl + 1) <= pf by A653, NAT_1: 13;

                            then (pl + 1) <= (pf + 1) by NAT_1: 13;

                            then

                             A668: 1 <= LL by XREAL_1: 19;

                             A669:

                            now

                              reconsider u = ((pf + 1) - LL) as Nat;

                              let i1,i2,j1,j2 be Nat;

                              assume that

                               A670: [i1, i2] in ( Indices G1) and

                               A671: [j1, j2] in ( Indices G1) and

                               A672: (hf /. ( len hf)) = (G1 * (i1,i2)) and

                               A673: (h2 /. 1) = (G1 * (j1,j2)) and ( len hf) in ( dom hf) and

                               A674: 1 in ( dom h2);

                              (ma + 1) in ( dom G1) by A469, A674;

                              then

                               A675: [(ma + 1), K2] in ( Indices G1) by A96, A365, A355, ZFMISC_1: 87;

                              

                               A676: [ma, K2] in ( Indices G1) by A41, A96, A365, A355, ZFMISC_1: 87;

                              

                               A677: ( len F) in ( dom F) by A663, A668, FINSEQ_3: 25;

                              (hf /. ( len hf)) = (hf /. (( len h1) + ( len F))) by FINSEQ_1: 22

                              .= (F /. ( len F)) by A677, FINSEQ_4: 69

                              .= (F1 /. u) by A663, A664, A677

                              .= (g /. u) by A654, A663, A664, A677

                              .= (G1 * (ma,K2)) by A365, A366, A355, A419, MATRIX_0:def 7;

                              then

                               A678: i1 = ma & i2 = K2 by A670, A672, A676, GOBOARD1: 5;

                              (h2 /. 1) = (G1 * ((ma + 1),K2)) by A421, A674;

                              then j1 = (ma + 1) & j2 = K2 by A671, A673, A675, GOBOARD1: 5;

                              

                              hence ( |.(i1 - j1).| + |.(i2 - j2).|) = ( |.(ma - (ma + 1)).| + 0 ) by A678, ABSVALUE: 2

                              .= |.( - ((ma + 1) - ma)).|

                              .= |.1.| by COMPLEX1: 52

                              .= 1 by ABSVALUE:def 1;

                            end;

                            now

                              let n;

                              assume

                               A679: n in ( dom F);

                              then

                              reconsider w = ((pf + 1) - n) as Nat by A659, A663, A664;

                              

                               A680: (F /. n) = (F1 /. w) by A663, A664, A679;

                              then ((pf + 1) - n) in ( dom g) by A654, A663, A664, A679;

                              then

                              consider i, j such that

                               A681: [i, j] in ( Indices G1) & (g /. w) = (G1 * (i,j)) by A15, GOBOARD1:def 9;

                              take i, j;

                              thus [i, j] in ( Indices G1) & (F /. n) = (G1 * (i,j)) by A654, A663, A664, A679, A680, A681;

                            end;

                            then for n st n in ( dom (h1 ^ F)) holds ex i, j st [i, j] in ( Indices G1) & ((h1 ^ F) /. n) = (G1 * (i,j)) by A406, GOBOARD1: 23;

                            then

                             A682: for n st n in ( dom FF) holds ex i, j st [i, j] in ( Indices G1) & (FF /. n) = (G1 * (i,j)) by A473, GOBOARD1: 23;

                            set x = the Element of (( rng FF) /\ ( rng tt));

                            

                             A683: ( 0 + 1) <= (( len F) + (( len h1) + ( len h2))) by A663, A668, XREAL_1: 7;

                            

                             A684: ( rng FF) = (( rng (h1 ^ F)) \/ ( rng h2)) by FINSEQ_1: 31

                            .= ((( rng h1) \/ ( rng F)) \/ ( rng h2)) by FINSEQ_1: 31;

                            

                             A685: for k st k in ( Seg ( width G1)) & (( rng F) /\ ( rng ( Col (G1,k)))) = {} holds (( rng FF) /\ ( rng ( Col (G1,k)))) = {}

                            proof

                              

                               A686: ( len ( Col (G1,K2))) = ( len G1) by MATRIX_0:def 8;

                              

                               A687: ( len ( Col (G1,K1))) = ( len G1) by MATRIX_0:def 8;

                              let k;

                              assume that

                               A688: k in ( Seg ( width G1)) and

                               A689: (( rng F) /\ ( rng ( Col (G1,k)))) = {} ;

                              set gg = ( Col (G1,k));

                              assume

                               A690: (( rng FF) /\ ( rng gg)) <> {} ;

                              set x = the Element of (( rng FF) /\ ( rng gg));

                              ( rng FF) = (( rng F) \/ (( rng h1) \/ ( rng h2))) by A684, XBOOLE_1: 4;

                              

                              then

                               A691: (( rng FF) /\ ( rng gg)) = ( {} \/ ((( rng h1) \/ ( rng h2)) /\ ( rng gg))) by A689, XBOOLE_1: 23

                              .= ((( rng h1) /\ ( rng gg)) \/ (( rng h2) /\ ( rng gg))) by XBOOLE_1: 23;

                              now

                                per cases by A690, A691, XBOOLE_0:def 3;

                                  suppose

                                   A692: x in (( rng h1) /\ ( rng gg));

                                  then

                                   A693: x in ( rng gg) by XBOOLE_0:def 4;

                                  

                                   A694: 1 in ( Seg LL) by A668, FINSEQ_1: 1;

                                  ((pf + 1) - 1) = pf;

                                  then

                                   A695: (F /. 1) = (F1 /. pf) & (F1 /. pf) = (g /. pf) by A654, A663, A694;

                                  x in ( rng h1) by A692, XBOOLE_0:def 4;

                                  then

                                  consider i be Element of NAT such that

                                   A696: i in ( dom h1) and

                                   A697: x = (h1 /. i) by PARTFUN2: 2;

                                  

                                   A698: x = (G1 * (i,K1)) by A369, A696, A697;

                                  reconsider y = x as Point of ( TOP-REAL 2) by A697;

                                  

                                   A699: (Lmi /. K1) = (Lmi . K1) by A367, PARTFUN1:def 6;

                                  

                                   A700: ( dom CK1) = ( Seg ( len G1)) by A687, FINSEQ_1:def 3

                                  .= ( dom G1) by FINSEQ_1:def 3;

                                  then

                                   A701: i in ( dom CK1) by A401, A696;

                                  (CK1 /. i) = (CK1 . i) by A401, A696, A700, PARTFUN1:def 6;

                                  then y = (CK1 /. i) by A698, A700, A701, MATRIX_0:def 8;

                                  then y in ( rng CK1) by A701, PARTFUN2: 2;

                                  then

                                   A702: K1 = k by A367, A400, A688, A693, GOBOARD1: 4;

                                  (CK1 /. mi) = (CK1 . mi) by A39, A700, PARTFUN1:def 6;

                                  then (F /. 1) = (CK1 /. mi) by A39, A367, A368, A400, A699, A695, MATRIX_0: 42;

                                  then

                                   A703: (F /. 1) in ( rng ( Col (G1,k))) by A39, A700, A702, PARTFUN2: 2;

                                  (F /. 1) in ( rng F) by A663, A664, A694, PARTFUN2: 2;

                                  hence contradiction by A689, A703, XBOOLE_0:def 4;

                                end;

                                  suppose

                                   A704: x in (( rng h2) /\ ( rng gg));

                                  then x in ( rng h2) by XBOOLE_0:def 4;

                                  then

                                  consider i be Element of NAT such that

                                   A705: i in ( dom h2) and

                                   A706: x = (h2 /. i) by PARTFUN2: 2;

                                  

                                   A707: x = (G1 * ((ma + i),K2)) by A421, A705, A706;

                                  reconsider y = x as Point of ( TOP-REAL 2) by A706;

                                  

                                   A708: x in ( rng gg) by A704, XBOOLE_0:def 4;

                                  reconsider u = ((pf + 1) - LL) as Nat;

                                  

                                   A709: (Lma /. K2) = (Lma . K2) by A365, PARTFUN1:def 6;

                                  

                                   A710: ( dom CK2) = ( Seg ( len G1)) by A686, FINSEQ_1:def 3

                                  .= ( dom G1) by FINSEQ_1:def 3;

                                  then

                                   A711: (CK2 /. ma) = (CK2 . ma) by A41, PARTFUN1:def 6;

                                  

                                   A712: (ma + i) in ( dom CK2) by A469, A705, A710;

                                  (CK2 /. (ma + i)) = (CK2 . (ma + i)) by A469, A705, A710, PARTFUN1:def 6;

                                  then y = (CK2 /. (ma + i)) by A707, A710, A712, MATRIX_0:def 8;

                                  then y in ( rng CK2) by A712, PARTFUN2: 2;

                                  then

                                   A713: K2 = k by A365, A355, A688, A708, GOBOARD1: 4;

                                  

                                   A714: LL in ( Seg LL) by A668, FINSEQ_1: 1;

                                  then (F /. LL) = (F1 /. u) & (F1 /. u) = (g /. u) by A654, A663;

                                  then (F /. LL) = (CK2 /. ma) by A41, A365, A366, A355, A709, A711, MATRIX_0: 42;

                                  then

                                   A715: (F /. LL) in ( rng ( Col (G1,k))) by A41, A710, A713, PARTFUN2: 2;

                                  (F /. LL) in ( rng F) by A663, A664, A714, PARTFUN2: 2;

                                  hence contradiction by A689, A715, XBOOLE_0:def 4;

                                end;

                              end;

                              hence contradiction;

                            end;

                            (( rng F) /\ ( rng C)) = {}

                            proof

                              set x = the Element of (( rng F) /\ ( rng C));

                              assume

                               A716: not thesis;

                              then

                               A717: x in ( rng C) by XBOOLE_0:def 4;

                              x in ( rng F) by A716, XBOOLE_0:def 4;

                              then

                              consider i1 be Element of NAT such that

                               A718: i1 in ( dom F) and

                               A719: (F /. i1) = x by PARTFUN2: 2;

                              reconsider w = ((pf + 1) - i1) as Nat by A659, A663, A664, A718;

                              1 <= i1 by A718, FINSEQ_3: 25;

                              then

                               A720: w <= ((pf + 1) - 1) by XREAL_1: 13;

                              

                               A721: w in ( dom g) by A654, A663, A664, A718;

                              then

                               A722: w in ( dom g2) by A13, A24, A17, FINSEQ_4: 71;

                              (F /. i1) = (F1 /. w) & (F1 /. w) = (g /. w) by A654, A663, A664, A718;

                              then (g2 /. w) in ( rng C) by A13, A24, A17, A717, A719, A721, FINSEQ_4: 71;

                              then m <= w by A13, A722;

                              hence contradiction by A17, A543, A720, XXREAL_0: 2;

                            end;

                            then (( rng FF) /\ ( rng ( Col (G1,( width G1))))) = {} by A73, A685;

                            then

                             A723: ( rng FF) misses ( rng ( Col (G1,( width G1)))) by XBOOLE_0:def 7;

                             A724:

                            now

                              let n;

                              assume that

                               A725: n in ( dom F) and

                               A726: (n + 1) in ( dom F);

                              reconsider w3 = ((pf + 1) - n), w2 = ((pf + 1) - (n + 1)) as Element of NAT by A659, A663, A664, A725, A726;

                              (F /. n) = (F1 /. w3) by A663, A664, A725;

                              then

                               A727: ((pf + 1) - n) in ( dom g) & (F /. n) = (g /. w3) by A654, A663, A664, A725;

                              (F /. (n + 1)) = (F1 /. w2) by A663, A664, A726;

                              then

                               A728: ((pf + 1) - (n + 1)) in ( dom g) & (F /. (n + 1)) = (g /. w2) by A654, A663, A664, A726;

                              let i1,i2,j1,j2 be Nat;

                              assume

                               A729: [i1, i2] in ( Indices G1) & [j1, j2] in ( Indices G1) & (F /. n) = (G1 * (i1,i2)) & (F /. (n + 1)) = (G1 * (j1,j2));

                              (w2 + 1) = ((pf + 1) - n);

                              

                              hence 1 = ( |.(j1 - i1).| + |.(j2 - i2).|) by A15, A727, A728, A729, GOBOARD1:def 9

                              .= ( |.( - (i1 - j1)).| + |.( - (i2 - j2)).|)

                              .= ( |.(i1 - j1).| + |.( - (i2 - j2)).|) by COMPLEX1: 52

                              .= ( |.(i1 - j1).| + |.(i2 - j2).|) by COMPLEX1: 52;

                            end;

                            

                             A730: ((pf + 1) - 1) = pf;

                             A731:

                            now

                              per cases ;

                                suppose

                                 A732: mi = 1;

                                

                                 A733: pf in ( Seg pf) by A364, FINSEQ_1: 1;

                                

                                 A734: 1 in ( Seg LL) by A668, FINSEQ_1: 1;

                                h1 = {} by A369, A732;

                                then FF = (F ^ h2) by FINSEQ_1: 34;

                                

                                then (FF /. 1) = (F /. 1) by A663, A664, A734, FINSEQ_4: 68

                                .= (F1 /. pf) by A663, A730, A734

                                .= (g /. pf) by A359, A733, FINSEQ_4: 71;

                                hence (FF /. 1) in ( rng ( Line (G1,1))) by A359, A732;

                              end;

                                suppose

                                 A735: mi <> 1;

                                1 <= mi by A39, FINSEQ_3: 25;

                                then 1 < mi by A735, XXREAL_0: 1;

                                then (1 + 1) <= mi by NAT_1: 13;

                                then

                                 A736: 1 <= l1 by XREAL_1: 19;

                                then

                                 A737: 1 in ( Seg l1) by FINSEQ_1: 1;

                                ( len ( Line (G1,1))) = ( width G1) by MATRIX_0:def 7;

                                then

                                 A738: K1 in ( dom L1) by A367, A400, FINSEQ_1:def 3;

                                then

                                 A739: (L1 /. K1) = (L1 . K1) by PARTFUN1:def 6;

                                ( len (h1 ^ F)) = (( len h1) + ( len F)) & 0 <= ( len F) by FINSEQ_1: 22;

                                then ( 0 + 1) <= ( len (h1 ^ F)) by A369, A736, XREAL_1: 7;

                                then 1 in ( dom (h1 ^ F)) by FINSEQ_3: 25;

                                

                                then (FF /. 1) = ((h1 ^ F) /. 1) by FINSEQ_4: 68

                                .= (h1 /. 1) by A369, A468, A737, FINSEQ_4: 68

                                .= (G1 * (1,K1)) by A369, A468, A737

                                .= (L1 /. K1) by A367, A400, A739, MATRIX_0:def 7;

                                hence (FF /. 1) in ( rng ( Line (G1,1))) by A738, PARTFUN2: 2;

                              end;

                            end;

                            ( rng tt) c= ( rng f) by A351, A354;

                            then

                             A740: ( rng tt) c= ( rng g1) by A178;

                            now

                              

                               A741: [mi, K1] in ( Indices G1) by A39, A96, A367, A400, ZFMISC_1: 87;

                              reconsider w4 = ((pf + 1) - 1) as Nat;

                              let i1,i2,j1,j2 be Nat;

                              assume that

                               A742: [i1, i2] in ( Indices G1) and

                               A743: [j1, j2] in ( Indices G1) and

                               A744: (h1 /. ( len h1)) = (G1 * (i1,i2)) and

                               A745: (F /. 1) = (G1 * (j1,j2)) and

                               A746: ( len h1) in ( dom h1) and

                               A747: 1 in ( dom F);

                              (F /. 1) = (F1 /. w4) by A663, A664, A747

                              .= (g /. w4) by A654, A663, A664, A747

                              .= (G1 * (mi,K1)) by A367, A368, A400, A526, MATRIX_0:def 7;

                              then

                               A748: j1 = mi & j2 = K1 by A743, A745, A741, GOBOARD1: 5;

                              l1 in ( dom G1) by A369, A401, A746;

                              then

                               A749: [l1, K1] in ( Indices G1) by A96, A367, A400, ZFMISC_1: 87;

                              (h1 /. ( len h1)) = (G1 * (l1,K1)) by A369, A746;

                              then i1 = l1 & i2 = K1 by A742, A744, A749, GOBOARD1: 5;

                              

                              hence ( |.(i1 - j1).| + |.(i2 - j2).|) = ( |.((mi - 1) - mi).| + 0 ) by A748, ABSVALUE: 2

                              .= |.( - 1).|

                              .= |.1.| by COMPLEX1: 52

                              .= 1 by ABSVALUE:def 1;

                            end;

                            then for n st n in ( dom (h1 ^ F)) & (n + 1) in ( dom (h1 ^ F)) holds for i1,i2,j1,j2 be Nat st [i1, i2] in ( Indices G1) & [j1, j2] in ( Indices G1) & ((h1 ^ F) /. n) = (G1 * (i1,i2)) & ((h1 ^ F) /. (n + 1)) = (G1 * (j1,j2)) holds ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A408, A724, GOBOARD1: 24;

                            then for n st n in ( dom FF) & (n + 1) in ( dom FF) holds for m, k, i, j st [m, k] in ( Indices G1) & [i, j] in ( Indices G1) & (FF /. n) = (G1 * (m,k)) & (FF /. (n + 1)) = (G1 * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1 by A475, A669, GOBOARD1: 24;

                            then FF is_sequence_on G1 by A682, GOBOARD1:def 9;

                            then

                             A750: FF is_sequence_on D by A73, A152, A723, GOBOARD1: 25;

                            

                             A751: ( len FF) = (( len (h1 ^ F)) + ( len h2)) by FINSEQ_1: 22

                            .= ((( len h1) + ( len F)) + ( len h2)) by FINSEQ_1: 22;

                            then 1 in ( dom FF) by A683, FINSEQ_3: 25;

                            then

                             A752: (FF /. 1) in ( rng ( Line (D,1))) by A73, A26, A152, A731, A723, MATRIX_0: 75;

                             A753:

                            now

                              per cases ;

                                suppose

                                 A754: ma = ( len G1);

                                

                                 A755: pl in ( Seg pf) by A487, A653, FINSEQ_1: 1;

                                

                                 A756: ((pf + 1) - ((pf + 1) - pl)) = pl;

                                

                                 A757: ( len F) in ( dom F) by A663, A668, FINSEQ_3: 25;

                                h2 = {} by A421, A754;

                                then

                                 A758: FF = (h1 ^ F) by FINSEQ_1: 34;

                                

                                then (FF /. ( len FF)) = (FF /. (( len h1) + ( len F))) by FINSEQ_1: 22

                                .= (F /. LL) by A663, A758, A757, FINSEQ_4: 69

                                .= (F1 /. pl) by A663, A664, A756, A757

                                .= (g /. pl) by A359, A755, FINSEQ_4: 71;

                                hence (FF /. ( len FF)) in ( rng ( Line (G1,( len G1)))) by A363, A754;

                              end;

                                suppose

                                 A759: ma <> ( len G1);

                                ma <= ( len G1) by A41, FINSEQ_3: 25;

                                then ma < ( len G1) by A759, XXREAL_0: 1;

                                then (ma + 1) <= ( len G1) by NAT_1: 13;

                                then

                                 A760: 1 <= l2 by XREAL_1: 19;

                                then

                                 A761: l2 in ( Seg l2) by FINSEQ_1: 1;

                                ( len ( Line (G1,( len G1)))) = ( width G1) by MATRIX_0:def 7;

                                then

                                 A762: K2 in ( dom Ll) by A365, A355, FINSEQ_1:def 3;

                                then

                                 A763: (Ll /. K2) = (Ll . K2) by PARTFUN1:def 6;

                                

                                 A764: ( len h2) in ( dom h2) by A421, A760, FINSEQ_3: 25;

                                (FF /. ( len FF)) = (FF /. (( len (h1 ^ F)) + ( len h2))) by FINSEQ_1: 22

                                .= (h2 /. l2) by A421, A764, FINSEQ_4: 69

                                .= (G1 * ((ma + l2),K2)) by A421, A485, A761

                                .= (Ll /. K2) by A365, A355, A763, MATRIX_0:def 7;

                                hence (FF /. ( len FF)) in ( rng ( Line (G1,( len G1)))) by A762, PARTFUN2: 2;

                              end;

                            end;

                            ( len FF) in ( dom FF) by A751, A683, FINSEQ_3: 25;

                            then

                             A765: (FF /. ( len FF)) in ( rng ( Line (D,( len D)))) by A73, A27, A152, A153, A753, A723, MATRIX_0: 75;

                            ( width D) = k by A3, A73, MATRIX_0: 63;

                            then (( rng FF) /\ ( rng tt)) <> {} by A2, A92, A353, A751, A683, A750, A752, A765, A341;

                            then

                             A766: x in (( rng FF) /\ ( rng tt));

                            (( rng tt) /\ ( rng FF)) = (((( rng h1) \/ ( rng F)) /\ ( rng tt)) \/ {} ) by A492, A684, XBOOLE_1: 23

                            .= ( {} \/ (( rng F) /\ ( rng tt))) by A424, XBOOLE_1: 23

                            .= (( rng tt) /\ ( rng F));

                            then (( rng FF) /\ ( rng tt)) c= (( rng g1) /\ ( rng g2)) by A740, A665, XBOOLE_1: 27;

                            hence thesis by A766;

                          end;

                        end;

                        hence thesis;

                      end;

                    end;

                    hence thesis;

                  end;

                end;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A767: P[ 0 ];

      

       A768: for k holds P[k] from NAT_1:sch 2( A767, A1);

       A769:

      now

        let k;

        let G1, g1, g2;

        assume k = ( width G1) & k > 0 & 1 <= ( len g1) & 1 <= ( len g2) & g1 is_sequence_on G1 & g2 is_sequence_on G1 & (g1 /. 1) in ( rng ( Line (G1,1))) & (g1 /. ( len g1)) in ( rng ( Line (G1,( len G1)))) & (g2 /. 1) in ( rng ( Col (G1,1))) & (g2 /. ( len g2)) in ( rng ( Col (G1,( width G1))));

        then (( rng g1) /\ ( rng g2)) <> {} by A768;

        hence ( rng g1) meets ( rng g2) by XBOOLE_0:def 7;

      end;

      ( width G) <> 0 by MATRIX_0:def 10;

      then

       A770: ( width G) > 0 ;

      assume 1 <= ( len f1) & 1 <= ( len f2) & f1 is_sequence_on G & f2 is_sequence_on G & (f1 /. 1) in ( rng ( Line (G,1))) & (f1 /. ( len f1)) in ( rng ( Line (G,( len G)))) & (f2 /. 1) in ( rng ( Col (G,1))) & (f2 /. ( len f2)) in ( rng ( Col (G,( width G))));

      hence thesis by A769, A770;

    end;

    theorem :: GOBOARD4:2

    

     Th2: for G, f1, f2 st 2 <= ( len f1) & 2 <= ( len f2) & f1 is_sequence_on G & f2 is_sequence_on G & (f1 /. 1) in ( rng ( Line (G,1))) & (f1 /. ( len f1)) in ( rng ( Line (G,( len G)))) & (f2 /. 1) in ( rng ( Col (G,1))) & (f2 /. ( len f2)) in ( rng ( Col (G,( width G)))) holds ( L~ f1) meets ( L~ f2)

    proof

      let G, f1, f2;

      assume that

       A1: 2 <= ( len f1) and

       A2: 2 <= ( len f2) and

       A3: f1 is_sequence_on G & f2 is_sequence_on G & (f1 /. 1) in ( rng ( Line (G,1))) & (f1 /. ( len f1)) in ( rng ( Line (G,( len G)))) & (f2 /. 1) in ( rng ( Col (G,1))) & (f2 /. ( len f2)) in ( rng ( Col (G,( width G))));

      1 <= ( len f1) & 1 <= ( len f2) by A1, A2, XXREAL_0: 2;

      then ( rng f1) meets ( rng f2) by A3, Th1;

      then

      consider x be object such that

       A4: x in ( rng f1) and

       A5: x in ( rng f2) by XBOOLE_0: 3;

      ex m be Element of NAT st m in ( dom f2) & (f2 /. m) = x by A5, PARTFUN2: 2;

      then

       A6: x in ( L~ f2) by A2, GOBOARD1: 1;

      ex n be Element of NAT st n in ( dom f1) & (f1 /. n) = x by A4, PARTFUN2: 2;

      then x in ( L~ f1) by A1, GOBOARD1: 1;

      hence thesis by A6, XBOOLE_0: 3;

    end;

    theorem :: GOBOARD4:3

    for G, f1, f2 st 2 <= ( len f1) & 2 <= ( len f2) & f1 is_sequence_on G & f2 is_sequence_on G & (f1 /. 1) in ( rng ( Line (G,1))) & (f1 /. ( len f1)) in ( rng ( Line (G,( len G)))) & (f2 /. 1) in ( rng ( Col (G,1))) & (f2 /. ( len f2)) in ( rng ( Col (G,( width G)))) holds ( L~ f1) meets ( L~ f2) by Th2;

    definition

      let f be Relation, r,s be Real;

      :: GOBOARD4:def1

      pred f lies_between r,s means ( rng f) c= [.r, s.];

    end

    definition

      let f be FinSequence of REAL , r,s be Real;

      :: original: lies_between

      redefine

      :: GOBOARD4:def2

      pred f lies_between r,s means for n st n in ( dom f) holds r <= (f . n) & (f . n) <= s;

      compatibility

      proof

        hereby

          assume f lies_between (r,s);

          then

           A1: ( rng f) c= [.r, s.];

          let n;

          assume n in ( dom f);

          then (f . n) in ( rng f) by FUNCT_1: 3;

          hence r <= (f . n) & (f . n) <= s by A1, XXREAL_1: 1;

        end;

        assume

         A2: for n st n in ( dom f) holds r <= (f . n) & (f . n) <= s;

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A3: x in ( dom f) and

         A4: y = (f . x) by FUNCT_1:def 3;

        reconsider n = x as Nat by A3;

        r <= (f . n) & (f . n) <= s by A2, A3;

        hence thesis by A4, XXREAL_1: 1;

      end;

    end

    theorem :: GOBOARD4:4

    

     Th4: for f1,f2 be FinSequence of ( TOP-REAL 2) st 2 <= ( len f1) & 2 <= ( len f2) & f1 is special & f2 is special & (for n st n in ( dom f1) & (n + 1) in ( dom f1) holds (f1 /. n) <> (f1 /. (n + 1))) & (for n st n in ( dom f2) & (n + 1) in ( dom f2) holds (f2 /. n) <> (f2 /. (n + 1))) & ( X_axis f1) lies_between ((( X_axis f1) . 1),(( X_axis f1) . ( len f1))) & ( X_axis f2) lies_between ((( X_axis f1) . 1),(( X_axis f1) . ( len f1))) & ( Y_axis f1) lies_between ((( Y_axis f2) . 1),(( Y_axis f2) . ( len f2))) & ( Y_axis f2) lies_between ((( Y_axis f2) . 1),(( Y_axis f2) . ( len f2))) holds ( L~ f1) meets ( L~ f2)

    proof

      let f1,f2 be FinSequence of ( TOP-REAL 2);

      assume that

       A1: 2 <= ( len f1) and

       A2: 2 <= ( len f2) and

       A3: f1 is special and

       A4: f2 is special and

       A5: for n st n in ( dom f1) & (n + 1) in ( dom f1) holds (f1 /. n) <> (f1 /. (n + 1)) and

       A6: for n st n in ( dom f2) & (n + 1) in ( dom f2) holds (f2 /. n) <> (f2 /. (n + 1)) and

       A7: ( X_axis f1) lies_between ((( X_axis f1) . 1),(( X_axis f1) . ( len f1))) and

       A8: ( X_axis f2) lies_between ((( X_axis f1) . 1),(( X_axis f1) . ( len f1))) and

       A9: ( Y_axis f1) lies_between ((( Y_axis f2) . 1),(( Y_axis f2) . ( len f2))) and

       A10: ( Y_axis f2) lies_between ((( Y_axis f2) . 1),(( Y_axis f2) . ( len f2)));

      ( len f1) <> 0 & ( len f2) <> 0 by A1, A2;

      then

      reconsider f1, f2 as non empty FinSequence of ( TOP-REAL 2);

      reconsider f = (f1 ^ f2) as non empty FinSequence of ( TOP-REAL 2);

      

       A11: ( Seg ( len f2)) = ( dom f2) by FINSEQ_1:def 3;

      reconsider p1 = (f1 /. 1), p2 = (f1 /. ( len f1)), q1 = (f2 /. 1), q2 = (f2 /. ( len f2)) as Point of ( TOP-REAL 2);

      set x = ( X_axis f), y = ( Y_axis f), x1 = ( X_axis f1), y1 = ( Y_axis f1), x2 = ( X_axis f2), y2 = ( Y_axis f2);

      

       A12: ( Seg ( len f1)) = ( dom f1) by FINSEQ_1:def 3;

      

       A13: 1 <= ( len f1) by A1, XXREAL_0: 2;

      then

       A14: 1 in ( dom f1) by FINSEQ_3: 25;

      then

       A15: (f /. 1) = (f1 /. 1) by FINSEQ_4: 68;

      

       A16: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

      set G = ( GoB f);

      

       A17: ( dom x) = ( Seg ( len x)) & ( len x) = ( len f) by FINSEQ_1:def 3, GOBOARD1:def 1;

      

       A18: ( Seg ( len x2)) = ( dom x2) & ( len x2) = ( len f2) by FINSEQ_1:def 3, GOBOARD1:def 1;

      

       A19: ( len f) = (( len f1) + ( len f2)) by FINSEQ_1: 22;

      

       A20: ( Seg ( len x1)) = ( dom x1) & ( len x1) = ( len f1) by FINSEQ_1:def 3, GOBOARD1:def 1;

      then

       A21: (x1 . 1) = (p1 `1 ) by A12, A14, GOBOARD1:def 1;

       A22:

      now

        let m;

        set s = (x . m);

        assume

         A23: m in ( dom f);

        then

         A24: m <= ( len f) by FINSEQ_3: 25;

        

         A25: 1 <= m by A23, FINSEQ_3: 25;

        now

          per cases ;

            suppose

             A26: m <= ( len f1);

            reconsider u = (f1 /. m) as Point of ( TOP-REAL 2);

            

             A27: m in ( dom f1) by A25, A26, FINSEQ_3: 25;

            then (f /. m) = u by FINSEQ_4: 68;

            then

             A28: (x . m) = (u `1 ) by A16, A17, A23, GOBOARD1:def 1;

            (x1 . m) = (u `1 ) by A12, A20, A27, GOBOARD1:def 1;

            hence (p1 `1 ) <= s by A7, A12, A20, A21, A27, A28;

          end;

            suppose

             A29: ( len f1) < m;

            then

            reconsider w5 = (m - ( len f1)) as Element of NAT by INT_1: 5;

            w5 > 0 by A29, XREAL_1: 50;

            then

             A30: 1 <= w5 by NAT_1: 14;

            

             A31: m = (w5 + ( len f1));

            then

            reconsider m1 = (m - ( len f1)) as Nat;

            reconsider u = (f2 /. m1) as Point of ( TOP-REAL 2);

            

             A32: w5 <= ( len f2) by A19, A24, A31, XREAL_1: 6;

            then (f /. m) = (f2 /. w5) by A31, A30, SEQ_4: 136;

            then

             A33: (x . m) = (u `1 ) by A16, A17, A23, GOBOARD1:def 1;

            

             A34: m1 in ( dom f2) by A30, A32, FINSEQ_3: 25;

            then (x2 . m1) = (u `1 ) by A11, A18, GOBOARD1:def 1;

            hence (p1 `1 ) <= s by A8, A11, A18, A21, A34, A33;

          end;

        end;

        hence (p1 `1 ) <= s;

      end;

      ( len f) = (( len f1) + ( len f2)) by FINSEQ_1: 22;

      then (2 + 2) <= ( len f) by A1, A2, XREAL_1: 7;

      then 1 <= ( len f) by XXREAL_0: 2;

      then

       A35: 1 in ( dom f) by FINSEQ_3: 25;

      then (x . 1) = (p1 `1 ) by A16, A17, A15, GOBOARD1:def 1;

      then

       A36: (f /. 1) in ( rng ( Line (G,1))) by A35, A22, GOBOARD2: 15;

      

       A37: ( len f1) in ( dom f1) by A13, FINSEQ_3: 25;

      then

       A38: (f /. ( len f1)) = (f1 /. ( len f1)) by FINSEQ_4: 68;

      

       A39: (x1 . ( len f1)) = (p2 `1 ) by A12, A20, A37, GOBOARD1:def 1;

       A40:

      now

        let m;

        set s = (x . m);

        assume

         A41: m in ( dom f);

        then

         A42: m <= ( len f) by FINSEQ_3: 25;

        

         A43: 1 <= m by A41, FINSEQ_3: 25;

        now

          per cases ;

            suppose

             A44: m <= ( len f1);

            reconsider u = (f1 /. m) as Point of ( TOP-REAL 2);

            

             A45: m in ( dom f1) by A43, A44, FINSEQ_3: 25;

            then (f /. m) = u by FINSEQ_4: 68;

            then

             A46: (x . m) = (u `1 ) by A16, A17, A41, GOBOARD1:def 1;

            (x1 . m) = (u `1 ) by A12, A20, A45, GOBOARD1:def 1;

            hence s <= (p2 `1 ) by A7, A12, A20, A39, A45, A46;

          end;

            suppose

             A47: ( len f1) < m;

            then

            reconsider w5 = (m - ( len f1)) as Element of NAT by INT_1: 5;

            w5 > 0 by A47, XREAL_1: 50;

            then

             A48: 1 <= w5 by NAT_1: 14;

            

             A49: m = (w5 + ( len f1));

            then

            reconsider m1 = (m - ( len f1)) as Nat;

            reconsider u = (f2 /. m1) as Point of ( TOP-REAL 2);

            

             A50: w5 <= ( len f2) by A19, A42, A49, XREAL_1: 6;

            then (f /. m) = (f2 /. w5) by A49, A48, SEQ_4: 136;

            then

             A51: (x . m) = (u `1 ) by A16, A17, A41, GOBOARD1:def 1;

            

             A52: m1 in ( dom f2) by A48, A50, FINSEQ_3: 25;

            then (x2 . m1) = (u `1 ) by A11, A18, GOBOARD1:def 1;

            hence s <= (p2 `1 ) by A8, A11, A18, A39, A52, A51;

          end;

        end;

        hence s <= (p2 `1 );

      end;

      

       A53: ( dom f1) c= ( dom f) by FINSEQ_1: 26;

      then (x . ( len f1)) = (p2 `1 ) by A16, A17, A37, A38, GOBOARD1:def 1;

      then

       A54: (f /. ( len f1)) in ( rng ( Line (G,( len G)))) by A53, A37, A40, GOBOARD2: 16;

      now

        let n;

        assume

         A55: n in ( dom f1);

        ( dom f1) c= ( dom f) by FINSEQ_1: 26;

        then

        consider i, j such that

         A56: [i, j] in ( Indices G) & (f /. n) = (G * (i,j)) by A55, GOBOARD2: 14;

        take i, j;

        thus [i, j] in ( Indices G) & (f1 /. n) = (G * (i,j)) by A55, A56, FINSEQ_4: 68;

      end;

      then

      consider g1 such that

       A57: g1 is_sequence_on G & ( L~ g1) = ( L~ f1) & (g1 /. 1) = (f1 /. 1) & (g1 /. ( len g1)) = (f1 /. ( len f1)) and

       A58: ( len f1) <= ( len g1) by A3, A5, GOBOARD2: 12;

      now

        let n;

        assume

         A59: n in ( dom f2);

        then (( len f1) + n) in ( dom f) by FINSEQ_1: 28;

        then

        consider i, j such that

         A60: [i, j] in ( Indices G) & (f /. (( len f1) + n)) = (G * (i,j)) by GOBOARD2: 14;

        take i, j;

        thus [i, j] in ( Indices G) & (f2 /. n) = (G * (i,j)) by A59, A60, FINSEQ_4: 69;

      end;

      then

      consider g2 such that

       A61: g2 is_sequence_on G & ( L~ g2) = ( L~ f2) & (g2 /. 1) = (f2 /. 1) & (g2 /. ( len g2)) = (f2 /. ( len f2)) and

       A62: ( len f2) <= ( len g2) by A4, A6, GOBOARD2: 12;

      

       A63: 2 <= ( len g2) by A2, A62, XXREAL_0: 2;

      

       A64: 1 <= ( len f2) by A2, XXREAL_0: 2;

      then

       A65: 1 in ( dom f2) by FINSEQ_3: 25;

      then

       A66: (f /. (( len f1) + 1)) = (f2 /. 1) by FINSEQ_4: 69;

      

       A67: ( Seg ( len y)) = ( dom y) & ( len y) = ( len f) by FINSEQ_1:def 3, GOBOARD1:def 2;

      

       A68: ( Seg ( len y1)) = ( dom y1) & ( len y1) = ( len f1) by FINSEQ_1:def 3, GOBOARD1:def 2;

      

       A69: ( Seg ( len y2)) = ( dom y2) & ( len y2) = ( len f2) by FINSEQ_1:def 3, GOBOARD1:def 2;

      then

       A70: (y2 . 1) = (q1 `2 ) by A11, A65, GOBOARD1:def 2;

       A71:

      now

        let m;

        set s = (y . m);

        assume

         A72: m in ( dom f);

        then

         A73: m <= ( len f) by FINSEQ_3: 25;

        

         A74: 1 <= m by A72, FINSEQ_3: 25;

        now

          per cases ;

            suppose

             A75: m <= ( len f1);

            reconsider u = (f1 /. m) as Point of ( TOP-REAL 2);

            

             A76: m in ( dom f1) by A74, A75, FINSEQ_3: 25;

            then (f /. m) = u by FINSEQ_4: 68;

            then

             A77: (y . m) = (u `2 ) by A16, A67, A72, GOBOARD1:def 2;

            (y1 . m) = (u `2 ) by A12, A68, A76, GOBOARD1:def 2;

            hence (q1 `2 ) <= s by A9, A12, A68, A70, A76, A77;

          end;

            suppose

             A78: ( len f1) < m;

            then

            reconsider w5 = (m - ( len f1)) as Element of NAT by INT_1: 5;

            w5 > 0 by A78, XREAL_1: 50;

            then

             A79: 1 <= w5 by NAT_1: 14;

            

             A80: m = (w5 + ( len f1));

            then

            reconsider m1 = (m - ( len f1)) as Nat;

            reconsider u = (f2 /. m1) as Point of ( TOP-REAL 2);

            

             A81: w5 <= ( len f2) by A19, A73, A80, XREAL_1: 6;

            then (f /. m) = (f2 /. w5) by A80, A79, SEQ_4: 136;

            then

             A82: (y . m) = (u `2 ) by A16, A67, A72, GOBOARD1:def 2;

            

             A83: m1 in ( dom f2) by A79, A81, FINSEQ_3: 25;

            then (y2 . m1) = (u `2 ) by A11, A69, GOBOARD1:def 2;

            hence (q1 `2 ) <= s by A10, A11, A69, A70, A83, A82;

          end;

        end;

        hence (q1 `2 ) <= s;

      end;

      

       A84: (( len f1) + 1) in ( dom f) by A65, FINSEQ_1: 28;

      then (y . (( len f1) + 1)) = (q1 `2 ) by A16, A67, A66, GOBOARD1:def 2;

      then

       A85: (f /. (( len f1) + 1)) in ( rng ( Col (G,1))) by A84, A71, GOBOARD2: 17;

      

       A86: ( len f2) in ( dom f2) by A64, FINSEQ_3: 25;

      then

       A87: (f /. (( len f1) + ( len f2))) = (f2 /. ( len f2)) by FINSEQ_4: 69;

      

       A88: (y2 . ( len f2)) = (q2 `2 ) by A11, A69, A86, GOBOARD1:def 2;

       A89:

      now

        let m;

        set s = (y . m);

        assume

         A90: m in ( dom f);

        then

         A91: m <= ( len f) by FINSEQ_3: 25;

        

         A92: 1 <= m by A90, FINSEQ_3: 25;

        now

          per cases ;

            suppose

             A93: m <= ( len f1);

            reconsider u = (f1 /. m) as Point of ( TOP-REAL 2);

            

             A94: m in ( dom f1) by A92, A93, FINSEQ_3: 25;

            then (f /. m) = u by FINSEQ_4: 68;

            then

             A95: (y . m) = (u `2 ) by A16, A67, A90, GOBOARD1:def 2;

            (y1 . m) = (u `2 ) by A12, A68, A94, GOBOARD1:def 2;

            hence s <= (q2 `2 ) by A9, A12, A68, A88, A94, A95;

          end;

            suppose

             A96: ( len f1) < m;

            then

            reconsider w5 = (m - ( len f1)) as Element of NAT by INT_1: 5;

            w5 > 0 by A96, XREAL_1: 50;

            then

             A97: 1 <= w5 by NAT_1: 14;

            

             A98: m = (w5 + ( len f1));

            then

            reconsider m1 = (m - ( len f1)) as Nat;

            reconsider u = (f2 /. m1) as Point of ( TOP-REAL 2);

            

             A99: w5 <= ( len f2) by A19, A91, A98, XREAL_1: 6;

            then (f /. m) = (f2 /. w5) by A98, A97, SEQ_4: 136;

            then

             A100: (y . m) = (u `2 ) by A16, A67, A90, GOBOARD1:def 2;

            

             A101: m1 in ( dom f2) by A97, A99, FINSEQ_3: 25;

            then (y2 . m1) = (u `2 ) by A11, A69, GOBOARD1:def 2;

            hence s <= (q2 `2 ) by A10, A11, A69, A88, A101, A100;

          end;

        end;

        hence s <= (q2 `2 );

      end;

      

       A102: (( len f1) + ( len f2)) in ( dom f) by A86, FINSEQ_1: 28;

      then (y . (( len f1) + ( len f2))) = (q2 `2 ) by A16, A67, A87, GOBOARD1:def 2;

      then

       A103: (f /. (( len f1) + ( len f2))) in ( rng ( Col (G,( width G)))) by A102, A89, GOBOARD2: 18;

      2 <= ( len g1) by A1, A58, XXREAL_0: 2;

      hence thesis by A57, A61, A15, A38, A66, A87, A36, A54, A85, A103, A63, Th2;

    end;

    theorem :: GOBOARD4:5

    

     Th5: for f1,f2 be FinSequence of ( TOP-REAL 2) st f1 is one-to-one special & 2 <= ( len f1) & f2 is one-to-one special & 2 <= ( len f2) & ( X_axis f1) lies_between ((( X_axis f1) . 1),(( X_axis f1) . ( len f1))) & ( X_axis f2) lies_between ((( X_axis f1) . 1),(( X_axis f1) . ( len f1))) & ( Y_axis f1) lies_between ((( Y_axis f2) . 1),(( Y_axis f2) . ( len f2))) & ( Y_axis f2) lies_between ((( Y_axis f2) . 1),(( Y_axis f2) . ( len f2))) holds ( L~ f1) meets ( L~ f2)

    proof

      let f1,f2 be FinSequence of ( TOP-REAL 2);

      assume that

       A1: f1 is one-to-one special and

       A2: 2 <= ( len f1) and

       A3: f2 is one-to-one special and

       A4: 2 <= ( len f2) & ( X_axis f1) lies_between ((( X_axis f1) . 1),(( X_axis f1) . ( len f1))) & ( X_axis f2) lies_between ((( X_axis f1) . 1),(( X_axis f1) . ( len f1))) & ( Y_axis f1) lies_between ((( Y_axis f2) . 1),(( Y_axis f2) . ( len f2))) & ( Y_axis f2) lies_between ((( Y_axis f2) . 1),(( Y_axis f2) . ( len f2)));

      

       A5: for n st n in ( dom f2) & (n + 1) in ( dom f2) holds (f2 /. n) <> (f2 /. (n + 1))

      proof

        let n;

        assume n in ( dom f2) & (n + 1) in ( dom f2) & (f2 /. n) = (f2 /. (n + 1));

        then n = (n + 1) by A3, PARTFUN2: 10;

        hence contradiction;

      end;

      for n st n in ( dom f1) & (n + 1) in ( dom f1) holds (f1 /. n) <> (f1 /. (n + 1))

      proof

        let n;

        assume n in ( dom f1) & (n + 1) in ( dom f1) & (f1 /. n) = (f1 /. (n + 1));

        then n = (n + 1) by A1, PARTFUN2: 10;

        hence contradiction;

      end;

      hence thesis by A1, A2, A3, A4, A5, Th4;

    end;

    theorem :: GOBOARD4:6

    for P1, P2, p1, p2, q1, q2 st P1 is_S-P_arc_joining (p1,q1) & P2 is_S-P_arc_joining (p2,q2) & (for p st p in (P1 \/ P2) holds (p1 `1 ) <= (p `1 ) & (p `1 ) <= (q1 `1 )) & (for p st p in (P1 \/ P2) holds (p2 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 )) holds P1 meets P2

    proof

      let P1, P2, p1, p2, q1, q2;

      assume that

       A1: P1 is_S-P_arc_joining (p1,q1) and

       A2: P2 is_S-P_arc_joining (p2,q2) and

       A3: for p st p in (P1 \/ P2) holds (p1 `1 ) <= (p `1 ) & (p `1 ) <= (q1 `1 ) and

       A4: for p st p in (P1 \/ P2) holds (p2 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 );

      consider f1 such that

       A5: f1 is being_S-Seq and

       A6: P1 = ( L~ f1) and

       A7: p1 = (f1 /. 1) and

       A8: q1 = (f1 /. ( len f1)) by A1, TOPREAL4:def 1;

      ( len f1) <> 0 by A5, TOPREAL1:def 8;

      then

      reconsider f1 as non empty FinSequence of ( TOP-REAL 2);

      

       A9: ( Seg ( len f1)) = ( dom f1) by FINSEQ_1:def 3;

      consider f2 such that

       A10: f2 is being_S-Seq and

       A11: P2 = ( L~ f2) and

       A12: p2 = (f2 /. 1) and

       A13: q2 = (f2 /. ( len f2)) by A2, TOPREAL4:def 1;

      ( len f2) <> 0 by A10, TOPREAL1:def 8;

      then

      reconsider f2 as non empty FinSequence of ( TOP-REAL 2);

      

       A14: ( Seg ( len f2)) = ( dom f2) by FINSEQ_1:def 3;

      set x1 = ( X_axis f1), y1 = ( Y_axis f1), x2 = ( X_axis f2), y2 = ( Y_axis f2);

      

       A15: ( Seg ( len x1)) = ( dom x1) & ( len x1) = ( len f1) by FINSEQ_1:def 3, GOBOARD1:def 1;

      

       A16: ( dom y2) = ( Seg ( len y2)) & ( len y2) = ( len f2) by FINSEQ_1:def 3, GOBOARD1:def 2;

      

       A17: 2 <= ( len f2) by A10, TOPREAL1:def 8;

      then

       A18: 1 <= ( len f2) by XXREAL_0: 2;

      then 1 in ( dom f2) by FINSEQ_3: 25;

      then

       A19: (y2 . 1) = (p2 `2 ) by A12, A14, A16, GOBOARD1:def 2;

      ( len f2) in ( dom f2) by A18, FINSEQ_3: 25;

      then

       A20: (y2 . ( len f2)) = (q2 `2 ) by A13, A14, A16, GOBOARD1:def 2;

      

       A21: y2 lies_between ((y2 . 1),(y2 . ( len f2)))

      proof

        let n;

        set q = (f2 /. n);

        assume

         A22: n in ( dom y2);

        then q in ( L~ f2) by A17, A14, A16, GOBOARD1: 1;

        then

         A23: q in (P1 \/ P2) by A11, XBOOLE_0:def 3;

        (y2 . n) = (q `2 ) by A22, GOBOARD1:def 2;

        hence thesis by A4, A19, A20, A23;

      end;

      

       A24: 2 <= ( len f1) by A5, TOPREAL1:def 8;

      then

       A25: 1 <= ( len f1) by XXREAL_0: 2;

      then 1 in ( dom f1) by FINSEQ_3: 25;

      then

       A26: (x1 . 1) = (p1 `1 ) by A7, A9, A15, GOBOARD1:def 1;

      ( len f1) in ( dom f1) by A25, FINSEQ_3: 25;

      then

       A27: (x1 . ( len f1)) = (q1 `1 ) by A8, A9, A15, GOBOARD1:def 1;

      

       A28: x1 lies_between ((x1 . 1),(x1 . ( len f1)))

      proof

        let n;

        set q = (f1 /. n);

        assume

         A29: n in ( dom x1);

        then q in ( L~ f1) by A24, A9, A15, GOBOARD1: 1;

        then

         A30: q in (P1 \/ P2) by A6, XBOOLE_0:def 3;

        (x1 . n) = (q `1 ) by A29, GOBOARD1:def 1;

        hence thesis by A3, A26, A27, A30;

      end;

      

       A31: ( dom x2) = ( Seg ( len x2)) & ( len x2) = ( len f2) by FINSEQ_1:def 3, GOBOARD1:def 1;

      

       A32: x2 lies_between ((x1 . 1),(x1 . ( len f1)))

      proof

        let n;

        set q = (f2 /. n);

        assume

         A33: n in ( dom x2);

        then q in ( L~ f2) by A17, A14, A31, GOBOARD1: 1;

        then

         A34: q in (P1 \/ P2) by A11, XBOOLE_0:def 3;

        (x2 . n) = (q `1 ) by A33, GOBOARD1:def 1;

        hence thesis by A3, A26, A27, A34;

      end;

      

       A35: ( dom y1) = ( Seg ( len y1)) & ( len y1) = ( len f1) by FINSEQ_1:def 3, GOBOARD1:def 2;

      

       A36: y1 lies_between ((y2 . 1),(y2 . ( len f2)))

      proof

        let n;

        set q = (f1 /. n);

        assume

         A37: n in ( dom y1);

        then q in ( L~ f1) by A24, A9, A35, GOBOARD1: 1;

        then

         A38: q in (P1 \/ P2) by A6, XBOOLE_0:def 3;

        (y1 . n) = (q `2 ) by A37, GOBOARD1:def 2;

        hence thesis by A4, A19, A20, A38;

      end;

      

       A39: f2 is one-to-one special by A10, TOPREAL1:def 8;

      f1 is one-to-one special by A5, TOPREAL1:def 8;

      hence thesis by A6, A11, A39, A24, A17, A28, A32, A36, A21, Th5;

    end;