goboard3.miz



    begin

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

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

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

G for Go-board,

x for set;

     Lm1:

    now

      let f, k;

      

       A1: ( dom (f | k)) = ( Seg ( len (f | k))) by FINSEQ_1:def 3;

      assume

       A2: ( len f) = (k + 1);

      then

       A3: ( len (f | k)) = k by FINSEQ_1: 59, NAT_1: 11;

      assume k <> 0 ;

      then

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

      assume

       A5: f is unfolded;

      

       A6: k <= (k + 1) by NAT_1: 11;

      then

       A7: k in ( dom f) by A2, A4, FINSEQ_3: 25;

      thus (f | k) is unfolded

      proof

        let n be Nat;

        set f1 = (f | k);

        assume that

         A8: 1 <= n and

         A9: (n + 2) <= ( len f1);

        reconsider n as Element of NAT by ORDINAL1:def 12;

        

         A10: (n + 1) in ( dom f1) by A8, A9, SEQ_4: 135;

        n in ( dom f1) by A8, A9, SEQ_4: 135;

        then

         A11: ( LSeg (f1,n)) = ( LSeg (f,n)) by A10, TOPREAL3: 17;

        ( len f1) <= ( len f) by A2, A6, FINSEQ_1: 59;

        then

         A12: (n + 2) <= ( len f) by A9, XXREAL_0: 2;

        

         A13: ((n + 1) + 1) = (n + (1 + 1));

        (n + 2) in ( dom f1) by A8, A9, SEQ_4: 135;

        then

         A14: ( LSeg (f1,(n + 1))) = ( LSeg (f,(n + 1))) by A10, A13, TOPREAL3: 17;

        (f1 /. (n + 1)) = (f /. (n + 1)) by A7, A3, A1, A10, FINSEQ_4: 71;

        hence thesis by A5, A8, A11, A14, A12;

      end;

    end;

    theorem :: GOBOARD3:1

    

     Th1: (for n st n in ( dom f) holds ex i, j st [i, j] in ( Indices G) & (f /. n) = (G * (i,j))) & f is one-to-one unfolded s.n.c. special implies ex g st g is_sequence_on G & g is one-to-one unfolded s.n.c. special & ( L~ f) = ( L~ g) & (f /. 1) = (g /. 1) & (f /. ( len f)) = (g /. ( len g)) & ( len f) <= ( len g)

    proof

      defpred P[ Nat] means for f st ( len f) = $1 & (for n st n in ( dom f) holds ex i, j st [i, j] in ( Indices G) & (f /. n) = (G * (i,j))) & f is one-to-one unfolded s.n.c. special holds ex g st g is_sequence_on G & g is one-to-one unfolded s.n.c. special & ( L~ f) = ( L~ g) & (f /. 1) = (g /. 1) & (f /. ( len f)) = (g /. ( len g)) & ( len f) <= ( len g);

      

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

      proof

        let k such that

         A2: P[k];

        let f such that

         A3: ( len f) = (k + 1) and

         A4: for n st n in ( dom f) holds ex i, j st [i, j] in ( Indices G) & (f /. n) = (G * (i,j)) and

         A5: f is one-to-one and

         A6: f is unfolded and

         A7: f is s.n.c. and

         A8: f is special;

        per cases ;

          suppose

           A9: k = 0 ;

          take g = f;

          

           A10: ( dom f) = {1} by A3, A9, FINSEQ_1: 2, FINSEQ_1:def 3;

          now

            let n;

            assume that

             A11: n in ( dom g) and

             A12: (n + 1) in ( dom g);

            n = 1 by A10, A11, TARSKI:def 1;

            hence for i1,i2,j1,j2 be Nat st [i1, i2] in ( Indices G) & [j1, j2] in ( Indices G) & (g /. n) = (G * (i1,i2)) & (g /. (n + 1)) = (G * (j1,j2)) holds ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A10, A12, TARSKI:def 1;

          end;

          hence g is_sequence_on G by A4, GOBOARD1:def 9;

          thus thesis by A5, A6, A7, A8;

        end;

          suppose

           A13: k <> 0 ;

          

           A14: ( len (f | k)) = k by A3, FINSEQ_1: 59, NAT_1: 11;

          set f1 = (f | k);

          

           A15: f1 is unfolded by A3, A6, A13, Lm1;

          

           A16: f1 is s.n.c. by A7, GOBOARD2: 7;

          f1 = (f | ( Seg k)) by FINSEQ_1:def 15;

          then

           A17: f1 is one-to-one by A5, FUNCT_1: 52;

          

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

          1 <= ( len f) by A3, NAT_1: 11;

          then

           A19: (k + 1) in ( dom f) by A3, FINSEQ_3: 25;

          then

          consider j1,j2 be Nat such that

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

           A21: (f /. (k + 1)) = (G * (j1,j2)) by A4;

          

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

          then

           A23: j1 in ( dom G) by A20, ZFMISC_1: 87;

          

           A24: ( 0 + 1) <= k by A13, NAT_1: 13;

          then

           A25: 1 in ( Seg k) by FINSEQ_1: 1;

          

           A26: k <= (k + 1) by NAT_1: 11;

          then

           A27: k in ( dom f) by A3, A24, FINSEQ_3: 25;

          then

          consider i1,i2 be Nat such that

           A28: [i1, i2] in ( Indices G) and

           A29: (f /. k) = (G * (i1,i2)) by A4;

          reconsider l1 = ( Line (G,i1)), c1 = ( Col (G,i2)) as FinSequence of ( TOP-REAL 2);

          set x1 = ( X_axis l1), y1 = ( Y_axis l1), x2 = ( X_axis c1), y2 = ( Y_axis c1);

          

           A30: ( dom y1) = ( Seg ( len y1)) & ( len y1) = ( len l1) by FINSEQ_1:def 3, GOBOARD1:def 2;

          

           A31: ( dom (f | k)) = ( Seg ( len (f | k))) by FINSEQ_1:def 3;

          

           A32: f1 is special

          proof

            let n be Nat;

            assume that

             A33: 1 <= n and

             A34: (n + 1) <= ( len f1);

            (n + 1) in ( dom f1) by A33, A34, SEQ_4: 134;

            then

             A35: (f1 /. (n + 1)) = (f /. (n + 1)) by A27, A14, A31, FINSEQ_4: 71;

            ( len f1) <= ( len f) by A3, A26, FINSEQ_1: 59;

            then

             A36: (n + 1) <= ( len f) by A34, XXREAL_0: 2;

            n in ( dom f1) by A33, A34, SEQ_4: 134;

            then (f1 /. n) = (f /. n) by A27, A14, A31, FINSEQ_4: 71;

            hence thesis by A8, A33, A35, A36;

          end;

          now

            let n;

            assume

             A37: n in ( dom f1);

            then n in ( dom f) by A27, A14, A31, FINSEQ_4: 71;

            then

            consider i, j such that

             A38: [i, j] in ( Indices G) & (f /. n) = (G * (i,j)) by A4;

            take i, j;

            thus [i, j] in ( Indices G) & (f1 /. n) = (G * (i,j)) by A27, A14, A31, A37, A38, FINSEQ_4: 71;

          end;

          then

          consider g1 such that

           A39: g1 is_sequence_on G and

           A40: g1 is one-to-one and

           A41: g1 is unfolded and

           A42: g1 is s.n.c. and

           A43: g1 is special and

           A44: ( L~ g1) = ( L~ f1) and

           A45: (g1 /. 1) = (f1 /. 1) and

           A46: (g1 /. ( len g1)) = (f1 /. ( len f1)) and

           A47: ( len f1) <= ( len g1) by A2, A14, A17, A15, A16, A32;

          

           A48: for n st n in ( dom g1) & (n + 1) in ( dom g1) holds for m, k, i, j st [m, k] in ( Indices G) & [i, j] in ( Indices G) & (g1 /. n) = (G * (m,k)) & (g1 /. (n + 1)) = (G * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1 by A39, GOBOARD1:def 9;

          

           A49: 1 < k implies ( rng g1) c= ( L~ f1)

          proof

            assume 1 < k;

            then

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

            let x be object;

            assume x in ( rng g1);

            then ex n be Element of NAT st n in ( dom g1) & (g1 /. n) = x by PARTFUN2: 2;

            hence thesis by A14, A44, A47, A50, GOBOARD1: 1, XXREAL_0: 2;

          end;

          

           A51: k in ( Seg k) by A24, FINSEQ_1: 1;

          

           A52: k = 1 implies ( L~ g1) = {} & ( rng g1) = {(f /. k)}

          proof

            

             A53: (g1 /. ( len g1)) = (f /. k) by A27, A14, A51, A46, FINSEQ_4: 71;

            assume

             A54: k = 1;

            hence ( L~ g1) = {} by A14, A44, TOPREAL1: 22;

            then

             A55: ( len g1) = 1 or ( len g1) = 0 by TOPREAL1: 22;

            

             A56: ( rng g1) c= {(f /. k)}

            proof

              let x be object;

              assume x in ( rng g1);

              then

              consider n be Element of NAT such that

               A57: n in ( dom g1) and

               A58: (g1 /. n) = x by PARTFUN2: 2;

              n in ( Seg ( len g1)) by A57, FINSEQ_1:def 3;

              then n = ( len g1) by A55, FINSEQ_1: 2, TARSKI:def 1;

              hence thesis by A53, A58, TARSKI:def 1;

            end;

            1 <= ( len g1) by A3, A47, A54, FINSEQ_1: 59;

            then ( len g1) in ( dom g1) by FINSEQ_3: 25;

            then (f /. k) in ( rng g1) by A53, PARTFUN2: 2;

            then {(f /. k)} c= ( rng g1) by ZFMISC_1: 31;

            hence thesis by A56;

          end;

          

           A59: ( len c1) = ( len G) by MATRIX_0:def 8;

          

          then

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

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

          

           A61: ( dom y2) = ( Seg ( len y2)) & ( len y2) = ( len c1) by FINSEQ_1:def 3, GOBOARD1:def 2;

          

           A62: ( dom x1) = ( Seg ( len x1)) & ( len x1) = ( len l1) by FINSEQ_1:def 3, GOBOARD1:def 1;

          

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

          

           A64: ( len x2) = ( len c1) by GOBOARD1:def 1;

          

          then

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

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

          

           A66: i1 in ( dom G) by A28, A22, ZFMISC_1: 87;

          then

           A67: x1 is constant by GOBOARD1:def 4;

          

           A68: i2 in ( Seg ( width G)) by A28, A22, ZFMISC_1: 87;

          then

           A69: x2 is increasing by GOBOARD1:def 7;

          

           A70: y2 is constant by A68, GOBOARD1:def 5;

          

           A71: y1 is increasing by A66, GOBOARD1:def 6;

          

           A72: ( len l1) = ( width G) by MATRIX_0:def 7;

          then

           A73: ( Seg ( width G)) = ( dom l1) by FINSEQ_1:def 3;

          

           A74: j2 in ( Seg ( width G)) by A20, A22, ZFMISC_1: 87;

          

           A75: for n st n in ( dom g1) holds ex m, k st [m, k] in ( Indices G) & (g1 /. n) = (G * (m,k)) by A39, GOBOARD1:def 9;

          now

            per cases by A8, A27, A28, A29, A19, A20, A21, GOBOARD2: 11;

              suppose

               A76: i1 = j1;

              set ppi = (G * (i1,i2)), pj = (G * (i1,j2));

              now

                per cases by XXREAL_0: 1;

                  case

                   A77: i2 > j2;

                  (l1 /. i2) = (l1 . i2) by A68, A73, PARTFUN1:def 6;

                  then

                   A78: (l1 /. i2) = ppi by A68, MATRIX_0:def 7;

                  then

                   A79: (y1 . i2) = (ppi `2 ) by A68, A30, A72, GOBOARD1:def 2;

                  (l1 /. j2) = (l1 . j2) by A74, A73, PARTFUN1:def 6;

                  then

                   A80: (l1 /. j2) = pj by A74, MATRIX_0:def 7;

                  then

                   A81: (y1 . j2) = (pj `2 ) by A74, A30, A72, GOBOARD1:def 2;

                  then

                   A82: (pj `2 ) < (ppi `2 ) by A68, A74, A71, A30, A72, A77, A79, SEQM_3:def 1;

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

                  defpred P1[ Nat, set] means for m st m = (i2 - $1) holds $2 = (G * (i1,m));

                  set lk = { w where w be Point of ( TOP-REAL 2) : (w `1 ) = (ppi `1 ) & (pj `2 ) <= (w `2 ) & (w `2 ) <= (ppi `2 ) };

                  

                   A83: ppi = |[(ppi `1 ), (ppi `2 )]| by EUCLID: 53;

                   A84:

                  now

                    let n;

                    assume n in ( Seg l);

                    then

                     A85: n <= l by FINSEQ_1: 1;

                    l <= i2 by XREAL_1: 43;

                    then

                    reconsider w = (i2 - n) as Element of NAT by A85, INT_1: 5, XXREAL_0: 2;

                    (i2 - n) <= i2 & i2 <= ( width G) by A68, FINSEQ_1: 1, XREAL_1: 43;

                    then

                     A86: w <= ( width G) by XXREAL_0: 2;

                    

                     A87: 1 <= j2 by A74, FINSEQ_1: 1;

                    (i2 - l) <= (i2 - n) by A85, XREAL_1: 13;

                    then 1 <= w by A87, XXREAL_0: 2;

                    then w in ( Seg ( width G)) by A86, FINSEQ_1: 1;

                    hence (i2 - n) is Element of NAT & [i1, (i2 - n)] in ( Indices G) & (i2 - n) in ( Seg ( width G)) by A22, A66, ZFMISC_1: 87;

                  end;

                   A88:

                  now

                    let n be Nat;

                    assume n in ( Seg l);

                    then

                    reconsider m = (i2 - n) as Element of NAT by A84;

                    take p = (G * (i1,m));

                    thus P1[n, p];

                  end;

                  consider g2 such that

                   A89: ( len g2) = l & for n be Nat st n in ( Seg l) holds P1[n, (g2 /. n)] from FINSEQ_4:sch 1( A88);

                  take g = (g1 ^ g2);

                  

                   A90: ( dom g2) = ( Seg l) by A89, FINSEQ_1:def 3;

                  now

                    let n;

                    assume

                     A91: n in ( dom g2);

                    then (i2 - n) is Element of NAT by A84, A90;

                    then

                    reconsider m = (i2 - n) as Nat;

                    take k = i1, m;

                    thus [k, m] in ( Indices G) & (g2 /. n) = (G * (k,m)) by A84, A89, A90, A91;

                  end;

                  then

                   A92: for n st n in ( dom g) holds ex i, j st [i, j] in ( Indices G) & (g /. n) = (G * (i,j)) by A75, GOBOARD1: 23;

                  

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

                  

                   A94: (x1 . i2) = (ppi `1 ) by A68, A62, A72, A78, GOBOARD1:def 1;

                   A95:

                  now

                    let n, p;

                    assume that

                     A96: n in ( dom g2) and

                     A97: (g2 /. n) = p;

                    reconsider n1 = (i2 - n) as Element of NAT by A84, A90, A96;

                    n <= ( len g2) by A96, FINSEQ_3: 25;

                    then

                     A98: (i2 - ( len g2)) <= n1 by XREAL_1: 13;

                    set pn = (G * (i1,n1));

                    

                     A99: (g2 /. n) = pn by A89, A93, A96;

                    

                     A100: (i2 - n) in ( Seg ( width G)) by A84, A89, A93, A96;

                    then

                     A101: (x1 . n1) = (x1 . i2) by A68, A67, A62, A72, SEQM_3:def 10;

                    (l1 /. n1) = (l1 . n1) by A73, A100, PARTFUN1:def 6;

                    then

                     A102: (l1 /. n1) = pn by A100, MATRIX_0:def 7;

                    then

                     A103: (y1 . n1) = (pn `2 ) by A30, A72, A100, GOBOARD1:def 2;

                    (x1 . n1) = (pn `1 ) by A62, A72, A100, A102, GOBOARD1:def 1;

                    hence (p `1 ) = (ppi `1 ) & (pj `2 ) <= (p `2 ) & (p `2 ) <= (ppi `2 ) by A68, A74, A71, A30, A72, A89, A79, A81, A94, A97, A100, A99, A98, A101, A103, SEQ_4: 137, XREAL_1: 43;

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

                    hence p in ( rng l1) by A72, A97, A100, A99, A102, PARTFUN2: 2;

                    1 <= n by A96, FINSEQ_3: 25;

                    then n1 < i2 by XREAL_1: 44;

                    hence (p `2 ) < (ppi `2 ) by A68, A71, A30, A72, A79, A97, A100, A99, A103, SEQM_3:def 1;

                  end;

                  

                   A104: g2 is special

                  proof

                    let n be Nat;

                    set p = (g2 /. n);

                    assume

                     A105: 1 <= n & (n + 1) <= ( len g2);

                    then n in ( dom g2) by SEQ_4: 134;

                    then

                     A106: (p `1 ) = (ppi `1 ) by A95;

                    (n + 1) in ( dom g2) by A105, SEQ_4: 134;

                    hence thesis by A95, A106;

                  end;

                   A107:

                  now

                    let n, m, p, q;

                    assume that

                     A108: n in ( dom g2) and

                     A109: m in ( dom g2) and

                     A110: n < m and

                     A111: (g2 /. n) = p & (g2 /. m) = q;

                    

                     A112: (i2 - n) in ( Seg ( width G)) by A84, A90, A108;

                    reconsider n1 = (i2 - n), m1 = (i2 - m) as Element of NAT by A84, A90, A108, A109;

                    set pn = (G * (i1,n1)), pm = (G * (i1,m1));

                    

                     A113: m1 < n1 by A110, XREAL_1: 15;

                    (l1 /. n1) = (l1 . n1) by A73, A84, A90, A108, PARTFUN1:def 6;

                    then (l1 /. n1) = pn by A112, MATRIX_0:def 7;

                    then

                     A114: (y1 . n1) = (pn `2 ) by A30, A72, A112, GOBOARD1:def 2;

                    

                     A115: (i2 - m) in ( Seg ( width G)) by A84, A90, A109;

                    (l1 /. m1) = (l1 . m1) by A73, A84, A90, A109, PARTFUN1:def 6;

                    then (l1 /. m1) = pm by A115, MATRIX_0:def 7;

                    then

                     A116: (y1 . m1) = (pm `2 ) by A30, A72, A115, GOBOARD1:def 2;

                    (g2 /. n) = pn & (g2 /. m) = pm by A89, A90, A108, A109;

                    hence (q `2 ) < (p `2 ) by A71, A30, A72, A111, A112, A115, A113, A114, A116, SEQM_3:def 1;

                  end;

                  for n, m st m > (n + 1) & n in ( dom g2) & (n + 1) in ( dom g2) & m in ( dom g2) & (m + 1) in ( dom g2) holds ( LSeg (g2,n)) misses ( LSeg (g2,m))

                  proof

                    let n, m;

                    assume that

                     A117: m > (n + 1) and

                     A118: n in ( dom g2) and

                     A119: (n + 1) in ( dom g2) and

                     A120: m in ( dom g2) and

                     A121: (m + 1) in ( dom g2) and

                     A122: (( LSeg (g2,n)) /\ ( LSeg (g2,m))) <> {} ;

                    reconsider p1 = (g2 /. n), p2 = (g2 /. (n + 1)), q1 = (g2 /. m), q2 = (g2 /. (m + 1)) as Point of ( TOP-REAL 2);

                    

                     A123: (p1 `1 ) = (ppi `1 ) & (p2 `1 ) = (ppi `1 ) by A95, A118, A119;

                    n < (n + 1) by NAT_1: 13;

                    then

                     A124: (p2 `2 ) < (p1 `2 ) by A107, A118, A119;

                    set lp = { w where w be Point of ( TOP-REAL 2) : (w `1 ) = (ppi `1 ) & (p2 `2 ) <= (w `2 ) & (w `2 ) <= (p1 `2 ) }, lq = { w where w be Point of ( TOP-REAL 2) : (w `1 ) = (ppi `1 ) & (q2 `2 ) <= (w `2 ) & (w `2 ) <= (q1 `2 ) };

                    

                     A125: p1 = |[(p1 `1 ), (p1 `2 )]| & p2 = |[(p2 `1 ), (p2 `2 )]| by EUCLID: 53;

                    m < (m + 1) by NAT_1: 13;

                    then

                     A126: (q2 `2 ) < (q1 `2 ) by A107, A120, A121;

                    

                     A127: q1 = |[(q1 `1 ), (q1 `2 )]| & q2 = |[(q2 `1 ), (q2 `2 )]| by EUCLID: 53;

                    set x = the Element of (( LSeg (g2,n)) /\ ( LSeg (g2,m)));

                    

                     A128: x in ( LSeg (g2,n)) by A122, XBOOLE_0:def 4;

                    

                     A129: (q1 `1 ) = (ppi `1 ) & (q2 `1 ) = (ppi `1 ) by A95, A120, A121;

                    

                     A130: x in ( LSeg (g2,m)) by A122, XBOOLE_0:def 4;

                    1 <= m & (m + 1) <= ( len g2) by A120, A121, FINSEQ_3: 25;

                    

                    then ( LSeg (g2,m)) = ( LSeg (q2,q1)) by TOPREAL1:def 3

                    .= lq by A126, A129, A127, TOPREAL3: 9;

                    then

                     A131: ex tm be Point of ( TOP-REAL 2) st tm = x & (tm `1 ) = (ppi `1 ) & (q2 `2 ) <= (tm `2 ) & (tm `2 ) <= (q1 `2 ) by A130;

                    1 <= n & (n + 1) <= ( len g2) by A118, A119, FINSEQ_3: 25;

                    

                    then ( LSeg (g2,n)) = ( LSeg (p2,p1)) by TOPREAL1:def 3

                    .= lp by A124, A123, A125, TOPREAL3: 9;

                    then

                     A132: ex tn be Point of ( TOP-REAL 2) st tn = x & (tn `1 ) = (ppi `1 ) & (p2 `2 ) <= (tn `2 ) & (tn `2 ) <= (p1 `2 ) by A128;

                    (q1 `2 ) < (p2 `2 ) by A107, A117, A119, A120;

                    hence contradiction by A132, A131, XXREAL_0: 2;

                  end;

                  then

                   A133: g2 is s.n.c. by GOBOARD2: 1;

                  

                   A134: not (f /. k) in ( L~ g2)

                  proof

                    set ls = { ( LSeg (g2,m)) : 1 <= m & (m + 1) <= ( len g2) };

                    assume (f /. k) in ( L~ g2);

                    then

                    consider X be set such that

                     A135: (f /. k) in X and

                     A136: X in ls by TARSKI:def 4;

                    consider m such that

                     A137: X = ( LSeg (g2,m)) and

                     A138: 1 <= m & (m + 1) <= ( len g2) by A136;

                    reconsider q1 = (g2 /. m), q2 = (g2 /. (m + 1)) as Point of ( TOP-REAL 2);

                    

                     A139: m in ( dom g2) by A138, SEQ_4: 134;

                    then

                     A140: (q1 `1 ) = (ppi `1 ) by A95;

                    set lq = { w where w be Point of ( TOP-REAL 2) : (w `1 ) = (ppi `1 ) & (q2 `2 ) <= (w `2 ) & (w `2 ) <= (q1 `2 ) };

                    

                     A141: q1 = |[(q1 `1 ), (q1 `2 )]| & q2 = |[(q2 `1 ), (q2 `2 )]| by EUCLID: 53;

                    

                     A142: (m + 1) in ( dom g2) by A138, SEQ_4: 134;

                    then

                     A143: (q2 `1 ) = (ppi `1 ) by A95;

                    m < (m + 1) by NAT_1: 13;

                    then

                     A144: (q2 `2 ) < (q1 `2 ) by A107, A139, A142;

                    ( LSeg (g2,m)) = ( LSeg (q2,q1)) by A138, TOPREAL1:def 3

                    .= lq by A140, A143, A144, A141, TOPREAL3: 9;

                    then ex p st p = (f /. k) & (p `1 ) = (ppi `1 ) & (q2 `2 ) <= (p `2 ) & (p `2 ) <= (q1 `2 ) by A135, A137;

                    hence contradiction by A29, A95, A139;

                  end;

                  (x1 . j2) = (pj `1 ) by A74, A62, A72, A80, GOBOARD1:def 1;

                  then

                   A145: (ppi `1 ) = (pj `1 ) by A68, A74, A67, A62, A72, A94, SEQM_3:def 10;

                  now

                    let n,m be Element of NAT ;

                    assume that

                     A146: n in ( dom g2) & m in ( dom g2) and

                     A147: n <> m;

                    reconsider n1 = (i2 - n), m1 = (i2 - m) as Element of NAT by A84, A90, A146;

                    

                     A148: (g2 /. n) = (G * (i1,n1)) & (g2 /. m) = (G * (i1,m1)) by A89, A90, A146;

                    assume

                     A149: (g2 /. n) = (g2 /. m);

                     [i1, (i2 - n)] in ( Indices G) & [i1, (i2 - m)] in ( Indices G) by A84, A90, A146;

                    then n1 = m1 by A148, A149, GOBOARD1: 5;

                    hence contradiction by A147;

                  end;

                  then for n,m be Element of NAT st n in ( dom g2) & m in ( dom g2) & (g2 /. n) = (g2 /. m) holds n = m;

                  then

                   A150: g2 is one-to-one by PARTFUN2: 9;

                  reconsider m1 = (i2 - l) as Element of NAT by ORDINAL1:def 12;

                  

                   A151: pj = |[(pj `1 ), (pj `2 )]| by EUCLID: 53;

                  

                   A152: ( LSeg (f,k)) = ( LSeg (pj,ppi)) by A3, A24, A29, A21, A76, TOPREAL1:def 3

                  .= lk by A82, A145, A83, A151, TOPREAL3: 9;

                  

                   A153: ( rng g2) c= ( LSeg (f,k))

                  proof

                    let x be object;

                    assume x in ( rng g2);

                    then

                    consider n be Element of NAT such that

                     A154: n in ( dom g2) and

                     A155: (g2 /. n) = x by PARTFUN2: 2;

                    reconsider n1 = (i2 - n) as Element of NAT by A84, A89, A93, A154;

                    set pn = (G * (i1,n1));

                    

                     A156: (g2 /. n) = pn by A89, A93, A154;

                    then

                     A157: (pn `2 ) <= (ppi `2 ) by A95, A154;

                    (pn `1 ) = (ppi `1 ) & (pj `2 ) <= (pn `2 ) by A95, A154, A156;

                    hence thesis by A152, A155, A156, A157;

                  end;

                   A158:

                  now

                    let n;

                    assume that

                     A159: n in ( dom g2) and

                     A160: (n + 1) in ( dom g2);

                    reconsider m1 = (i2 - n), m2 = (i2 - (n + 1)) as Element of NAT by A84, A90, A159, A160;

                    let l1,l2,l3,l4 be Nat;

                    assume that

                     A161: [l1, l2] in ( Indices G) and

                     A162: [l3, l4] in ( Indices G) and

                     A163: (g2 /. n) = (G * (l1,l2)) and

                     A164: (g2 /. (n + 1)) = (G * (l3,l4));

                     [i1, (i2 - (n + 1))] in ( Indices G) & (g2 /. (n + 1)) = (G * (i1,m2)) by A84, A89, A90, A160;

                    then

                     A165: l3 = i1 & l4 = m2 by A162, A164, GOBOARD1: 5;

                     [i1, (i2 - n)] in ( Indices G) & (g2 /. n) = (G * (i1,m1)) by A84, A89, A90, A159;

                    then l1 = i1 & l2 = m1 by A161, A163, GOBOARD1: 5;

                    

                    hence ( |.(l1 - l3).| + |.(l2 - l4).|) = ( 0 + |.((i2 - n) - (i2 - (n + 1))).|) by A165, ABSVALUE: 2

                    .= 1 by ABSVALUE:def 1;

                  end;

                  now

                    let l1,l2,l3,l4 be Nat;

                    assume that

                     A166: [l1, l2] in ( Indices G) and

                     A167: [l3, l4] in ( Indices G) and

                     A168: (g1 /. ( len g1)) = (G * (l1,l2)) and

                     A169: (g2 /. 1) = (G * (l3,l4)) and ( len g1) in ( dom g1) and

                     A170: 1 in ( dom g2);

                    reconsider m1 = (i2 - 1) as Element of NAT by A84, A90, A170;

                     [i1, (i2 - 1)] in ( Indices G) & (g2 /. 1) = (G * (i1,m1)) by A84, A89, A90, A170;

                    then

                     A171: l3 = i1 & l4 = m1 by A167, A169, GOBOARD1: 5;

                    (f1 /. ( len f1)) = (f /. k) by A27, A14, A51, FINSEQ_4: 71;

                    then l1 = i1 & l2 = i2 by A46, A28, A29, A166, A168, GOBOARD1: 5;

                    

                    hence ( |.(l1 - l3).| + |.(l2 - l4).|) = ( 0 + |.(i2 - (i2 - 1)).|) by A171, ABSVALUE: 2

                    .= 1 by ABSVALUE:def 1;

                  end;

                  then for n st n in ( dom g) & (n + 1) in ( dom g) holds for m, k, i, j st [m, k] in ( Indices G) & [i, j] in ( Indices G) & (g /. n) = (G * (m,k)) & (g /. (n + 1)) = (G * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1 by A48, A158, GOBOARD1: 24;

                  hence g is_sequence_on G by A92, GOBOARD1:def 9;

                  

                   A172: ( LSeg (f,k)) = ( LSeg (ppi,pj)) by A3, A24, A29, A21, A76, TOPREAL1:def 3;

                  

                   A173: not (f /. k) in ( rng g2)

                  proof

                    assume (f /. k) in ( rng g2);

                    then

                    consider n be Element of NAT such that

                     A174: n in ( dom g2) and

                     A175: (g2 /. n) = (f /. k) by PARTFUN2: 2;

                    reconsider n1 = (i2 - n) as Element of NAT by A84, A89, A93, A174;

                     [i1, (i2 - n)] in ( Indices G) & (g2 /. n) = (G * (i1,n1)) by A84, A89, A93, A174;

                    then

                     A176: n1 = i2 by A28, A29, A175, GOBOARD1: 5;

                     0 < n by A93, A174, FINSEQ_1: 1;

                    hence contradiction by A176;

                  end;

                  (( rng g1) /\ ( rng g2)) = {}

                  proof

                    set x = the Element of (( rng g1) /\ ( rng g2));

                    assume

                     A177: not thesis;

                    then

                     A178: x in ( rng g2) by XBOOLE_0:def 4;

                    

                     A179: x in ( rng g1) by A177, XBOOLE_0:def 4;

                    now

                      per cases by A24, XXREAL_0: 1;

                        suppose k = 1;

                        hence contradiction by A52, A173, A179, A178, TARSKI:def 1;

                      end;

                        suppose 1 < k;

                        then x in (( L~ f1) /\ ( LSeg (f,k))) & (( L~ f1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, A49, A153, A179, A178, GOBOARD2: 4, XBOOLE_0:def 4;

                        hence contradiction by A173, A178, TARSKI:def 1;

                      end;

                    end;

                    hence contradiction;

                  end;

                  then ( rng g1) misses ( rng g2);

                  hence g is one-to-one by A40, A150, FINSEQ_3: 91;

                  

                   A180: for n st 1 <= n & (n + 2) <= ( len g2) holds (( LSeg (g2,n)) /\ ( LSeg (g2,(n + 1)))) = {(g2 /. (n + 1))}

                  proof

                    let n;

                    assume that

                     A181: 1 <= n and

                     A182: (n + 2) <= ( len g2);

                    

                     A183: (n + 1) in ( dom g2) by A181, A182, SEQ_4: 135;

                    then (g2 /. (n + 1)) in ( rng g2) by PARTFUN2: 2;

                    then (g2 /. (n + 1)) in lk by A152, A153;

                    then

                    consider u1 be Point of ( TOP-REAL 2) such that

                     A184: (g2 /. (n + 1)) = u1 and

                     A185: (u1 `1 ) = (ppi `1 ) and (pj `2 ) <= (u1 `2 ) and (u1 `2 ) <= (ppi `2 );

                    

                     A186: (n + 2) in ( dom g2) by A181, A182, SEQ_4: 135;

                    then (g2 /. (n + 2)) in ( rng g2) by PARTFUN2: 2;

                    then (g2 /. (n + 2)) in lk by A152, A153;

                    then

                    consider u2 be Point of ( TOP-REAL 2) such that

                     A187: (g2 /. (n + 2)) = u2 and

                     A188: (u2 `1 ) = (ppi `1 ) and (pj `2 ) <= (u2 `2 ) and (u2 `2 ) <= (ppi `2 );

                    (n + (1 + 1)) = ((n + 1) + 1) & 1 <= (n + 1) by NAT_1: 11;

                    then

                     A189: ( LSeg (g2,(n + 1))) = ( LSeg (u1,u2)) by A182, A184, A187, TOPREAL1:def 3;

                    (n + 1) < ((n + 1) + 1) by NAT_1: 13;

                    then

                     A190: (u2 `2 ) < (u1 `2 ) by A107, A183, A186, A184, A187;

                    

                     A191: n in ( dom g2) by A181, A182, SEQ_4: 135;

                    then (g2 /. n) in ( rng g2) by PARTFUN2: 2;

                    then (g2 /. n) in lk by A152, A153;

                    then

                    consider u be Point of ( TOP-REAL 2) such that

                     A192: (g2 /. n) = u and

                     A193: (u `1 ) = (ppi `1 ) and (pj `2 ) <= (u `2 ) and (u `2 ) <= (ppi `2 );

                    (n + 1) <= (n + 2) by XREAL_1: 6;

                    then (n + 1) <= ( len g2) by A182, XXREAL_0: 2;

                    then

                     A194: ( LSeg (g2,n)) = ( LSeg (u,u1)) by A181, A192, A184, TOPREAL1:def 3;

                    set lg = { w where w be Point of ( TOP-REAL 2) : (w `1 ) = (ppi `1 ) & (u2 `2 ) <= (w `2 ) & (w `2 ) <= (u `2 ) };

                    n < (n + 1) by NAT_1: 13;

                    then

                     A195: (u1 `2 ) < (u `2 ) by A107, A191, A183, A192, A184;

                    then

                     A196: u1 in lg by A185, A190;

                    u = |[(u `1 ), (u `2 )]| & u2 = |[(u2 `1 ), (u2 `2 )]| by EUCLID: 53;

                    then ( LSeg ((g2 /. n),(g2 /. (n + 2)))) = lg by A192, A193, A187, A188, A190, A195, TOPREAL3: 9, XXREAL_0: 2;

                    hence thesis by A192, A184, A187, A194, A189, A196, TOPREAL1: 8;

                  end;

                  thus g is unfolded

                  proof

                    let n be Nat;

                    assume that

                     A197: 1 <= n and

                     A198: (n + 2) <= ( len g);

                    

                     A199: ((n + 1) + 1) <= ( len g) by A198;

                    

                     A200: (n + (1 + 1)) = ((n + 1) + 1);

                    

                     A201: n <= (n + 1) by NAT_1: 11;

                    (n + 1) <= ((n + 1) + 1) by NAT_1: 11;

                    then

                     A202: (n + 1) <= ( len g) by A198, XXREAL_0: 2;

                    

                     A203: ( len g) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

                    ((n + 2) - ( len g1)) = ((n - ( len g1)) + 2);

                    then

                     A204: ((n - ( len g1)) + 2) <= ( len g2) by A198, A203, XREAL_1: 20;

                    

                     A205: 1 <= (n + 1) & ((n + 1) + 1) = (n + (1 + 1)) by NAT_1: 11;

                    per cases ;

                      suppose

                       A206: (n + 2) <= ( len g1);

                      

                       A207: (n + (1 + 1)) = ((n + 1) + 1);

                      

                       A208: (n + 1) in ( dom g1) by A197, A206, SEQ_4: 135;

                      then

                       A209: (g /. (n + 1)) = (g1 /. (n + 1)) by FINSEQ_4: 68;

                      n in ( dom g1) by A197, A206, SEQ_4: 135;

                      then

                       A210: ( LSeg (g1,n)) = ( LSeg (g,n)) by A208, TOPREAL3: 18;

                      (n + 2) in ( dom g1) by A197, A206, SEQ_4: 135;

                      then ( LSeg (g1,(n + 1))) = ( LSeg (g,(n + 1))) by A208, A207, TOPREAL3: 18;

                      hence thesis by A41, A197, A206, A210, A209;

                    end;

                      suppose ( len g1) < (n + 2);

                      then (( len g1) + 1) <= (n + 2) by NAT_1: 13;

                      then

                       A211: ( len g1) <= ((n + 2) - 1) by XREAL_1: 19;

                      now

                        per cases ;

                          suppose

                           A212: ( len g1) = (n + 1);

                          now

                            1 < ( len g1) by A197, A212, NAT_1: 13;

                            then

                             A213: (1 + 1) <= ( len g1) by NAT_1: 13;

                            assume k = 1;

                            hence contradiction by A52, A213, TOPREAL1: 23;

                          end;

                          then 1 < k by A24, XXREAL_0: 1;

                          then

                           A214: (( L~ f1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, GOBOARD2: 4;

                          (g /. (n + 1)) in ( LSeg (g,n)) & (g /. (n + 1)) in ( LSeg (g,(n + 1))) by A197, A198, A202, A205, TOPREAL1: 21;

                          then (g /. (n + 1)) in (( LSeg (g,n)) /\ ( LSeg (g,(n + 1)))) by XBOOLE_0:def 4;

                          then

                           A215: {(g /. (n + 1))} c= (( LSeg (g,n)) /\ ( LSeg (g,(n + 1)))) by ZFMISC_1: 31;

                          

                           A216: 1 <= (( len g) - ( len g1)) by A199, A212, XREAL_1: 19;

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

                          then

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

                          then (g2 /. 1) in lk by A152, A153;

                          then

                          consider u1 be Point of ( TOP-REAL 2) such that

                           A218: (g2 /. 1) = u1 and (u1 `1 ) = (ppi `1 ) and (pj `2 ) <= (u1 `2 ) and (u1 `2 ) <= (ppi `2 );

                          ppi in ( LSeg (ppi,pj)) by RLTOPSP1: 68;

                          then

                           A219: ( LSeg (ppi,u1)) c= ( LSeg (f,k)) by A172, A153, A217, A218, TOPREAL1: 6;

                          1 <= (n + 1) by NAT_1: 11;

                          then

                           A220: (n + 1) in ( dom g1) by A212, FINSEQ_3: 25;

                          

                          then

                           A221: (g /. (n + 1)) = (f1 /. ( len f1)) by A46, A212, FINSEQ_4: 68

                          .= ppi by A27, A14, A51, A29, FINSEQ_4: 71;

                          n in ( dom g1) by A197, A201, A212, FINSEQ_3: 25;

                          then

                           A222: ( LSeg (g,n)) = ( LSeg (g1,n)) by A220, TOPREAL3: 18;

                          (g /. (n + 2)) = (g2 /. 1) by A200, A203, A212, A216, SEQ_4: 136;

                          then

                           A223: ( LSeg (g,(n + 1))) = ( LSeg (ppi,u1)) by A198, A205, A221, A218, TOPREAL1:def 3;

                          ( LSeg (g1,n)) c= ( L~ f1) by A44, TOPREAL3: 19;

                          then (( LSeg (g,n)) /\ ( LSeg (g,(n + 1)))) c= {(g /. (n + 1))} by A29, A214, A222, A221, A219, A223, XBOOLE_1: 27;

                          hence thesis by A215;

                        end;

                          suppose ( len g1) <> (n + 1);

                          then ( len g1) < (n + 1) by A211, XXREAL_0: 1;

                          then

                           A224: ( len g1) <= n by NAT_1: 13;

                          then

                          reconsider n1 = (n - ( len g1)) as Element of NAT by INT_1: 5;

                          now

                            per cases ;

                              suppose

                               A225: ( len g1) = n;

                              then 1 <= ( len g2) by A202, A203, XREAL_1: 6;

                              then

                               A226: (g /. (n + 1)) = (g2 /. 1) by A225, SEQ_4: 136;

                              

                               A227: ( 0 + 2) <= ( len g2) by A198, A203, A225, XREAL_1: 6;

                              then 1 <= ( len g2) by XXREAL_0: 2;

                              then

                               A228: 1 in ( dom g2) by FINSEQ_3: 25;

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

                              then (g2 /. 1) in lk by A152, A153;

                              then

                              consider u1 be Point of ( TOP-REAL 2) such that

                               A229: (g2 /. 1) = u1 and

                               A230: (u1 `1 ) = (ppi `1 ) and (pj `2 ) <= (u1 `2 ) and

                               A231: (u1 `2 ) <= (ppi `2 );

                              

                               A232: 2 in ( dom g2) by A227, FINSEQ_3: 25;

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

                              then (g2 /. 2) in lk by A152, A153;

                              then

                              consider u2 be Point of ( TOP-REAL 2) such that

                               A233: (g2 /. 2) = u2 and

                               A234: (u2 `1 ) = (ppi `1 ) and (pj `2 ) <= (u2 `2 ) and

                               A235: (u2 `2 ) <= (ppi `2 );

                              set lg = { w where w be Point of ( TOP-REAL 2) : (w `1 ) = (ppi `1 ) & (u2 `2 ) <= (w `2 ) & (w `2 ) <= (ppi `2 ) };

                              (u2 `2 ) < (u1 `2 ) by A107, A228, A232, A229, A233;

                              then

                               A236: u1 in lg by A230, A231;

                              u2 = |[(u2 `1 ), (u2 `2 )]| by EUCLID: 53;

                              then

                               A237: ( LSeg (ppi,(g2 /. 2))) = lg by A83, A233, A234, A235, TOPREAL3: 9;

                              1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                              then ( len g1) in ( dom g1) by FINSEQ_3: 25;

                              

                              then (g /. n) = (f1 /. ( len f1)) by A46, A225, FINSEQ_4: 68

                              .= ppi by A27, A14, A51, A29, FINSEQ_4: 71;

                              then

                               A238: ( LSeg (g,n)) = ( LSeg (ppi,u1)) by A197, A202, A226, A229, TOPREAL1:def 3;

                              2 <= ( len g2) by A198, A203, A225, XREAL_1: 6;

                              then (g /. (n + 2)) = (g2 /. 2) by A225, SEQ_4: 136;

                              then ( LSeg (g,(n + 1))) = ( LSeg (u1,u2)) by A198, A205, A226, A229, A233, TOPREAL1:def 3;

                              hence thesis by A226, A229, A233, A236, A238, A237, TOPREAL1: 8;

                            end;

                              suppose ( len g1) <> n;

                              then

                               A239: ( len g1) < n by A224, XXREAL_0: 1;

                              then (( len g1) + 1) <= n by NAT_1: 13;

                              then

                               A240: 1 <= n1 by XREAL_1: 19;

                              (n1 + ( len g1)) = n;

                              then

                               A241: ( LSeg (g,n)) = ( LSeg (g2,n1)) by A202, A239, GOBOARD2: 5;

                              

                               A242: (n + 1) = ((n1 + 1) + ( len g1));

                              ((n1 + 1) + ( len g1)) = (n + 1);

                              then (n1 + 1) <= ( len g2) by A202, A203, XREAL_1: 6;

                              then

                               A243: (g /. (n + 1)) = (g2 /. (n1 + 1)) by A242, NAT_1: 11, SEQ_4: 136;

                              ( len g1) < (n + 1) by A201, A239, XXREAL_0: 2;

                              then ( LSeg (g,(n + 1))) = ( LSeg (g2,(n1 + 1))) by A199, A242, GOBOARD2: 5;

                              hence thesis by A180, A204, A241, A243, A240;

                            end;

                          end;

                          hence thesis;

                        end;

                      end;

                      hence thesis;

                    end;

                  end;

                  

                   A244: ( L~ g2) c= ( LSeg (f,k))

                  proof

                    let x be object;

                    set ls = { ( LSeg (g2,m)) : 1 <= m & (m + 1) <= ( len g2) };

                    assume x in ( L~ g2);

                    then

                    consider X be set such that

                     A245: x in X and

                     A246: X in ls by TARSKI:def 4;

                    consider m such that

                     A247: X = ( LSeg (g2,m)) and

                     A248: 1 <= m & (m + 1) <= ( len g2) by A246;

                    reconsider q1 = (g2 /. m), q2 = (g2 /. (m + 1)) as Point of ( TOP-REAL 2);

                    

                     A249: ( LSeg (g2,m)) = ( LSeg (q1,q2)) by A248, TOPREAL1:def 3;

                    (m + 1) in ( dom g2) by A248, SEQ_4: 134;

                    then

                     A250: (g2 /. (m + 1)) in ( rng g2) by PARTFUN2: 2;

                    m in ( dom g2) by A248, SEQ_4: 134;

                    then (g2 /. m) in ( rng g2) by PARTFUN2: 2;

                    then ( LSeg (q1,q2)) c= ( LSeg (ppi,pj)) by A172, A153, A250, TOPREAL1: 6;

                    hence thesis by A172, A245, A247, A249;

                  end;

                  

                   A251: (( L~ g1) /\ ( L~ g2)) = {}

                  proof

                    per cases ;

                      suppose k = 1;

                      hence thesis by A52;

                    end;

                      suppose k <> 1;

                      then 1 < k by A24, XXREAL_0: 1;

                      then (( L~ g1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, A44, GOBOARD2: 4;

                      then

                       A252: (( L~ g1) /\ ( L~ g2)) c= {(f /. k)} by A244, XBOOLE_1: 26;

                      now

                        set x = the Element of (( L~ g1) /\ ( L~ g2));

                        assume (( L~ g1) /\ ( L~ g2)) <> {} ;

                        then x in {(f /. k)} & x in ( L~ g2) by A252, XBOOLE_0:def 4;

                        hence contradiction by A134, TARSKI:def 1;

                      end;

                      hence thesis;

                    end;

                  end;

                  for n, m st m > (n + 1) & n in ( dom g) & (n + 1) in ( dom g) & m in ( dom g) & (m + 1) in ( dom g) holds ( LSeg (g,n)) misses ( LSeg (g,m))

                  proof

                    

                     A253: 1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                    then ( len g1) in ( dom g1) by FINSEQ_3: 25;

                    

                    then

                     A254: (g /. ( len g1)) = (g1 /. ( len g1)) by FINSEQ_4: 68

                    .= ppi by A27, A14, A51, A46, A29, FINSEQ_4: 71;

                    reconsider qq = (g2 /. 1) as Point of ( TOP-REAL 2);

                    set l1 = { ( LSeg (g1,i)) : 1 <= i & (i + 1) <= ( len g1) }, l2 = { ( LSeg (g2,j)) : 1 <= j & (j + 1) <= ( len g2) };

                    let n, m;

                    assume that

                     A255: m > (n + 1) and

                     A256: n in ( dom g) and

                     A257: (n + 1) in ( dom g) and

                     A258: m in ( dom g) and

                     A259: (m + 1) in ( dom g);

                    

                     A260: 1 <= n by A256, FINSEQ_3: 25;

                    (j2 + 1) <= i2 by A77, NAT_1: 13;

                    then

                     A261: 1 <= l by XREAL_1: 19;

                    then

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

                    then

                     A263: (qq `1 ) = (ppi `1 ) & (qq `2 ) < (ppi `2 ) by A95;

                    

                     A264: (g /. (( len g1) + 1)) = qq by A89, A261, SEQ_4: 136;

                    

                     A265: (pj `2 ) <= (qq `2 ) by A95, A262;

                    

                     A266: (m + 1) <= ( len g) by A259, FINSEQ_3: 25;

                    

                     A267: 1 <= (m + 1) by A259, FINSEQ_3: 25;

                    

                     A268: 1 <= (n + 1) by A257, FINSEQ_3: 25;

                    

                     A269: (n + 1) <= ( len g) by A257, FINSEQ_3: 25;

                    

                     A270: qq = |[(qq `1 ), (qq `2 )]| by EUCLID: 53;

                    

                     A271: 1 <= m by A258, FINSEQ_3: 25;

                    set ql = { z where z be Point of ( TOP-REAL 2) : (z `1 ) = (ppi `1 ) & (qq `2 ) <= (z `2 ) & (z `2 ) <= (ppi `2 ) };

                    

                     A272: n <= (n + 1) by NAT_1: 11;

                    

                     A273: ( len g) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

                    then (( len g1) + 1) <= ( len g) by A89, A261, XREAL_1: 7;

                    

                    then

                     A274: ( LSeg (g,( len g1))) = ( LSeg (qq,ppi)) by A253, A254, A264, TOPREAL1:def 3

                    .= ql by A83, A263, A270, TOPREAL3: 9;

                    

                     A275: m <= (m + 1) by NAT_1: 11;

                    then

                     A276: (n + 1) <= (m + 1) by A255, XXREAL_0: 2;

                    now

                      per cases ;

                        suppose

                         A277: (m + 1) <= ( len g1);

                        then m <= ( len g1) by A275, XXREAL_0: 2;

                        then

                         A278: m in ( dom g1) by A271, FINSEQ_3: 25;

                        (m + 1) in ( dom g1) by A267, A277, FINSEQ_3: 25;

                        then

                         A279: ( LSeg (g,m)) = ( LSeg (g1,m)) by A278, TOPREAL3: 18;

                        

                         A280: (n + 1) <= ( len g1) by A276, A277, XXREAL_0: 2;

                        then n <= ( len g1) by A272, XXREAL_0: 2;

                        then

                         A281: n in ( dom g1) by A260, FINSEQ_3: 25;

                        (n + 1) in ( dom g1) by A268, A280, FINSEQ_3: 25;

                        then ( LSeg (g,n)) = ( LSeg (g1,n)) by A281, TOPREAL3: 18;

                        hence thesis by A42, A255, A279;

                      end;

                        suppose ( len g1) < (m + 1);

                        then

                         A282: ( len g1) <= m by NAT_1: 13;

                        then

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

                        now

                          per cases ;

                            suppose

                             A283: m = ( len g1);

                            

                             A284: ( LSeg (g,m)) c= ( LSeg (f,k))

                            proof

                              let x be object;

                              assume x in ( LSeg (g,m));

                              then

                              consider px be Point of ( TOP-REAL 2) such that

                               A285: px = x & (px `1 ) = (ppi `1 ) and

                               A286: (qq `2 ) <= (px `2 ) and

                               A287: (px `2 ) <= (ppi `2 ) by A274, A283;

                              (pj `2 ) <= (px `2 ) by A265, A286, XXREAL_0: 2;

                              hence thesis by A152, A285, A287;

                            end;

                            n <= ( len g1) by A255, A272, A283, XXREAL_0: 2;

                            then

                             A288: n in ( dom g1) by A260, FINSEQ_3: 25;

                            now

                              1 < ( len g1) by A255, A268, A283, XXREAL_0: 2;

                              then

                               A289: (1 + 1) <= ( len g1) by NAT_1: 13;

                              assume k = 1;

                              hence contradiction by A52, A289, TOPREAL1: 23;

                            end;

                            then 1 < k by A24, XXREAL_0: 1;

                            then

                             A290: (( L~ f1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, GOBOARD2: 4;

                            

                             A291: (n + 1) in ( dom g1) by A255, A268, A283, FINSEQ_3: 25;

                            then

                             A292: ( LSeg (g,n)) = ( LSeg (g1,n)) by A288, TOPREAL3: 18;

                            then ( LSeg (g,n)) in l1 by A255, A260, A283;

                            then ( LSeg (g,n)) c= ( L~ f1) by A44, ZFMISC_1: 74;

                            then

                             A293: (( LSeg (g,n)) /\ ( LSeg (g,m))) c= {(f /. k)} by A290, A284, XBOOLE_1: 27;

                            now

                              set x = the Element of (( LSeg (g,n)) /\ ( LSeg (g,m)));

                              assume

                               A294: (( LSeg (g,n)) /\ ( LSeg (g,m))) <> {} ;

                              then

                               A295: x in ( LSeg (g,n)) by XBOOLE_0:def 4;

                              x in {(f /. k)} by A293, A294;

                              then

                               A296: x = (f /. k) by TARSKI:def 1;

                              (f /. k) = (g1 /. ( len g1)) by A27, A14, A51, A46, FINSEQ_4: 71;

                              hence contradiction by A40, A41, A42, A255, A283, A288, A291, A292, A295, A296, GOBOARD2: 2;

                            end;

                            hence thesis;

                          end;

                            suppose m <> ( len g1);

                            then

                             A297: ( len g1) < m by A282, XXREAL_0: 1;

                            then (( len g1) + 1) <= m by NAT_1: 13;

                            then

                             A298: 1 <= m1 by XREAL_1: 19;

                            (m + 1) = ((m1 + 1) + ( len g1));

                            then

                             A299: (m1 + 1) <= ( len g2) by A266, A273, XREAL_1: 6;

                            m = (m1 + ( len g1));

                            then

                             A300: ( LSeg (g,m)) = ( LSeg (g2,m1)) by A266, A297, GOBOARD2: 5;

                            then ( LSeg (g,m)) in l2 by A298, A299;

                            then

                             A301: ( LSeg (g,m)) c= ( L~ g2) by ZFMISC_1: 74;

                            now

                              per cases ;

                                suppose

                                 A302: (n + 1) <= ( len g1);

                                then n <= ( len g1) by A272, XXREAL_0: 2;

                                then

                                 A303: n in ( dom g1) by A260, FINSEQ_3: 25;

                                (n + 1) in ( dom g1) by A268, A302, FINSEQ_3: 25;

                                then ( LSeg (g,n)) = ( LSeg (g1,n)) by A303, TOPREAL3: 18;

                                then ( LSeg (g,n)) in l1 by A260, A302;

                                then ( LSeg (g,n)) c= ( L~ g1) by ZFMISC_1: 74;

                                then (( LSeg (g,n)) /\ ( LSeg (g,m))) = {} by A251, A301, XBOOLE_1: 3, XBOOLE_1: 27;

                                hence thesis;

                              end;

                                suppose ( len g1) < (n + 1);

                                then

                                 A304: ( len g1) <= n by NAT_1: 13;

                                then

                                reconsider n1 = (n - ( len g1)) as Element of NAT by INT_1: 5;

                                

                                 A305: ((n - ( len g1)) + 1) = ((n + 1) - ( len g1));

                                

                                 A306: n = (n1 + ( len g1));

                                now

                                  per cases ;

                                    suppose

                                     A307: ( len g1) = n;

                                    now

                                      reconsider q1 = (g2 /. m1), q2 = (g2 /. (m1 + 1)) as Point of ( TOP-REAL 2);

                                      set x = the Element of (( LSeg (g,n)) /\ ( LSeg (g,m)));

                                      set q1l = { v where v be Point of ( TOP-REAL 2) : (v `1 ) = (ppi `1 ) & (q2 `2 ) <= (v `2 ) & (v `2 ) <= (q1 `2 ) };

                                      

                                       A308: q1 = |[(q1 `1 ), (q1 `2 )]| & q2 = |[(q2 `1 ), (q2 `2 )]| by EUCLID: 53;

                                      assume

                                       A309: (( LSeg (g,n)) /\ ( LSeg (g,m))) <> {} ;

                                      then

                                       A310: x in ( LSeg (g,m)) by XBOOLE_0:def 4;

                                      x in ( LSeg (g,n)) by A309, XBOOLE_0:def 4;

                                      then

                                       A311: ex qx be Point of ( TOP-REAL 2) st qx = x & (qx `1 ) = (ppi `1 ) & (qq `2 ) <= (qx `2 ) & (qx `2 ) <= (ppi `2 ) by A274, A307;

                                      

                                       A312: m1 in ( dom g2) by A298, A299, SEQ_4: 134;

                                      then

                                       A313: (q1 `1 ) = (ppi `1 ) by A95;

                                      

                                       A314: (m1 + 1) in ( dom g2) by A298, A299, SEQ_4: 134;

                                      then

                                       A315: (q2 `1 ) = (ppi `1 ) by A95;

                                      m1 < (m1 + 1) by NAT_1: 13;

                                      then

                                       A316: (q2 `2 ) < (q1 `2 ) by A107, A312, A314;

                                      ( LSeg (g2,m1)) = ( LSeg (q2,q1)) by A298, A299, TOPREAL1:def 3

                                      .= q1l by A313, A315, A316, A308, TOPREAL3: 9;

                                      then

                                       A317: ex qy be Point of ( TOP-REAL 2) st qy = x & (qy `1 ) = (ppi `1 ) & (q2 `2 ) <= (qy `2 ) & (qy `2 ) <= (q1 `2 ) by A300, A310;

                                      m1 > (n1 + 1) & (n1 + 1) >= 1 by A255, A305, NAT_1: 11, XREAL_1: 9;

                                      then m1 > 1 by XXREAL_0: 2;

                                      then (q1 `2 ) < (qq `2 ) by A107, A262, A312;

                                      hence contradiction by A311, A317, XXREAL_0: 2;

                                    end;

                                    hence thesis;

                                  end;

                                    suppose n <> ( len g1);

                                    then ( len g1) < n by A304, XXREAL_0: 1;

                                    then

                                     A318: ( LSeg (g,n)) = ( LSeg (g2,n1)) by A269, A306, GOBOARD2: 5;

                                    m1 > (n1 + 1) by A255, A305, XREAL_1: 9;

                                    hence thesis by A133, A300, A318;

                                  end;

                                end;

                                hence thesis;

                              end;

                            end;

                            hence thesis;

                          end;

                        end;

                        hence thesis;

                      end;

                    end;

                    hence thesis;

                  end;

                  hence g is s.n.c. by GOBOARD2: 1;

                  now

                    set p = (g1 /. ( len g1)), q = (g2 /. 1);

                    (j2 + 1) <= i2 by A77, NAT_1: 13;

                    then 1 <= l by XREAL_1: 19;

                    then 1 in ( dom g2) by A90, FINSEQ_1: 1;

                    then (q `1 ) = (ppi `1 ) by A95;

                    hence (p `1 ) = (q `1 ) or (p `2 ) = (q `2 ) by A27, A14, A51, A46, A29, FINSEQ_4: 71;

                  end;

                  hence g is special by A43, A104, GOBOARD2: 8;

                  thus ( L~ g) = ( L~ f)

                  proof

                    set lg = { ( LSeg (g,i)) : 1 <= i & (i + 1) <= ( len g) }, lf = { ( LSeg (f,j)) : 1 <= j & (j + 1) <= ( len f) };

                    

                     A319: ( len g) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

                     A320:

                    now

                      let j;

                      assume that

                       A321: ( len g1) <= j and

                       A322: j <= ( len g);

                      reconsider w = (j - ( len g1)) as Element of NAT by A321, INT_1: 5;

                      let p such that

                       A323: p = (g /. j);

                      now

                        per cases ;

                          suppose

                           A324: j = ( len g1);

                          1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                          then ( len g1) in ( dom g1) by FINSEQ_3: 25;

                          

                          then

                           A325: (g /. ( len g1)) = (f1 /. ( len f1)) by A46, FINSEQ_4: 68

                          .= (G * (i1,i2)) by A27, A14, A51, A29, FINSEQ_4: 71;

                          hence (p `1 ) = ((G * (i1,i2)) `1 ) by A323, A324;

                          thus ((G * (i1,j2)) `2 ) <= (p `2 ) & (p `2 ) <= ((G * (i1,i2)) `2 ) by A68, A74, A71, A30, A72, A77, A79, A81, A323, A324, A325, SEQM_3:def 1;

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

                          hence p in ( rng l1) by A68, A72, A78, A323, A324, A325, PARTFUN2: 2;

                        end;

                          suppose j <> ( len g1);

                          then ( len g1) < j by A321, XXREAL_0: 1;

                          then (( len g1) + 1) <= j by NAT_1: 13;

                          then

                           A326: 1 <= w by XREAL_1: 19;

                          

                           A327: w <= ( len g2) by A319, A322, XREAL_1: 20;

                          then

                           A328: w in ( dom g2) by A326, FINSEQ_3: 25;

                          (w + ( len g1)) = j;

                          then (g /. j) = (g2 /. w) by A326, A327, SEQ_4: 136;

                          hence (p `1 ) = (ppi `1 ) & (pj `2 ) <= (p `2 ) & (p `2 ) <= (ppi `2 ) & p in ( rng l1) by A95, A323, A328;

                        end;

                      end;

                      hence (p `1 ) = (ppi `1 ) & (pj `2 ) <= (p `2 ) & (p `2 ) <= (ppi `2 ) & p in ( rng l1);

                    end;

                    thus ( L~ g) c= ( L~ f)

                    proof

                      let x be object;

                      assume x in ( L~ g);

                      then

                      consider X be set such that

                       A329: x in X and

                       A330: X in lg by TARSKI:def 4;

                      consider i such that

                       A331: X = ( LSeg (g,i)) and

                       A332: 1 <= i and

                       A333: (i + 1) <= ( len g) by A330;

                      per cases ;

                        suppose

                         A334: (i + 1) <= ( len g1);

                        i <= (i + 1) by NAT_1: 11;

                        then i <= ( len g1) by A334, XXREAL_0: 2;

                        then

                         A335: i in ( dom g1) by A332, FINSEQ_3: 25;

                        1 <= (i + 1) by NAT_1: 11;

                        then (i + 1) in ( dom g1) by A334, FINSEQ_3: 25;

                        then X = ( LSeg (g1,i)) by A331, A335, TOPREAL3: 18;

                        then X in { ( LSeg (g1,j)) : 1 <= j & (j + 1) <= ( len g1) } by A332, A334;

                        then

                         A336: x in ( L~ f1) by A44, A329, TARSKI:def 4;

                        ( L~ f1) c= ( L~ f) by TOPREAL3: 20;

                        hence thesis by A336;

                      end;

                        suppose

                         A337: (i + 1) > ( len g1);

                        reconsider q1 = (g /. i), q2 = (g /. (i + 1)) as Point of ( TOP-REAL 2);

                        

                         A338: i <= ( len g) by A333, NAT_1: 13;

                        

                         A339: ( len g1) <= i by A337, NAT_1: 13;

                        then

                         A340: (q1 `1 ) = (ppi `1 ) by A320, A338;

                        

                         A341: (q1 `2 ) <= (ppi `2 ) by A320, A339, A338;

                        

                         A342: (pj `2 ) <= (q1 `2 ) by A320, A339, A338;

                        (q2 `1 ) = (ppi `1 ) by A320, A333, A337;

                        then

                         A343: q2 = |[(q1 `1 ), (q2 `2 )]| by A340, EUCLID: 53;

                        

                         A344: (q2 `2 ) <= (ppi `2 ) by A320, A333, A337;

                        

                         A345: q1 = |[(q1 `1 ), (q1 `2 )]| & ( LSeg (g,i)) = ( LSeg (q2,q1)) by A332, A333, EUCLID: 53, TOPREAL1:def 3;

                        

                         A346: (pj `2 ) <= (q2 `2 ) by A320, A333, A337;

                        now

                          per cases by XXREAL_0: 1;

                            suppose (q1 `2 ) > (q2 `2 );

                            then ( LSeg (g,i)) = { p2 : (p2 `1 ) = (q1 `1 ) & (q2 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q1 `2 ) } by A343, A345, TOPREAL3: 9;

                            then

                            consider p2 such that

                             A347: p2 = x & (p2 `1 ) = (q1 `1 ) and

                             A348: (q2 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q1 `2 ) by A329, A331;

                            (pj `2 ) <= (p2 `2 ) & (p2 `2 ) <= (ppi `2 ) by A341, A346, A348, XXREAL_0: 2;

                            then

                             A349: x in ( LSeg (f,k)) by A152, A340, A347;

                            ( LSeg (f,k)) in lf by A3, A24;

                            hence thesis by A349, TARSKI:def 4;

                          end;

                            suppose (q1 `2 ) = (q2 `2 );

                            then ( LSeg (g,i)) = {q1} by A343, A345, RLTOPSP1: 70;

                            then x = q1 by A329, A331, TARSKI:def 1;

                            then

                             A350: x in ( LSeg (f,k)) by A152, A340, A342, A341;

                            ( LSeg (f,k)) in lf by A3, A24;

                            hence thesis by A350, TARSKI:def 4;

                          end;

                            suppose (q1 `2 ) < (q2 `2 );

                            then ( LSeg (g,i)) = { p1 : (p1 `1 ) = (q1 `1 ) & (q1 `2 ) <= (p1 `2 ) & (p1 `2 ) <= (q2 `2 ) } by A343, A345, TOPREAL3: 9;

                            then

                            consider p2 such that

                             A351: p2 = x & (p2 `1 ) = (q1 `1 ) and

                             A352: (q1 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q2 `2 ) by A329, A331;

                            (pj `2 ) <= (p2 `2 ) & (p2 `2 ) <= (ppi `2 ) by A342, A344, A352, XXREAL_0: 2;

                            then

                             A353: x in ( LSeg (f,k)) by A152, A340, A351;

                            ( LSeg (f,k)) in lf by A3, A24;

                            hence thesis by A353, TARSKI:def 4;

                          end;

                        end;

                        hence thesis;

                      end;

                    end;

                    let x be object;

                    assume x in ( L~ f);

                    then

                     A354: x in (( L~ f1) \/ ( LSeg (f,k))) by A3, A13, GOBOARD2: 3;

                    per cases by A354, XBOOLE_0:def 3;

                      suppose

                       A355: x in ( L~ f1);

                      ( L~ g1) c= ( L~ g) by GOBOARD2: 6;

                      hence thesis by A44, A355;

                    end;

                      suppose x in ( LSeg (f,k));

                      then

                      consider p1 such that

                       A356: p1 = x and

                       A357: (p1 `1 ) = (ppi `1 ) and

                       A358: (pj `2 ) <= (p1 `2 ) and

                       A359: (p1 `2 ) <= (ppi `2 ) by A152;

                      defpred P2[ Nat] means ( len g1) <= $1 & $1 <= ( len g) & for q st q = (g /. $1) holds (q `2 ) >= (p1 `2 );

                       A360:

                      now

                        reconsider n = ( len g1) as Nat;

                        take n;

                        thus P2[n]

                        proof

                          thus ( len g1) <= n & n <= ( len g) by A319, XREAL_1: 31;

                          1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                          then

                           A361: ( len g1) in ( dom g1) by FINSEQ_3: 25;

                          let q;

                          assume q = (g /. n);

                          

                          then q = (f1 /. ( len f1)) by A46, A361, FINSEQ_4: 68

                          .= (G * (i1,i2)) by A27, A14, A51, A29, FINSEQ_4: 71;

                          hence thesis by A359;

                        end;

                      end;

                      

                       A362: for n be Nat holds P2[n] implies n <= ( len g);

                      consider ma be Nat such that

                       A363: P2[ma] & for n be Nat st P2[n] holds n <= ma from NAT_1:sch 6( A362, A360);

                      reconsider ma as Element of NAT by ORDINAL1:def 12;

                      now

                        per cases ;

                          suppose

                           A364: ma = ( len g);

                          (j2 + 1) <= i2 by A77, NAT_1: 13;

                          then

                           A365: 1 <= l by XREAL_1: 19;

                          then (( len g1) + 1) <= ma by A89, A319, A364, XREAL_1: 7;

                          then

                           A366: ( len g1) <= (ma - 1) by XREAL_1: 19;

                          then ( 0 + 1) <= ma by XREAL_1: 19;

                          then

                          reconsider m1 = (ma - 1) as Element of NAT by INT_1: 5;

                          reconsider q = (g /. m1) as Point of ( TOP-REAL 2);

                          

                           A367: (ma - 1) <= ( len g) by A364, XREAL_1: 43;

                          then

                           A368: (q `1 ) = (ppi `1 ) by A320, A366;

                          

                           A369: (pj `2 ) <= (q `2 ) by A320, A367, A366;

                          set lq = { e where e be Point of ( TOP-REAL 2) : (e `1 ) = (ppi `1 ) & (pj `2 ) <= (e `2 ) & (e `2 ) <= (q `2 ) };

                          

                           A370: (i2 - l) = j2;

                          

                           A371: l in ( dom g2) by A89, A365, FINSEQ_3: 25;

                          

                          then

                           A372: (g /. ma) = (g2 /. l) by A89, A319, A364, FINSEQ_4: 69

                          .= pj by A89, A90, A371, A370;

                          then (p1 `2 ) <= (pj `2 ) by A363;

                          then

                           A373: (p1 `2 ) = (pj `2 ) by A358, XXREAL_0: 1;

                          1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                          then

                           A374: 1 <= m1 by A366, XXREAL_0: 2;

                          

                           A375: (m1 + 1) = ma;

                          then q = |[(q `1 ), (q `2 )]| & ( LSeg (g,m1)) = ( LSeg (pj,q)) by A364, A372, A374, EUCLID: 53, TOPREAL1:def 3;

                          then ( LSeg (g,m1)) = lq by A145, A151, A368, A369, TOPREAL3: 9;

                          then

                           A376: p1 in ( LSeg (g,m1)) by A357, A373, A369;

                          ( LSeg (g,m1)) in lg by A364, A374, A375;

                          hence thesis by A356, A376, TARSKI:def 4;

                        end;

                          suppose ma <> ( len g);

                          then ma < ( len g) by A363, XXREAL_0: 1;

                          then

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

                          reconsider qa = (g /. ma), qa1 = (g /. (ma + 1)) as Point of ( TOP-REAL 2);

                          set lma = { p2 : (p2 `1 ) = (ppi `1 ) & (qa1 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (qa `2 ) };

                          

                           A378: qa1 = |[(qa1 `1 ), (qa1 `2 )]| by EUCLID: 53;

                          

                           A379: (p1 `2 ) <= (qa `2 ) by A363;

                          

                           A380: ( len g1) <= (ma + 1) by A363, NAT_1: 13;

                          then

                           A381: (qa1 `1 ) = (ppi `1 ) by A320, A377;

                           A382:

                          now

                            assume (p1 `2 ) <= (qa1 `2 );

                            then for q holds q = (g /. (ma + 1)) implies (p1 `2 ) <= (q `2 );

                            then (ma + 1) <= ma by A363, A377, A380;

                            hence contradiction by XREAL_1: 29;

                          end;

                          

                           A383: (qa `1 ) = (ppi `1 ) & qa = |[(qa `1 ), (qa `2 )]| by A320, A363, EUCLID: 53;

                          

                           A384: 1 <= ma by A24, A14, A47, A363, NAT_1: 13;

                          

                          then ( LSeg (g,ma)) = ( LSeg (qa1,qa)) by A377, TOPREAL1:def 3

                          .= lma by A379, A382, A381, A383, A378, TOPREAL3: 9, XXREAL_0: 2;

                          then

                           A385: x in ( LSeg (g,ma)) by A356, A357, A379, A382;

                          ( LSeg (g,ma)) in lg by A377, A384;

                          hence thesis by A385, TARSKI:def 4;

                        end;

                      end;

                      hence thesis;

                    end;

                  end;

                  

                   A386: ( len g) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

                  1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                  then 1 in ( dom g1) by FINSEQ_3: 25;

                  

                  hence (g /. 1) = (f1 /. 1) by A45, FINSEQ_4: 68

                  .= (f /. 1) by A27, A25, FINSEQ_4: 71;

                  (j2 + 1) <= i2 by A77, NAT_1: 13;

                  then

                   A387: 1 <= l by XREAL_1: 19;

                  then

                   A388: l in ( dom g2) by A90, FINSEQ_1: 1;

                  

                  hence (g /. ( len g)) = (g2 /. l) by A89, A386, FINSEQ_4: 69

                  .= (G * (i1,m1)) by A89, A90, A388

                  .= (f /. ( len f)) by A3, A21, A76;

                  thus ( len f) <= ( len g) by A3, A14, A47, A89, A387, A386, XREAL_1: 7;

                end;

                  case

                   A389: i2 = j2;

                  k <> (k + 1);

                  hence contradiction by A5, A27, A29, A19, A21, A76, A389, PARTFUN2: 10;

                end;

                  case

                   A390: i2 < j2;

                  (l1 /. i2) = (l1 . i2) by A68, A73, PARTFUN1:def 6;

                  then

                   A391: (l1 /. i2) = ppi by A68, MATRIX_0:def 7;

                  then

                   A392: (y1 . i2) = (ppi `2 ) by A68, A30, A72, GOBOARD1:def 2;

                  (l1 /. j2) = (l1 . j2) by A74, A73, PARTFUN1:def 6;

                  then

                   A393: (l1 /. j2) = pj by A74, MATRIX_0:def 7;

                  then

                   A394: (y1 . j2) = (pj `2 ) by A74, A30, A72, GOBOARD1:def 2;

                  then

                   A395: (ppi `2 ) < (pj `2 ) by A68, A74, A71, A30, A72, A390, A392, SEQM_3:def 1;

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

                  deffunc F( Nat) = (G * (i1,(i2 + $1)));

                  consider g2 such that

                   A396: ( len g2) = l & for n be Nat st n in ( dom g2) holds (g2 /. n) = F(n) from FINSEQ_4:sch 2;

                  take g = (g1 ^ g2);

                  

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

                   A398:

                  now

                    let n;

                    

                     A399: n <= (i2 + n) by NAT_1: 11;

                    assume

                     A400: n in ( Seg l);

                    then n <= l by FINSEQ_1: 1;

                    then

                     A401: (i2 + n) <= (l + i2) by XREAL_1: 7;

                    j2 <= ( width G) by A74, FINSEQ_1: 1;

                    then

                     A402: (i2 + n) <= ( width G) by A401, XXREAL_0: 2;

                    1 <= n by A400, FINSEQ_1: 1;

                    then 1 <= (i2 + n) by A399, XXREAL_0: 2;

                    hence (i2 + n) in ( Seg ( width G)) by A402, FINSEQ_1: 1;

                    hence [i1, (i2 + n)] in ( Indices G) by A22, A66, ZFMISC_1: 87;

                  end;

                  now

                    let n such that

                     A403: n in ( dom g2);

                    take m = i1, k = (i2 + n);

                    thus [m, k] in ( Indices G) & (g2 /. n) = (G * (m,k)) by A396, A398, A397, A403;

                  end;

                  then

                   A404: for n st n in ( dom g) holds ex i, j st [i, j] in ( Indices G) & (g /. n) = (G * (i,j)) by A75, GOBOARD1: 23;

                  

                   A405: (x1 . i2) = (ppi `1 ) by A68, A62, A72, A391, GOBOARD1:def 1;

                   A406:

                  now

                    let n, p;

                    assume that

                     A407: n in ( dom g2) and

                     A408: (g2 /. n) = p;

                    

                     A409: (g2 /. n) = (G * (i1,(i2 + n))) by A396, A407;

                    set n1 = (i2 + n);

                    set pn = (G * (i1,n1));

                    

                     A410: (i2 + n) in ( Seg ( width G)) by A396, A398, A397, A407;

                    then

                     A411: (x1 . n1) = (x1 . i2) by A68, A67, A62, A72, SEQM_3:def 10;

                    (l1 /. n1) = (l1 . n1) by A73, A396, A398, A397, A407, PARTFUN1:def 6;

                    then

                     A412: (l1 /. n1) = pn by A410, MATRIX_0:def 7;

                    then

                     A413: (y1 . n1) = (pn `2 ) by A30, A72, A410, GOBOARD1:def 2;

                    n <= ( len g2) by A397, A407, FINSEQ_1: 1;

                    then

                     A414: n1 <= (i2 + ( len g2)) by XREAL_1: 7;

                    (x1 . n1) = (pn `1 ) by A62, A72, A410, A412, GOBOARD1:def 1;

                    hence (p `1 ) = (ppi `1 ) & (ppi `2 ) <= (p `2 ) & (p `2 ) <= (pj `2 ) by A68, A74, A71, A30, A72, A396, A392, A394, A405, A408, A409, A410, A414, A411, A413, SEQ_4: 137, XREAL_1: 31;

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

                    hence p in ( rng l1) by A72, A408, A409, A410, A412, PARTFUN2: 2;

                    1 <= n by A397, A407, FINSEQ_1: 1;

                    then i2 < n1 by XREAL_1: 29;

                    hence (p `2 ) > (ppi `2 ) by A68, A71, A30, A72, A392, A408, A409, A410, A413, SEQM_3:def 1;

                  end;

                  

                   A415: g2 is special

                  proof

                    let n be Nat;

                    set p = (g2 /. n);

                    assume

                     A416: 1 <= n & (n + 1) <= ( len g2);

                    then n in ( dom g2) by SEQ_4: 134;

                    then

                     A417: (p `1 ) = (ppi `1 ) by A406;

                    (n + 1) in ( dom g2) by A416, SEQ_4: 134;

                    hence thesis by A406, A417;

                  end;

                  now

                    let n,m be Element of NAT ;

                    assume that

                     A418: n in ( dom g2) & m in ( dom g2) and

                     A419: n <> m;

                    

                     A420: (g2 /. n) = (G * (i1,(i2 + n))) & (g2 /. m) = (G * (i1,(i2 + m))) by A396, A418;

                    assume

                     A421: (g2 /. n) = (g2 /. m);

                     [i1, (i2 + n)] in ( Indices G) & [i1, (i2 + m)] in ( Indices G) by A396, A398, A397, A418;

                    then (i2 + n) = (i2 + m) by A420, A421, GOBOARD1: 5;

                    hence contradiction by A419;

                  end;

                  then for n,m be Element of NAT st n in ( dom g2) & m in ( dom g2) & (g2 /. n) = (g2 /. m) holds n = m;

                  then

                   A422: g2 is one-to-one by PARTFUN2: 9;

                  set lk = { w where w be Point of ( TOP-REAL 2) : (w `1 ) = (ppi `1 ) & (ppi `2 ) <= (w `2 ) & (w `2 ) <= (pj `2 ) };

                  

                   A423: ppi = |[(ppi `1 ), (ppi `2 )]| by EUCLID: 53;

                   A424:

                  now

                    let n, m, p, q;

                    assume that

                     A425: n in ( dom g2) and

                     A426: m in ( dom g2) and

                     A427: n < m and

                     A428: (g2 /. n) = p & (g2 /. m) = q;

                    

                     A429: (i2 + n) in ( Seg ( width G)) by A396, A398, A397, A425;

                    set n1 = (i2 + n), m1 = (i2 + m);

                    set pn = (G * (i1,n1)), pm = (G * (i1,m1));

                    

                     A430: n1 < m1 by A427, XREAL_1: 8;

                    (l1 /. n1) = (l1 . n1) by A73, A396, A398, A397, A425, PARTFUN1:def 6;

                    then (l1 /. n1) = pn by A429, MATRIX_0:def 7;

                    then

                     A431: (y1 . n1) = (pn `2 ) by A30, A72, A429, GOBOARD1:def 2;

                    

                     A432: (i2 + m) in ( Seg ( width G)) by A396, A398, A397, A426;

                    (l1 /. m1) = (l1 . m1) by A73, A396, A398, A397, A426, PARTFUN1:def 6;

                    then (l1 /. m1) = pm by A432, MATRIX_0:def 7;

                    then

                     A433: (y1 . m1) = (pm `2 ) by A30, A72, A432, GOBOARD1:def 2;

                    (g2 /. n) = (G * (i1,(i2 + n))) & (g2 /. m) = (G * (i1,(i2 + m))) by A396, A425, A426;

                    hence (p `2 ) < (q `2 ) by A71, A30, A72, A428, A429, A432, A430, A431, A433, SEQM_3:def 1;

                  end;

                  for n, m st m > (n + 1) & n in ( dom g2) & (n + 1) in ( dom g2) & m in ( dom g2) & (m + 1) in ( dom g2) holds ( LSeg (g2,n)) misses ( LSeg (g2,m))

                  proof

                    let n, m;

                    assume that

                     A434: m > (n + 1) and

                     A435: n in ( dom g2) and

                     A436: (n + 1) in ( dom g2) and

                     A437: m in ( dom g2) and

                     A438: (m + 1) in ( dom g2) and

                     A439: (( LSeg (g2,n)) /\ ( LSeg (g2,m))) <> {} ;

                    reconsider p1 = (g2 /. n), p2 = (g2 /. (n + 1)), q1 = (g2 /. m), q2 = (g2 /. (m + 1)) as Point of ( TOP-REAL 2);

                    

                     A440: (p1 `1 ) = (ppi `1 ) & (p2 `1 ) = (ppi `1 ) by A406, A435, A436;

                    n < (n + 1) by NAT_1: 13;

                    then

                     A441: (p1 `2 ) < (p2 `2 ) by A424, A435, A436;

                    set lp = { w where w be Point of ( TOP-REAL 2) : (w `1 ) = (ppi `1 ) & (p1 `2 ) <= (w `2 ) & (w `2 ) <= (p2 `2 ) }, lq = { w where w be Point of ( TOP-REAL 2) : (w `1 ) = (ppi `1 ) & (q1 `2 ) <= (w `2 ) & (w `2 ) <= (q2 `2 ) };

                    

                     A442: p1 = |[(p1 `1 ), (p1 `2 )]| & p2 = |[(p2 `1 ), (p2 `2 )]| by EUCLID: 53;

                    m < (m + 1) by NAT_1: 13;

                    then

                     A443: (q1 `2 ) < (q2 `2 ) by A424, A437, A438;

                    

                     A444: q1 = |[(q1 `1 ), (q1 `2 )]| & q2 = |[(q2 `1 ), (q2 `2 )]| by EUCLID: 53;

                    set x = the Element of (( LSeg (g2,n)) /\ ( LSeg (g2,m)));

                    

                     A445: x in ( LSeg (g2,n)) by A439, XBOOLE_0:def 4;

                    

                     A446: (q1 `1 ) = (ppi `1 ) & (q2 `1 ) = (ppi `1 ) by A406, A437, A438;

                    

                     A447: x in ( LSeg (g2,m)) by A439, XBOOLE_0:def 4;

                    1 <= m & (m + 1) <= ( len g2) by A437, A438, FINSEQ_3: 25;

                    

                    then ( LSeg (g2,m)) = ( LSeg (q1,q2)) by TOPREAL1:def 3

                    .= lq by A443, A446, A444, TOPREAL3: 9;

                    then

                     A448: ex tm be Point of ( TOP-REAL 2) st tm = x & (tm `1 ) = (ppi `1 ) & (q1 `2 ) <= (tm `2 ) & (tm `2 ) <= (q2 `2 ) by A447;

                    1 <= n & (n + 1) <= ( len g2) by A435, A436, FINSEQ_3: 25;

                    

                    then ( LSeg (g2,n)) = ( LSeg (p1,p2)) by TOPREAL1:def 3

                    .= lp by A441, A440, A442, TOPREAL3: 9;

                    then

                     A449: ex tn be Point of ( TOP-REAL 2) st tn = x & (tn `1 ) = (ppi `1 ) & (p1 `2 ) <= (tn `2 ) & (tn `2 ) <= (p2 `2 ) by A445;

                    (p2 `2 ) < (q1 `2 ) by A424, A434, A436, A437;

                    hence contradiction by A449, A448, XXREAL_0: 2;

                  end;

                  then

                   A450: g2 is s.n.c. by GOBOARD2: 1;

                  

                   A451: not (f /. k) in ( L~ g2)

                  proof

                    set ls = { ( LSeg (g2,m)) : 1 <= m & (m + 1) <= ( len g2) };

                    assume (f /. k) in ( L~ g2);

                    then

                    consider X be set such that

                     A452: (f /. k) in X and

                     A453: X in ls by TARSKI:def 4;

                    consider m such that

                     A454: X = ( LSeg (g2,m)) and

                     A455: 1 <= m & (m + 1) <= ( len g2) by A453;

                    reconsider q1 = (g2 /. m), q2 = (g2 /. (m + 1)) as Point of ( TOP-REAL 2);

                    

                     A456: m in ( dom g2) by A455, SEQ_4: 134;

                    then

                     A457: (q1 `1 ) = (ppi `1 ) by A406;

                    set lq = { w where w be Point of ( TOP-REAL 2) : (w `1 ) = (ppi `1 ) & (q1 `2 ) <= (w `2 ) & (w `2 ) <= (q2 `2 ) };

                    

                     A458: q1 = |[(q1 `1 ), (q1 `2 )]| & q2 = |[(q2 `1 ), (q2 `2 )]| by EUCLID: 53;

                    

                     A459: (m + 1) in ( dom g2) by A455, SEQ_4: 134;

                    then

                     A460: (q2 `1 ) = (ppi `1 ) by A406;

                    m < (m + 1) by NAT_1: 13;

                    then

                     A461: (q1 `2 ) < (q2 `2 ) by A424, A456, A459;

                    ( LSeg (g2,m)) = ( LSeg (q1,q2)) by A455, TOPREAL1:def 3

                    .= lq by A457, A460, A461, A458, TOPREAL3: 9;

                    then ex p st p = (f /. k) & (p `1 ) = (ppi `1 ) & (q1 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 ) by A452, A454;

                    hence contradiction by A29, A406, A456;

                  end;

                  (x1 . j2) = (pj `1 ) by A74, A62, A72, A393, GOBOARD1:def 1;

                  then

                   A462: (ppi `1 ) = (pj `1 ) by A68, A74, A67, A62, A72, A405, SEQM_3:def 10;

                   A463:

                  now

                    let n;

                    assume that

                     A464: n in ( dom g2) and

                     A465: (n + 1) in ( dom g2);

                    let l1,l2,l3,l4 be Nat;

                    assume that

                     A466: [l1, l2] in ( Indices G) and

                     A467: [l3, l4] in ( Indices G) and

                     A468: (g2 /. n) = (G * (l1,l2)) and

                     A469: (g2 /. (n + 1)) = (G * (l3,l4));

                    (g2 /. (n + 1)) = (G * (i1,(i2 + (n + 1)))) & [i1, (i2 + (n + 1))] in ( Indices G) by A396, A398, A397, A465;

                    then

                     A470: l3 = i1 & l4 = (i2 + (n + 1)) by A467, A469, GOBOARD1: 5;

                    (g2 /. n) = (G * (i1,(i2 + n))) & [i1, (i2 + n)] in ( Indices G) by A396, A398, A397, A464;

                    then l1 = i1 & l2 = (i2 + n) by A466, A468, GOBOARD1: 5;

                    

                    hence ( |.(l1 - l3).| + |.(l2 - l4).|) = ( 0 + |.((i2 + n) - (i2 + (n + 1))).|) by A470, ABSVALUE: 2

                    .= |.( - 1).|

                    .= |.1.| by COMPLEX1: 52

                    .= 1 by ABSVALUE:def 1;

                  end;

                  now

                    let l1,l2,l3,l4 be Nat;

                    assume that

                     A471: [l1, l2] in ( Indices G) and

                     A472: [l3, l4] in ( Indices G) and

                     A473: (g1 /. ( len g1)) = (G * (l1,l2)) and

                     A474: (g2 /. 1) = (G * (l3,l4)) and ( len g1) in ( dom g1) and

                     A475: 1 in ( dom g2);

                    (g2 /. 1) = (G * (i1,(i2 + 1))) & [i1, (i2 + 1)] in ( Indices G) by A396, A398, A397, A475;

                    then

                     A476: l3 = i1 & l4 = (i2 + 1) by A472, A474, GOBOARD1: 5;

                    (f1 /. ( len f1)) = (f /. k) by A27, A14, A51, FINSEQ_4: 71;

                    then l1 = i1 & l2 = i2 by A46, A28, A29, A471, A473, GOBOARD1: 5;

                    

                    hence ( |.(l1 - l3).| + |.(l2 - l4).|) = ( 0 + |.(i2 - (i2 + 1)).|) by A476, ABSVALUE: 2

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

                    .= |.1.| by COMPLEX1: 52

                    .= 1 by ABSVALUE:def 1;

                  end;

                  then for n st n in ( dom g) & (n + 1) in ( dom g) holds for m, k, i, j st [m, k] in ( Indices G) & [i, j] in ( Indices G) & (g /. n) = (G * (m,k)) & (g /. (n + 1)) = (G * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1 by A48, A463, GOBOARD1: 24;

                  hence g is_sequence_on G by A404, GOBOARD1:def 9;

                  

                   A477: pj = |[(pj `1 ), (pj `2 )]| by EUCLID: 53;

                  

                   A478: ( LSeg (f,k)) = ( LSeg (ppi,pj)) by A3, A24, A29, A21, A76, TOPREAL1:def 3

                  .= lk by A395, A462, A423, A477, TOPREAL3: 9;

                  

                   A479: ( rng g2) c= ( LSeg (f,k))

                  proof

                    let x be object;

                    assume x in ( rng g2);

                    then

                    consider n be Element of NAT such that

                     A480: n in ( dom g2) and

                     A481: (g2 /. n) = x by PARTFUN2: 2;

                    set pn = (G * (i1,(i2 + n)));

                    

                     A482: (g2 /. n) = (G * (i1,(i2 + n))) by A396, A480;

                    then

                     A483: (pn `2 ) <= (pj `2 ) by A406, A480;

                    (pn `1 ) = (ppi `1 ) & (ppi `2 ) <= (pn `2 ) by A406, A480, A482;

                    hence thesis by A478, A481, A482, A483;

                  end;

                  

                   A484: not (f /. k) in ( rng g2)

                  proof

                    assume (f /. k) in ( rng g2);

                    then

                    consider n be Element of NAT such that

                     A485: n in ( dom g2) and

                     A486: (g2 /. n) = (f /. k) by PARTFUN2: 2;

                    

                     A487: 0 < n by A485, FINSEQ_3: 25;

                    

                     A488: (g2 /. n) = (G * (i1,(i2 + n))) by A396, A485;

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

                    then [i1, (i2 + n)] in ( Indices G) by A396, A398, A485;

                    then (i2 + n) = i2 by A28, A29, A486, A488, GOBOARD1: 5;

                    hence contradiction by A487;

                  end;

                  (( rng g1) /\ ( rng g2)) = {}

                  proof

                    set x = the Element of (( rng g1) /\ ( rng g2));

                    assume

                     A489: not thesis;

                    then

                     A490: x in ( rng g2) by XBOOLE_0:def 4;

                    

                     A491: x in ( rng g1) by A489, XBOOLE_0:def 4;

                    now

                      per cases by A24, XXREAL_0: 1;

                        suppose k = 1;

                        hence contradiction by A52, A484, A491, A490, TARSKI:def 1;

                      end;

                        suppose 1 < k;

                        then x in (( L~ f1) /\ ( LSeg (f,k))) & (( L~ f1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, A49, A479, A491, A490, GOBOARD2: 4, XBOOLE_0:def 4;

                        hence contradiction by A484, A490, TARSKI:def 1;

                      end;

                    end;

                    hence contradiction;

                  end;

                  then ( rng g1) misses ( rng g2);

                  hence g is one-to-one by A40, A422, FINSEQ_3: 91;

                  

                   A492: ( LSeg (f,k)) = ( LSeg (ppi,pj)) by A3, A24, A29, A21, A76, TOPREAL1:def 3;

                  

                   A493: for n st 1 <= n & (n + 2) <= ( len g2) holds (( LSeg (g2,n)) /\ ( LSeg (g2,(n + 1)))) = {(g2 /. (n + 1))}

                  proof

                    let n;

                    assume that

                     A494: 1 <= n and

                     A495: (n + 2) <= ( len g2);

                    

                     A496: (n + 1) in ( dom g2) by A494, A495, SEQ_4: 135;

                    then (g2 /. (n + 1)) in ( rng g2) by PARTFUN2: 2;

                    then (g2 /. (n + 1)) in lk by A478, A479;

                    then

                    consider u1 be Point of ( TOP-REAL 2) such that

                     A497: (g2 /. (n + 1)) = u1 and

                     A498: (u1 `1 ) = (ppi `1 ) and (ppi `2 ) <= (u1 `2 ) and (u1 `2 ) <= (pj `2 );

                    

                     A499: (n + 2) in ( dom g2) by A494, A495, SEQ_4: 135;

                    then (g2 /. (n + 2)) in ( rng g2) by PARTFUN2: 2;

                    then (g2 /. (n + 2)) in lk by A478, A479;

                    then

                    consider u2 be Point of ( TOP-REAL 2) such that

                     A500: (g2 /. (n + 2)) = u2 and

                     A501: (u2 `1 ) = (ppi `1 ) and (ppi `2 ) <= (u2 `2 ) and (u2 `2 ) <= (pj `2 );

                    1 <= (n + 1) & ((n + 1) + 1) = (n + (1 + 1)) by NAT_1: 11;

                    then

                     A502: ( LSeg (g2,(n + 1))) = ( LSeg (u1,u2)) by A495, A497, A500, TOPREAL1:def 3;

                    (n + 1) < ((n + 1) + 1) by NAT_1: 13;

                    then

                     A503: (u1 `2 ) < (u2 `2 ) by A424, A496, A499, A497, A500;

                    

                     A504: n in ( dom g2) by A494, A495, SEQ_4: 135;

                    then (g2 /. n) in ( rng g2) by PARTFUN2: 2;

                    then (g2 /. n) in lk by A478, A479;

                    then

                    consider u be Point of ( TOP-REAL 2) such that

                     A505: (g2 /. n) = u and

                     A506: (u `1 ) = (ppi `1 ) and (ppi `2 ) <= (u `2 ) and (u `2 ) <= (pj `2 );

                    (n + 1) <= (n + 2) by XREAL_1: 6;

                    then (n + 1) <= ( len g2) by A495, XXREAL_0: 2;

                    then

                     A507: ( LSeg (g2,n)) = ( LSeg (u,u1)) by A494, A505, A497, TOPREAL1:def 3;

                    set lg = { w where w be Point of ( TOP-REAL 2) : (w `1 ) = (ppi `1 ) & (u `2 ) <= (w `2 ) & (w `2 ) <= (u2 `2 ) };

                    n < (n + 1) by NAT_1: 13;

                    then

                     A508: (u `2 ) < (u1 `2 ) by A424, A504, A496, A505, A497;

                    then

                     A509: u1 in lg by A498, A503;

                    u = |[(u `1 ), (u `2 )]| & u2 = |[(u2 `1 ), (u2 `2 )]| by EUCLID: 53;

                    then ( LSeg ((g2 /. n),(g2 /. (n + 2)))) = lg by A505, A506, A500, A501, A503, A508, TOPREAL3: 9, XXREAL_0: 2;

                    hence thesis by A505, A497, A500, A507, A502, A509, TOPREAL1: 8;

                  end;

                  thus g is unfolded

                  proof

                    let n be Nat;

                    assume that

                     A510: 1 <= n and

                     A511: (n + 2) <= ( len g);

                    

                     A512: ((n + 1) + 1) <= ( len g) by A511;

                    (n + 1) <= ((n + 1) + 1) by NAT_1: 11;

                    then

                     A513: (n + 1) <= ( len g) by A511, XXREAL_0: 2;

                    

                     A514: ( len g) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

                    ((n + 2) - ( len g1)) = ((n - ( len g1)) + 2);

                    then

                     A515: ((n - ( len g1)) + 2) <= ( len g2) by A511, A514, XREAL_1: 20;

                    

                     A516: 1 <= (n + 1) by NAT_1: 11;

                    

                     A517: n <= (n + 1) by NAT_1: 11;

                    

                     A518: (n + (1 + 1)) = ((n + 1) + 1);

                    per cases ;

                      suppose

                       A519: (n + 2) <= ( len g1);

                      

                       A520: (n + (1 + 1)) = ((n + 1) + 1);

                      

                       A521: (n + 1) in ( dom g1) by A510, A519, SEQ_4: 135;

                      then

                       A522: (g /. (n + 1)) = (g1 /. (n + 1)) by FINSEQ_4: 68;

                      n in ( dom g1) by A510, A519, SEQ_4: 135;

                      then

                       A523: ( LSeg (g1,n)) = ( LSeg (g,n)) by A521, TOPREAL3: 18;

                      (n + 2) in ( dom g1) by A510, A519, SEQ_4: 135;

                      then ( LSeg (g1,(n + 1))) = ( LSeg (g,(n + 1))) by A521, A520, TOPREAL3: 18;

                      hence thesis by A41, A510, A519, A523, A522;

                    end;

                      suppose ( len g1) < (n + 2);

                      then (( len g1) + 1) <= (n + 2) by NAT_1: 13;

                      then

                       A524: ( len g1) <= ((n + 2) - 1) by XREAL_1: 19;

                      now

                        per cases ;

                          suppose

                           A525: ( len g1) = (n + 1);

                          now

                            1 < ( len g1) by A510, A525, NAT_1: 13;

                            then

                             A526: (1 + 1) <= ( len g1) by NAT_1: 13;

                            assume k = 1;

                            hence contradiction by A52, A526, TOPREAL1: 23;

                          end;

                          then 1 < k by A24, XXREAL_0: 1;

                          then

                           A527: (( L~ f1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, GOBOARD2: 4;

                          (g /. (n + 1)) in ( LSeg (g,n)) & (g /. (n + 1)) in ( LSeg (g,(n + 1))) by A510, A511, A516, A513, A518, TOPREAL1: 21;

                          then (g /. (n + 1)) in (( LSeg (g,n)) /\ ( LSeg (g,(n + 1)))) by XBOOLE_0:def 4;

                          then

                           A528: {(g /. (n + 1))} c= (( LSeg (g,n)) /\ ( LSeg (g,(n + 1)))) by ZFMISC_1: 31;

                          

                           A529: 1 <= (( len g) - ( len g1)) by A512, A525, XREAL_1: 19;

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

                          then

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

                          then (g2 /. 1) in lk by A478, A479;

                          then

                          consider u1 be Point of ( TOP-REAL 2) such that

                           A531: (g2 /. 1) = u1 and (u1 `1 ) = (ppi `1 ) and (ppi `2 ) <= (u1 `2 ) and (u1 `2 ) <= (pj `2 );

                          ppi in ( LSeg (ppi,pj)) by RLTOPSP1: 68;

                          then

                           A532: ( LSeg (ppi,u1)) c= ( LSeg (f,k)) by A492, A479, A530, A531, TOPREAL1: 6;

                          1 <= (n + 1) by NAT_1: 11;

                          then

                           A533: (n + 1) in ( dom g1) by A525, FINSEQ_3: 25;

                          

                          then

                           A534: (g /. (n + 1)) = (f1 /. ( len f1)) by A46, A525, FINSEQ_4: 68

                          .= ppi by A27, A14, A51, A29, FINSEQ_4: 71;

                          n in ( dom g1) by A510, A517, A525, FINSEQ_3: 25;

                          then

                           A535: ( LSeg (g,n)) = ( LSeg (g1,n)) by A533, TOPREAL3: 18;

                          (g /. (n + 2)) = (g2 /. 1) by A518, A514, A525, A529, SEQ_4: 136;

                          then

                           A536: ( LSeg (g,(n + 1))) = ( LSeg (ppi,u1)) by A511, A516, A518, A534, A531, TOPREAL1:def 3;

                          ( LSeg (g1,n)) c= ( L~ f1) by A44, TOPREAL3: 19;

                          then (( LSeg (g,n)) /\ ( LSeg (g,(n + 1)))) c= {(g /. (n + 1))} by A29, A527, A535, A534, A532, A536, XBOOLE_1: 27;

                          hence thesis by A528;

                        end;

                          suppose ( len g1) <> (n + 1);

                          then ( len g1) < (n + 1) by A524, XXREAL_0: 1;

                          then

                           A537: ( len g1) <= n by NAT_1: 13;

                          then

                          reconsider n1 = (n - ( len g1)) as Element of NAT by INT_1: 5;

                          now

                            per cases ;

                              suppose

                               A538: ( len g1) = n;

                              then

                               A539: 2 <= ( len g2) by A511, A514, XREAL_1: 6;

                              then 1 <= ( len g2) by XXREAL_0: 2;

                              then

                               A540: (g /. (n + 1)) = (g2 /. 1) by A538, SEQ_4: 136;

                              1 <= ( len g2) by A539, XXREAL_0: 2;

                              then

                               A541: 1 in ( dom g2) by FINSEQ_3: 25;

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

                              then (g2 /. 1) in lk by A478, A479;

                              then

                              consider u1 be Point of ( TOP-REAL 2) such that

                               A542: (g2 /. 1) = u1 and

                               A543: (u1 `1 ) = (ppi `1 ) & (ppi `2 ) <= (u1 `2 ) and (u1 `2 ) <= (pj `2 );

                              1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                              then ( len g1) in ( dom g1) by FINSEQ_3: 25;

                              

                              then (g /. n) = (f1 /. ( len f1)) by A46, A538, FINSEQ_4: 68

                              .= ppi by A27, A14, A51, A29, FINSEQ_4: 71;

                              then

                               A544: ( LSeg (g,n)) = ( LSeg (ppi,u1)) by A510, A513, A540, A542, TOPREAL1:def 3;

                              

                               A545: 2 in ( dom g2) by A539, FINSEQ_3: 25;

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

                              then (g2 /. 2) in lk by A478, A479;

                              then

                              consider u2 be Point of ( TOP-REAL 2) such that

                               A546: (g2 /. 2) = u2 and

                               A547: (u2 `1 ) = (ppi `1 ) & (ppi `2 ) <= (u2 `2 ) and (u2 `2 ) <= (pj `2 );

                              set lg = { w where w be Point of ( TOP-REAL 2) : (w `1 ) = (ppi `1 ) & (ppi `2 ) <= (w `2 ) & (w `2 ) <= (u2 `2 ) };

                              (u1 `2 ) < (u2 `2 ) by A424, A541, A545, A542, A546;

                              then u2 = |[(u2 `1 ), (u2 `2 )]| & u1 in lg by A543, EUCLID: 53;

                              then

                               A548: u1 in ( LSeg (ppi,u2)) by A423, A547, TOPREAL3: 9;

                              (g /. (n + 2)) = (g2 /. 2) by A538, A539, SEQ_4: 136;

                              then ( LSeg (g,(n + 1))) = ( LSeg (u1,u2)) by A511, A516, A518, A540, A542, A546, TOPREAL1:def 3;

                              hence thesis by A540, A542, A544, A548, TOPREAL1: 8;

                            end;

                              suppose ( len g1) <> n;

                              then

                               A549: ( len g1) < n by A537, XXREAL_0: 1;

                              then (( len g1) + 1) <= n by NAT_1: 13;

                              then

                               A550: 1 <= n1 by XREAL_1: 19;

                              (n1 + ( len g1)) = n;

                              then

                               A551: ( LSeg (g,n)) = ( LSeg (g2,n1)) by A513, A549, GOBOARD2: 5;

                              

                               A552: ((n1 + 1) + ( len g1)) = (n + 1);

                              then (n1 + 1) <= ( len g2) by A513, A514, XREAL_1: 6;

                              then

                               A553: (g /. (n + 1)) = (g2 /. (n1 + 1)) by A552, NAT_1: 11, SEQ_4: 136;

                              ( len g1) < (n + 1) by A517, A549, XXREAL_0: 2;

                              then ( LSeg (g,(n + 1))) = ( LSeg (g2,(n1 + 1))) by A512, A552, GOBOARD2: 5;

                              hence thesis by A493, A515, A551, A553, A550;

                            end;

                          end;

                          hence thesis;

                        end;

                      end;

                      hence thesis;

                    end;

                  end;

                  

                   A554: ( L~ g2) c= ( LSeg (f,k))

                  proof

                    let x be object;

                    set ls = { ( LSeg (g2,m)) : 1 <= m & (m + 1) <= ( len g2) };

                    assume x in ( L~ g2);

                    then

                    consider X be set such that

                     A555: x in X and

                     A556: X in ls by TARSKI:def 4;

                    consider m such that

                     A557: X = ( LSeg (g2,m)) and

                     A558: 1 <= m & (m + 1) <= ( len g2) by A556;

                    reconsider q1 = (g2 /. m), q2 = (g2 /. (m + 1)) as Point of ( TOP-REAL 2);

                    

                     A559: ( LSeg (g2,m)) = ( LSeg (q1,q2)) by A558, TOPREAL1:def 3;

                    (m + 1) in ( dom g2) by A558, SEQ_4: 134;

                    then

                     A560: (g2 /. (m + 1)) in ( rng g2) by PARTFUN2: 2;

                    m in ( dom g2) by A558, SEQ_4: 134;

                    then (g2 /. m) in ( rng g2) by PARTFUN2: 2;

                    then ( LSeg (q1,q2)) c= ( LSeg (ppi,pj)) by A492, A479, A560, TOPREAL1: 6;

                    hence thesis by A492, A555, A557, A559;

                  end;

                  

                   A561: (( L~ g1) /\ ( L~ g2)) = {}

                  proof

                    per cases ;

                      suppose k = 1;

                      hence thesis by A52;

                    end;

                      suppose k <> 1;

                      then 1 < k by A24, XXREAL_0: 1;

                      then (( L~ g1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, A44, GOBOARD2: 4;

                      then

                       A562: (( L~ g1) /\ ( L~ g2)) c= {(f /. k)} by A554, XBOOLE_1: 26;

                      now

                        set x = the Element of (( L~ g1) /\ ( L~ g2));

                        assume (( L~ g1) /\ ( L~ g2)) <> {} ;

                        then x in {(f /. k)} & x in ( L~ g2) by A562, XBOOLE_0:def 4;

                        hence contradiction by A451, TARSKI:def 1;

                      end;

                      hence thesis;

                    end;

                  end;

                  for n, m st m > (n + 1) & n in ( dom g) & (n + 1) in ( dom g) & m in ( dom g) & (m + 1) in ( dom g) holds ( LSeg (g,n)) misses ( LSeg (g,m))

                  proof

                    

                     A563: 1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                    then ( len g1) in ( dom g1) by FINSEQ_3: 25;

                    

                    then

                     A564: (g /. ( len g1)) = (g1 /. ( len g1)) by FINSEQ_4: 68

                    .= ppi by A27, A14, A51, A46, A29, FINSEQ_4: 71;

                    reconsider qq = (g2 /. 1) as Point of ( TOP-REAL 2);

                    set l1 = { ( LSeg (g1,i)) : 1 <= i & (i + 1) <= ( len g1) }, l2 = { ( LSeg (g2,j)) : 1 <= j & (j + 1) <= ( len g2) };

                    let n, m;

                    assume that

                     A565: m > (n + 1) and

                     A566: n in ( dom g) and

                     A567: (n + 1) in ( dom g) and

                     A568: m in ( dom g) and

                     A569: (m + 1) in ( dom g);

                    

                     A570: 1 <= n by A566, FINSEQ_3: 25;

                    (i2 + 1) <= j2 by A390, NAT_1: 13;

                    then

                     A571: 1 <= l by XREAL_1: 19;

                    then

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

                    then

                     A573: (qq `1 ) = (ppi `1 ) & (qq `2 ) > (ppi `2 ) by A406;

                    

                     A574: (g /. (( len g1) + 1)) = qq by A396, A571, SEQ_4: 136;

                    

                     A575: (qq `2 ) <= (pj `2 ) by A406, A572;

                    

                     A576: (m + 1) <= ( len g) by A569, FINSEQ_3: 25;

                    

                     A577: 1 <= (m + 1) by A569, FINSEQ_3: 25;

                    

                     A578: 1 <= (n + 1) by A567, FINSEQ_3: 25;

                    

                     A579: (n + 1) <= ( len g) by A567, FINSEQ_3: 25;

                    

                     A580: qq = |[(qq `1 ), (qq `2 )]| by EUCLID: 53;

                    

                     A581: 1 <= m by A568, FINSEQ_3: 25;

                    set ql = { z where z be Point of ( TOP-REAL 2) : (z `1 ) = (ppi `1 ) & (ppi `2 ) <= (z `2 ) & (z `2 ) <= (qq `2 ) };

                    

                     A582: n <= (n + 1) by NAT_1: 11;

                    

                     A583: ( len g) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

                    then (( len g1) + 1) <= ( len g) by A396, A571, XREAL_1: 7;

                    

                    then

                     A584: ( LSeg (g,( len g1))) = ( LSeg (ppi,qq)) by A563, A564, A574, TOPREAL1:def 3

                    .= ql by A423, A573, A580, TOPREAL3: 9;

                    

                     A585: m <= (m + 1) by NAT_1: 11;

                    then

                     A586: (n + 1) <= (m + 1) by A565, XXREAL_0: 2;

                    now

                      per cases ;

                        suppose

                         A587: (m + 1) <= ( len g1);

                        then m <= ( len g1) by A585, XXREAL_0: 2;

                        then

                         A588: m in ( dom g1) by A581, FINSEQ_3: 25;

                        (m + 1) in ( dom g1) by A577, A587, FINSEQ_3: 25;

                        then

                         A589: ( LSeg (g,m)) = ( LSeg (g1,m)) by A588, TOPREAL3: 18;

                        

                         A590: (n + 1) <= ( len g1) by A586, A587, XXREAL_0: 2;

                        then n <= ( len g1) by A582, XXREAL_0: 2;

                        then

                         A591: n in ( dom g1) by A570, FINSEQ_3: 25;

                        (n + 1) in ( dom g1) by A578, A590, FINSEQ_3: 25;

                        then ( LSeg (g,n)) = ( LSeg (g1,n)) by A591, TOPREAL3: 18;

                        hence thesis by A42, A565, A589;

                      end;

                        suppose ( len g1) < (m + 1);

                        then

                         A592: ( len g1) <= m by NAT_1: 13;

                        then

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

                        now

                          per cases ;

                            suppose

                             A593: m = ( len g1);

                            

                             A594: ( LSeg (g,m)) c= ( LSeg (f,k))

                            proof

                              let x be object;

                              assume x in ( LSeg (g,m));

                              then

                              consider px be Point of ( TOP-REAL 2) such that

                               A595: px = x & (px `1 ) = (ppi `1 ) & (ppi `2 ) <= (px `2 ) and

                               A596: (px `2 ) <= (qq `2 ) by A584, A593;

                              (pj `2 ) >= (px `2 ) by A575, A596, XXREAL_0: 2;

                              hence thesis by A478, A595;

                            end;

                            n <= ( len g1) by A565, A582, A593, XXREAL_0: 2;

                            then

                             A597: n in ( dom g1) by A570, FINSEQ_3: 25;

                            now

                              1 < ( len g1) by A565, A578, A593, XXREAL_0: 2;

                              then

                               A598: (1 + 1) <= ( len g1) by NAT_1: 13;

                              assume k = 1;

                              hence contradiction by A52, A598, TOPREAL1: 23;

                            end;

                            then 1 < k by A24, XXREAL_0: 1;

                            then

                             A599: (( L~ f1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, GOBOARD2: 4;

                            

                             A600: (n + 1) in ( dom g1) by A565, A578, A593, FINSEQ_3: 25;

                            then

                             A601: ( LSeg (g,n)) = ( LSeg (g1,n)) by A597, TOPREAL3: 18;

                            then ( LSeg (g,n)) in l1 by A565, A570, A593;

                            then ( LSeg (g,n)) c= ( L~ f1) by A44, ZFMISC_1: 74;

                            then

                             A602: (( LSeg (g,n)) /\ ( LSeg (g,m))) c= {(f /. k)} by A599, A594, XBOOLE_1: 27;

                            now

                              set x = the Element of (( LSeg (g,n)) /\ ( LSeg (g,m)));

                              assume

                               A603: (( LSeg (g,n)) /\ ( LSeg (g,m))) <> {} ;

                              then

                               A604: x in ( LSeg (g,n)) by XBOOLE_0:def 4;

                              x in {(f /. k)} by A602, A603;

                              then

                               A605: x = (f /. k) by TARSKI:def 1;

                              (f /. k) = (g1 /. ( len g1)) by A27, A14, A51, A46, FINSEQ_4: 71;

                              hence contradiction by A40, A41, A42, A565, A593, A597, A600, A601, A604, A605, GOBOARD2: 2;

                            end;

                            hence thesis;

                          end;

                            suppose m <> ( len g1);

                            then

                             A606: ( len g1) < m by A592, XXREAL_0: 1;

                            then (( len g1) + 1) <= m by NAT_1: 13;

                            then

                             A607: 1 <= m1 by XREAL_1: 19;

                            (m + 1) = ((m1 + 1) + ( len g1));

                            then

                             A608: (m1 + 1) <= ( len g2) by A576, A583, XREAL_1: 6;

                            m = (m1 + ( len g1));

                            then

                             A609: ( LSeg (g,m)) = ( LSeg (g2,m1)) by A576, A606, GOBOARD2: 5;

                            then ( LSeg (g,m)) in l2 by A607, A608;

                            then

                             A610: ( LSeg (g,m)) c= ( L~ g2) by ZFMISC_1: 74;

                            now

                              per cases ;

                                suppose

                                 A611: (n + 1) <= ( len g1);

                                then n <= ( len g1) by A582, XXREAL_0: 2;

                                then

                                 A612: n in ( dom g1) by A570, FINSEQ_3: 25;

                                (n + 1) in ( dom g1) by A578, A611, FINSEQ_3: 25;

                                then ( LSeg (g,n)) = ( LSeg (g1,n)) by A612, TOPREAL3: 18;

                                then ( LSeg (g,n)) in l1 by A570, A611;

                                then ( LSeg (g,n)) c= ( L~ g1) by ZFMISC_1: 74;

                                then (( LSeg (g,n)) /\ ( LSeg (g,m))) = {} by A561, A610, XBOOLE_1: 3, XBOOLE_1: 27;

                                hence thesis;

                              end;

                                suppose ( len g1) < (n + 1);

                                then

                                 A613: ( len g1) <= n by NAT_1: 13;

                                then

                                reconsider n1 = (n - ( len g1)) as Element of NAT by INT_1: 5;

                                

                                 A614: ((n - ( len g1)) + 1) = ((n + 1) - ( len g1));

                                

                                 A615: n = (n1 + ( len g1));

                                now

                                  per cases ;

                                    suppose

                                     A616: ( len g1) = n;

                                    now

                                      reconsider q1 = (g2 /. m1), q2 = (g2 /. (m1 + 1)) as Point of ( TOP-REAL 2);

                                      set x = the Element of (( LSeg (g,n)) /\ ( LSeg (g,m)));

                                      set q1l = { v where v be Point of ( TOP-REAL 2) : (v `1 ) = (ppi `1 ) & (q1 `2 ) <= (v `2 ) & (v `2 ) <= (q2 `2 ) };

                                      

                                       A617: q1 = |[(q1 `1 ), (q1 `2 )]| & q2 = |[(q2 `1 ), (q2 `2 )]| by EUCLID: 53;

                                      assume

                                       A618: (( LSeg (g,n)) /\ ( LSeg (g,m))) <> {} ;

                                      then

                                       A619: x in ( LSeg (g,m)) by XBOOLE_0:def 4;

                                      x in ( LSeg (g,n)) by A618, XBOOLE_0:def 4;

                                      then

                                       A620: ex qx be Point of ( TOP-REAL 2) st qx = x & (qx `1 ) = (ppi `1 ) & (ppi `2 ) <= (qx `2 ) & (qx `2 ) <= (qq `2 ) by A584, A616;

                                      

                                       A621: m1 in ( dom g2) by A607, A608, SEQ_4: 134;

                                      then

                                       A622: (q1 `1 ) = (ppi `1 ) by A406;

                                      

                                       A623: (m1 + 1) in ( dom g2) by A607, A608, SEQ_4: 134;

                                      then

                                       A624: (q2 `1 ) = (ppi `1 ) by A406;

                                      m1 < (m1 + 1) by NAT_1: 13;

                                      then

                                       A625: (q1 `2 ) < (q2 `2 ) by A424, A621, A623;

                                      ( LSeg (g2,m1)) = ( LSeg (q1,q2)) by A607, A608, TOPREAL1:def 3

                                      .= q1l by A622, A624, A625, A617, TOPREAL3: 9;

                                      then

                                       A626: ex qy be Point of ( TOP-REAL 2) st qy = x & (qy `1 ) = (ppi `1 ) & (q1 `2 ) <= (qy `2 ) & (qy `2 ) <= (q2 `2 ) by A609, A619;

                                      m1 > (n1 + 1) & (n1 + 1) >= 1 by A565, A614, NAT_1: 11, XREAL_1: 9;

                                      then m1 > 1 by XXREAL_0: 2;

                                      then (qq `2 ) < (q1 `2 ) by A424, A572, A621;

                                      hence contradiction by A620, A626, XXREAL_0: 2;

                                    end;

                                    hence thesis;

                                  end;

                                    suppose n <> ( len g1);

                                    then ( len g1) < n by A613, XXREAL_0: 1;

                                    then

                                     A627: ( LSeg (g,n)) = ( LSeg (g2,n1)) by A579, A615, GOBOARD2: 5;

                                    m1 > (n1 + 1) by A565, A614, XREAL_1: 9;

                                    hence thesis by A450, A609, A627;

                                  end;

                                end;

                                hence thesis;

                              end;

                            end;

                            hence thesis;

                          end;

                        end;

                        hence thesis;

                      end;

                    end;

                    hence thesis;

                  end;

                  hence g is s.n.c. by GOBOARD2: 1;

                  now

                    set p = (g1 /. ( len g1)), q = (g2 /. 1);

                    (i2 + 1) <= j2 by A390, NAT_1: 13;

                    then 1 <= l by XREAL_1: 19;

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

                    then (q `1 ) = (ppi `1 ) by A406;

                    hence (p `1 ) = (q `1 ) or (p `2 ) = (q `2 ) by A27, A14, A51, A46, A29, FINSEQ_4: 71;

                  end;

                  hence g is special by A43, A415, GOBOARD2: 8;

                  thus ( L~ g) = ( L~ f)

                  proof

                    set lg = { ( LSeg (g,i)) : 1 <= i & (i + 1) <= ( len g) }, lf = { ( LSeg (f,j)) : 1 <= j & (j + 1) <= ( len f) };

                    

                     A628: ( len g) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

                     A629:

                    now

                      let j;

                      assume that

                       A630: ( len g1) <= j and

                       A631: j <= ( len g);

                      reconsider w = (j - ( len g1)) as Element of NAT by A630, INT_1: 5;

                      let p such that

                       A632: p = (g /. j);

                      per cases ;

                        suppose

                         A633: j = ( len g1);

                        1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                        then ( len g1) in ( dom g1) by FINSEQ_3: 25;

                        

                        then

                         A634: (g /. ( len g1)) = (f1 /. ( len f1)) by A46, FINSEQ_4: 68

                        .= (G * (i1,i2)) by A27, A14, A51, A29, FINSEQ_4: 71;

                        hence (p `1 ) = ((G * (i1,i2)) `1 ) by A632, A633;

                        thus ((G * (i1,i2)) `2 ) <= (p `2 ) & (p `2 ) <= ((G * (i1,j2)) `2 ) by A68, A74, A71, A30, A72, A390, A392, A394, A632, A633, A634, SEQM_3:def 1;

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

                        hence p in ( rng l1) by A68, A72, A391, A632, A633, A634, PARTFUN2: 2;

                      end;

                        suppose j <> ( len g1);

                        then ( len g1) < j by A630, XXREAL_0: 1;

                        then (( len g1) + 1) <= j by NAT_1: 13;

                        then

                         A635: 1 <= w by XREAL_1: 19;

                        

                         A636: w <= ( len g2) by A628, A631, XREAL_1: 20;

                        then

                         A637: w in ( dom g2) by A635, FINSEQ_3: 25;

                        j = (w + ( len g1));

                        then (g /. j) = (g2 /. w) by A635, A636, SEQ_4: 136;

                        hence (p `1 ) = (ppi `1 ) & (ppi `2 ) <= (p `2 ) & (p `2 ) <= (pj `2 ) & p in ( rng l1) by A406, A632, A637;

                      end;

                    end;

                    thus ( L~ g) c= ( L~ f)

                    proof

                      let x be object;

                      assume x in ( L~ g);

                      then

                      consider X be set such that

                       A638: x in X and

                       A639: X in lg by TARSKI:def 4;

                      consider i such that

                       A640: X = ( LSeg (g,i)) and

                       A641: 1 <= i and

                       A642: (i + 1) <= ( len g) by A639;

                      per cases ;

                        suppose

                         A643: (i + 1) <= ( len g1);

                        i <= (i + 1) by NAT_1: 11;

                        then i <= ( len g1) by A643, XXREAL_0: 2;

                        then

                         A644: i in ( dom g1) by A641, FINSEQ_3: 25;

                        1 <= (i + 1) by NAT_1: 11;

                        then (i + 1) in ( dom g1) by A643, FINSEQ_3: 25;

                        then X = ( LSeg (g1,i)) by A640, A644, TOPREAL3: 18;

                        then X in { ( LSeg (g1,j)) : 1 <= j & (j + 1) <= ( len g1) } by A641, A643;

                        then

                         A645: x in ( L~ f1) by A44, A638, TARSKI:def 4;

                        ( L~ f1) c= ( L~ f) by TOPREAL3: 20;

                        hence thesis by A645;

                      end;

                        suppose

                         A646: (i + 1) > ( len g1);

                        reconsider q1 = (g /. i), q2 = (g /. (i + 1)) as Point of ( TOP-REAL 2);

                        

                         A647: i <= ( len g) by A642, NAT_1: 13;

                        

                         A648: ( len g1) <= i by A646, NAT_1: 13;

                        then

                         A649: (q1 `1 ) = (ppi `1 ) by A629, A647;

                        

                         A650: (q1 `2 ) <= (pj `2 ) by A629, A648, A647;

                        

                         A651: (ppi `2 ) <= (q1 `2 ) by A629, A648, A647;

                        (q2 `1 ) = (ppi `1 ) by A629, A642, A646;

                        then

                         A652: q2 = |[(q1 `1 ), (q2 `2 )]| by A649, EUCLID: 53;

                        

                         A653: (q2 `2 ) <= (pj `2 ) by A629, A642, A646;

                        

                         A654: q1 = |[(q1 `1 ), (q1 `2 )]| & ( LSeg (g,i)) = ( LSeg (q2,q1)) by A641, A642, EUCLID: 53, TOPREAL1:def 3;

                        

                         A655: (ppi `2 ) <= (q2 `2 ) by A629, A642, A646;

                        now

                          per cases by XXREAL_0: 1;

                            suppose (q1 `2 ) > (q2 `2 );

                            then ( LSeg (g,i)) = { p2 : (p2 `1 ) = (q1 `1 ) & (q2 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q1 `2 ) } by A652, A654, TOPREAL3: 9;

                            then

                            consider p2 such that

                             A656: p2 = x & (p2 `1 ) = (q1 `1 ) and

                             A657: (q2 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q1 `2 ) by A638, A640;

                            (ppi `2 ) <= (p2 `2 ) & (p2 `2 ) <= (pj `2 ) by A650, A655, A657, XXREAL_0: 2;

                            then

                             A658: x in ( LSeg (f,k)) by A478, A649, A656;

                            ( LSeg (f,k)) in lf by A3, A24;

                            hence thesis by A658, TARSKI:def 4;

                          end;

                            suppose (q1 `2 ) = (q2 `2 );

                            then ( LSeg (g,i)) = {q1} by A652, A654, RLTOPSP1: 70;

                            then x = q1 by A638, A640, TARSKI:def 1;

                            then

                             A659: x in ( LSeg (f,k)) by A478, A649, A651, A650;

                            ( LSeg (f,k)) in lf by A3, A24;

                            hence thesis by A659, TARSKI:def 4;

                          end;

                            suppose (q1 `2 ) < (q2 `2 );

                            then ( LSeg (g,i)) = { p1 : (p1 `1 ) = (q1 `1 ) & (q1 `2 ) <= (p1 `2 ) & (p1 `2 ) <= (q2 `2 ) } by A652, A654, TOPREAL3: 9;

                            then

                            consider p2 such that

                             A660: p2 = x & (p2 `1 ) = (q1 `1 ) and

                             A661: (q1 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q2 `2 ) by A638, A640;

                            (ppi `2 ) <= (p2 `2 ) & (p2 `2 ) <= (pj `2 ) by A651, A653, A661, XXREAL_0: 2;

                            then

                             A662: x in ( LSeg (f,k)) by A478, A649, A660;

                            ( LSeg (f,k)) in lf by A3, A24;

                            hence thesis by A662, TARSKI:def 4;

                          end;

                        end;

                        hence thesis;

                      end;

                    end;

                    let x be object;

                    assume x in ( L~ f);

                    then

                     A663: x in (( L~ f1) \/ ( LSeg (f,k))) by A3, A13, GOBOARD2: 3;

                    now

                      per cases by A663, XBOOLE_0:def 3;

                        suppose

                         A664: x in ( L~ f1);

                        ( L~ g1) c= ( L~ g) by GOBOARD2: 6;

                        hence thesis by A44, A664;

                      end;

                        suppose x in ( LSeg (f,k));

                        then

                        consider p1 such that

                         A665: p1 = x and

                         A666: (p1 `1 ) = (ppi `1 ) and

                         A667: (ppi `2 ) <= (p1 `2 ) and

                         A668: (p1 `2 ) <= (pj `2 ) by A478;

                        defpred P2[ Nat] means ( len g1) <= $1 & $1 <= ( len g) & for q st q = (g /. $1) holds (q `2 ) <= (p1 `2 );

                         A669:

                        now

                          reconsider n = ( len g1) as Nat;

                          take n;

                          thus P2[n]

                          proof

                            thus ( len g1) <= n & n <= ( len g) by A628, XREAL_1: 31;

                            1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                            then

                             A670: ( len g1) in ( dom g1) by FINSEQ_3: 25;

                            let q;

                            assume q = (g /. n);

                            

                            then q = (f1 /. ( len f1)) by A46, A670, FINSEQ_4: 68

                            .= (G * (i1,i2)) by A27, A14, A51, A29, FINSEQ_4: 71;

                            hence thesis by A667;

                          end;

                        end;

                        

                         A671: for n be Nat holds P2[n] implies n <= ( len g);

                        consider ma be Nat such that

                         A672: P2[ma] & for n be Nat st P2[n] holds n <= ma from NAT_1:sch 6( A671, A669);

                        reconsider ma as Nat;

                        now

                          per cases ;

                            suppose

                             A673: ma = ( len g);

                            (i2 + 1) <= j2 by A390, NAT_1: 13;

                            then

                             A674: 1 <= l by XREAL_1: 19;

                            then (( len g1) + 1) <= ma by A396, A628, A673, XREAL_1: 7;

                            then

                             A675: ( len g1) <= (ma - 1) by XREAL_1: 19;

                            then ( 0 + 1) <= ma by XREAL_1: 19;

                            then

                            reconsider m1 = (ma - 1) as Element of NAT by INT_1: 5;

                            reconsider q = (g /. m1) as Point of ( TOP-REAL 2);

                            

                             A676: (ma - 1) <= ( len g) by A673, XREAL_1: 43;

                            then

                             A677: (q `1 ) = (ppi `1 ) by A629, A675;

                            

                             A678: (q `2 ) <= (pj `2 ) by A629, A676, A675;

                            set lq = { e where e be Point of ( TOP-REAL 2) : (e `1 ) = (ppi `1 ) & (q `2 ) <= (e `2 ) & (e `2 ) <= (pj `2 ) };

                            

                             A679: (i2 + l) = j2;

                            

                             A680: l in ( dom g2) by A396, A674, FINSEQ_3: 25;

                            

                            then

                             A681: (g /. ma) = (g2 /. l) by A396, A628, A673, FINSEQ_4: 69

                            .= pj by A396, A680, A679;

                            then (pj `2 ) <= (p1 `2 ) by A672;

                            then

                             A682: (p1 `2 ) = (pj `2 ) by A668, XXREAL_0: 1;

                            1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                            then

                             A683: 1 <= m1 by A675, XXREAL_0: 2;

                            

                             A684: (m1 + 1) = ma;

                            then q = |[(q `1 ), (q `2 )]| & ( LSeg (g,m1)) = ( LSeg (q,pj)) by A673, A681, A683, EUCLID: 53, TOPREAL1:def 3;

                            then ( LSeg (g,m1)) = lq by A462, A477, A677, A678, TOPREAL3: 9;

                            then

                             A685: p1 in ( LSeg (g,m1)) by A666, A682, A678;

                            ( LSeg (g,m1)) in lg by A673, A683, A684;

                            hence thesis by A665, A685, TARSKI:def 4;

                          end;

                            suppose ma <> ( len g);

                            then ma < ( len g) by A672, XXREAL_0: 1;

                            then

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

                            reconsider qa = (g /. ma), qa1 = (g /. (ma + 1)) as Point of ( TOP-REAL 2);

                            set lma = { p2 : (p2 `1 ) = (ppi `1 ) & (qa `2 ) <= (p2 `2 ) & (p2 `2 ) <= (qa1 `2 ) };

                            

                             A687: qa1 = |[(qa1 `1 ), (qa1 `2 )]| by EUCLID: 53;

                            

                             A688: (qa `2 ) <= (p1 `2 ) by A672;

                            

                             A689: ( len g1) <= (ma + 1) by A672, NAT_1: 13;

                            then

                             A690: (qa1 `1 ) = (ppi `1 ) by A629, A686;

                             A691:

                            now

                              assume (qa1 `2 ) <= (p1 `2 );

                              then for q holds q = (g /. (ma + 1)) implies (q `2 ) <= (p1 `2 );

                              then (ma + 1) <= ma by A672, A686, A689;

                              hence contradiction by XREAL_1: 29;

                            end;

                            

                             A692: (qa `1 ) = (ppi `1 ) & qa = |[(qa `1 ), (qa `2 )]| by A629, A672, EUCLID: 53;

                            

                             A693: 1 <= ma by A24, A14, A47, A672, NAT_1: 13;

                            

                            then ( LSeg (g,ma)) = ( LSeg (qa,qa1)) by A686, TOPREAL1:def 3

                            .= lma by A688, A691, A690, A692, A687, TOPREAL3: 9, XXREAL_0: 2;

                            then

                             A694: x in ( LSeg (g,ma)) by A665, A666, A688, A691;

                            ( LSeg (g,ma)) in lg by A686, A693;

                            hence thesis by A694, TARSKI:def 4;

                          end;

                        end;

                        hence thesis;

                      end;

                    end;

                    hence thesis;

                  end;

                  1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                  then 1 in ( dom g1) by FINSEQ_3: 25;

                  

                  hence (g /. 1) = (f1 /. 1) by A45, FINSEQ_4: 68

                  .= (f /. 1) by A27, A25, FINSEQ_4: 71;

                  

                   A695: ( len g) = (( len g1) + l) by A396, FINSEQ_1: 22;

                  (i2 + 1) <= j2 by A390, NAT_1: 13;

                  then

                   A696: 1 <= l by XREAL_1: 19;

                  then

                   A697: l in ( dom g2) by A396, FINSEQ_3: 25;

                  

                  hence (g /. ( len g)) = (g2 /. l) by A695, FINSEQ_4: 69

                  .= (G * (i1,(i2 + l))) by A396, A697

                  .= (f /. ( len f)) by A3, A21, A76;

                  thus ( len f) <= ( len g) by A3, A14, A47, A696, A695, XREAL_1: 7;

                end;

              end;

              hence thesis;

            end;

              suppose

               A698: i2 = j2;

              set ppi = (G * (i1,i2)), pj = (G * (j1,i2));

              now

                per cases by XXREAL_0: 1;

                  case

                   A699: i1 > j1;

                  (c1 /. i1) = (c1 . i1) by A66, A60, PARTFUN1:def 6;

                  then

                   A700: (c1 /. i1) = ppi by A66, MATRIX_0:def 8;

                  then

                   A701: (x2 . i1) = (ppi `1 ) by A66, A18, A63, A64, A59, GOBOARD1:def 1;

                  (c1 /. j1) = (c1 . j1) by A23, A60, PARTFUN1:def 6;

                  then

                   A702: (c1 /. j1) = pj by A23, MATRIX_0:def 8;

                  then

                   A703: (x2 . j1) = (pj `1 ) by A23, A18, A63, A64, A59, GOBOARD1:def 1;

                  then

                   A704: (pj `1 ) < (ppi `1 ) by A66, A23, A18, A69, A63, A64, A59, A699, A701, SEQM_3:def 1;

                  reconsider l = (i1 - j1) as Element of NAT by A699, INT_1: 5;

                  defpred P1[ Nat, set] means for m st m = (i1 - $1) holds $2 = (G * (m,i2));

                  set lk = { w where w be Point of ( TOP-REAL 2) : (w `2 ) = (ppi `2 ) & (pj `1 ) <= (w `1 ) & (w `1 ) <= (ppi `1 ) };

                  

                   A705: ppi = |[(ppi `1 ), (ppi `2 )]| by EUCLID: 53;

                   A706:

                  now

                    let n;

                    assume n in ( Seg l);

                    then

                     A707: n <= l by FINSEQ_1: 1;

                    l <= i1 by XREAL_1: 43;

                    then

                    reconsider w = (i1 - n) as Element of NAT by A707, INT_1: 5, XXREAL_0: 2;

                    (i1 - n) <= i1 & i1 <= ( len G) by A66, FINSEQ_3: 25, XREAL_1: 43;

                    then

                     A708: w <= ( len G) by XXREAL_0: 2;

                    

                     A709: 1 <= j1 by A23, FINSEQ_3: 25;

                    (i1 - l) <= (i1 - n) by A707, XREAL_1: 13;

                    then 1 <= w by A709, XXREAL_0: 2;

                    then w in ( dom G) by A708, FINSEQ_3: 25;

                    hence (i1 - n) is Nat & [(i1 - n), i2] in ( Indices G) & (i1 - n) in ( dom G) by A22, A68, ZFMISC_1: 87;

                  end;

                   A710:

                  now

                    let n be Nat;

                    assume n in ( Seg l);

                    then

                    reconsider m = (i1 - n) as Nat by A706;

                    take p = (G * (m,i2));

                    thus P1[n, p];

                  end;

                  consider g2 such that

                   A711: ( len g2) = l & for n be Nat st n in ( Seg l) holds P1[n, (g2 /. n)] from FINSEQ_4:sch 1( A710);

                  take g = (g1 ^ g2);

                  

                   A712: ( dom g2) = ( Seg l) by A711, FINSEQ_1:def 3;

                  now

                    let n;

                    assume

                     A713: n in ( dom g2);

                    then

                    reconsider m = (i1 - n) as Nat by A706, A712;

                    take m, k = i2;

                    thus [m, k] in ( Indices G) & (g2 /. n) = (G * (m,k)) by A706, A711, A712, A713;

                  end;

                  then

                   A714: for n st n in ( dom g) holds ex i, j st [i, j] in ( Indices G) & (g /. n) = (G * (i,j)) by A75, GOBOARD1: 23;

                  

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

                  

                   A716: (y2 . i1) = (ppi `2 ) by A66, A18, A61, A59, A700, GOBOARD1:def 2;

                   A717:

                  now

                    let n, p;

                    assume that

                     A718: n in ( dom g2) and

                     A719: (g2 /. n) = p;

                    reconsider n1 = (i1 - n) as Nat by A706, A712, A718;

                    n <= ( len g2) by A715, A718, FINSEQ_1: 1;

                    then

                     A720: (i1 - ( len g2)) <= n1 by XREAL_1: 13;

                    set pn = (G * (n1,i2));

                    

                     A721: (g2 /. n) = pn by A711, A715, A718;

                    

                     A722: (i1 - n) in ( dom G) by A706, A711, A715, A718;

                    then

                     A723: (y2 . n1) = (y2 . i1) by A66, A18, A70, A61, A59, SEQM_3:def 10;

                    (c1 /. n1) = (c1 . n1) by A60, A722, PARTFUN1:def 6;

                    then

                     A724: (c1 /. n1) = pn by A722, MATRIX_0:def 8;

                    then

                     A725: (x2 . n1) = (pn `1 ) by A18, A63, A64, A59, A722, GOBOARD1:def 1;

                    (y2 . n1) = (pn `2 ) by A18, A61, A59, A722, A724, GOBOARD1:def 2;

                    hence (p `2 ) = (ppi `2 ) & (pj `1 ) <= (p `1 ) & (p `1 ) <= (ppi `1 ) by A66, A23, A18, A69, A63, A64, A59, A711, A716, A701, A703, A719, A722, A721, A720, A723, A725, SEQ_4: 137, XREAL_1: 43;

                    thus p in ( rng c1) by A60, A719, A722, A721, A724, PARTFUN2: 2;

                    1 <= n by A715, A718, FINSEQ_1: 1;

                    then n1 < i1 by XREAL_1: 44;

                    hence (p `1 ) < (ppi `1 ) by A66, A18, A69, A63, A64, A59, A701, A719, A722, A721, A725, SEQM_3:def 1;

                  end;

                  

                   A726: g2 is special

                  proof

                    let n be Nat;

                    set p = (g2 /. n);

                    assume

                     A727: 1 <= n & (n + 1) <= ( len g2);

                    then n in ( dom g2) by SEQ_4: 134;

                    then

                     A728: (p `2 ) = (ppi `2 ) by A717;

                    (n + 1) in ( dom g2) by A727, SEQ_4: 134;

                    hence thesis by A717, A728;

                  end;

                   A729:

                  now

                    let n, m, p, q;

                    assume that

                     A730: n in ( dom g2) and

                     A731: m in ( dom g2) and

                     A732: n < m and

                     A733: (g2 /. n) = p & (g2 /. m) = q;

                    

                     A734: (i1 - n) in ( dom G) by A706, A712, A730;

                    reconsider n1 = (i1 - n), m1 = (i1 - m) as Nat by A706, A712, A730, A731;

                    set pn = (G * (n1,i2)), pm = (G * (m1,i2));

                    

                     A735: m1 < n1 by A732, XREAL_1: 15;

                    (c1 /. n1) = (c1 . n1) by A60, A706, A712, A730, PARTFUN1:def 6;

                    then (c1 /. n1) = pn by A734, MATRIX_0:def 8;

                    then

                     A736: (x2 . n1) = (pn `1 ) by A65, A60, A734, GOBOARD1:def 1;

                    

                     A737: (i1 - m) in ( dom G) by A706, A712, A731;

                    (c1 /. m1) = (c1 . m1) by A60, A706, A712, A731, PARTFUN1:def 6;

                    then (c1 /. m1) = pm by A737, MATRIX_0:def 8;

                    then

                     A738: (x2 . m1) = (pm `1 ) by A65, A60, A737, GOBOARD1:def 1;

                    (g2 /. n) = pn & (g2 /. m) = pm by A711, A712, A730, A731;

                    hence (q `1 ) < (p `1 ) by A69, A65, A60, A733, A734, A737, A735, A736, A738, SEQM_3:def 1;

                  end;

                  for n, m st m > (n + 1) & n in ( dom g2) & (n + 1) in ( dom g2) & m in ( dom g2) & (m + 1) in ( dom g2) holds ( LSeg (g2,n)) misses ( LSeg (g2,m))

                  proof

                    let n, m;

                    assume that

                     A739: m > (n + 1) and

                     A740: n in ( dom g2) and

                     A741: (n + 1) in ( dom g2) and

                     A742: m in ( dom g2) and

                     A743: (m + 1) in ( dom g2) and

                     A744: (( LSeg (g2,n)) /\ ( LSeg (g2,m))) <> {} ;

                    reconsider p1 = (g2 /. n), p2 = (g2 /. (n + 1)), q1 = (g2 /. m), q2 = (g2 /. (m + 1)) as Point of ( TOP-REAL 2);

                    

                     A745: (p1 `2 ) = (ppi `2 ) & (p2 `2 ) = (ppi `2 ) by A717, A740, A741;

                    n < (n + 1) by NAT_1: 13;

                    then

                     A746: (p2 `1 ) < (p1 `1 ) by A729, A740, A741;

                    set lp = { w where w be Point of ( TOP-REAL 2) : (w `2 ) = (ppi `2 ) & (p2 `1 ) <= (w `1 ) & (w `1 ) <= (p1 `1 ) }, lq = { w where w be Point of ( TOP-REAL 2) : (w `2 ) = (ppi `2 ) & (q2 `1 ) <= (w `1 ) & (w `1 ) <= (q1 `1 ) };

                    

                     A747: p1 = |[(p1 `1 ), (p1 `2 )]| & p2 = |[(p2 `1 ), (p2 `2 )]| by EUCLID: 53;

                    m < (m + 1) by NAT_1: 13;

                    then

                     A748: (q2 `1 ) < (q1 `1 ) by A729, A742, A743;

                    

                     A749: q1 = |[(q1 `1 ), (q1 `2 )]| & q2 = |[(q2 `1 ), (q2 `2 )]| by EUCLID: 53;

                    set x = the Element of (( LSeg (g2,n)) /\ ( LSeg (g2,m)));

                    

                     A750: x in ( LSeg (g2,n)) by A744, XBOOLE_0:def 4;

                    

                     A751: (q1 `2 ) = (ppi `2 ) & (q2 `2 ) = (ppi `2 ) by A717, A742, A743;

                    

                     A752: x in ( LSeg (g2,m)) by A744, XBOOLE_0:def 4;

                    1 <= m & (m + 1) <= ( len g2) by A742, A743, FINSEQ_3: 25;

                    

                    then ( LSeg (g2,m)) = ( LSeg (q2,q1)) by TOPREAL1:def 3

                    .= lq by A748, A751, A749, TOPREAL3: 10;

                    then

                     A753: ex tm be Point of ( TOP-REAL 2) st tm = x & (tm `2 ) = (ppi `2 ) & (q2 `1 ) <= (tm `1 ) & (tm `1 ) <= (q1 `1 ) by A752;

                    1 <= n & (n + 1) <= ( len g2) by A740, A741, FINSEQ_3: 25;

                    

                    then ( LSeg (g2,n)) = ( LSeg (p2,p1)) by TOPREAL1:def 3

                    .= lp by A746, A745, A747, TOPREAL3: 10;

                    then

                     A754: ex tn be Point of ( TOP-REAL 2) st tn = x & (tn `2 ) = (ppi `2 ) & (p2 `1 ) <= (tn `1 ) & (tn `1 ) <= (p1 `1 ) by A750;

                    (q1 `1 ) < (p2 `1 ) by A729, A739, A741, A742;

                    hence contradiction by A754, A753, XXREAL_0: 2;

                  end;

                  then

                   A755: g2 is s.n.c. by GOBOARD2: 1;

                  

                   A756: not (f /. k) in ( L~ g2)

                  proof

                    set ls = { ( LSeg (g2,m)) : 1 <= m & (m + 1) <= ( len g2) };

                    assume (f /. k) in ( L~ g2);

                    then

                    consider X be set such that

                     A757: (f /. k) in X and

                     A758: X in ls by TARSKI:def 4;

                    consider m such that

                     A759: X = ( LSeg (g2,m)) and

                     A760: 1 <= m & (m + 1) <= ( len g2) by A758;

                    reconsider q1 = (g2 /. m), q2 = (g2 /. (m + 1)) as Point of ( TOP-REAL 2);

                    

                     A761: m in ( dom g2) by A760, SEQ_4: 134;

                    then

                     A762: (q1 `2 ) = (ppi `2 ) by A717;

                    set lq = { w where w be Point of ( TOP-REAL 2) : (w `2 ) = (ppi `2 ) & (q2 `1 ) <= (w `1 ) & (w `1 ) <= (q1 `1 ) };

                    

                     A763: q1 = |[(q1 `1 ), (q1 `2 )]| & q2 = |[(q2 `1 ), (q2 `2 )]| by EUCLID: 53;

                    

                     A764: (m + 1) in ( dom g2) by A760, SEQ_4: 134;

                    then

                     A765: (q2 `2 ) = (ppi `2 ) by A717;

                    m < (m + 1) by NAT_1: 13;

                    then

                     A766: (q2 `1 ) < (q1 `1 ) by A729, A761, A764;

                    ( LSeg (g2,m)) = ( LSeg (q2,q1)) by A760, TOPREAL1:def 3

                    .= lq by A762, A765, A766, A763, TOPREAL3: 10;

                    then ex p st p = (f /. k) & (p `2 ) = (ppi `2 ) & (q2 `1 ) <= (p `1 ) & (p `1 ) <= (q1 `1 ) by A757, A759;

                    hence contradiction by A29, A717, A761;

                  end;

                  (y2 . j1) = (pj `2 ) by A23, A18, A61, A59, A702, GOBOARD1:def 2;

                  then

                   A767: (ppi `2 ) = (pj `2 ) by A66, A23, A18, A70, A61, A59, A716, SEQM_3:def 10;

                  now

                    let n,m be Element of NAT ;

                    assume that

                     A768: n in ( dom g2) & m in ( dom g2) and

                     A769: n <> m;

                    reconsider n1 = (i1 - n), m1 = (i1 - m) as Nat by A706, A712, A768;

                    

                     A770: (g2 /. n) = (G * (n1,i2)) & (g2 /. m) = (G * (m1,i2)) by A711, A712, A768;

                    assume

                     A771: (g2 /. n) = (g2 /. m);

                     [(i1 - n), i2] in ( Indices G) & [(i1 - m), i2] in ( Indices G) by A706, A712, A768;

                    then n1 = m1 by A770, A771, GOBOARD1: 5;

                    hence contradiction by A769;

                  end;

                  then for n,m be Element of NAT st n in ( dom g2) & m in ( dom g2) & (g2 /. n) = (g2 /. m) holds n = m;

                  then

                   A772: g2 is one-to-one by PARTFUN2: 9;

                  reconsider m1 = (i1 - l) as Nat;

                  

                   A773: pj = |[(pj `1 ), (pj `2 )]| by EUCLID: 53;

                  

                   A774: ( LSeg (f,k)) = ( LSeg (pj,ppi)) by A3, A24, A29, A21, A698, TOPREAL1:def 3

                  .= lk by A704, A767, A705, A773, TOPREAL3: 10;

                  

                   A775: ( rng g2) c= ( LSeg (f,k))

                  proof

                    let x be object;

                    assume x in ( rng g2);

                    then

                    consider n be Element of NAT such that

                     A776: n in ( dom g2) and

                     A777: (g2 /. n) = x by PARTFUN2: 2;

                    reconsider n1 = (i1 - n) as Nat by A706, A711, A715, A776;

                    set pn = (G * (n1,i2));

                    

                     A778: (g2 /. n) = pn by A711, A715, A776;

                    then

                     A779: (pn `1 ) <= (ppi `1 ) by A717, A776;

                    (pn `2 ) = (ppi `2 ) & (pj `1 ) <= (pn `1 ) by A717, A776, A778;

                    hence thesis by A774, A777, A778, A779;

                  end;

                   A780:

                  now

                    let n;

                    assume that

                     A781: n in ( dom g2) and

                     A782: (n + 1) in ( dom g2);

                    reconsider m1 = (i1 - n), m2 = (i1 - (n + 1)) as Nat by A706, A712, A781, A782;

                    let l1,l2,l3,l4 be Nat;

                    assume that

                     A783: [l1, l2] in ( Indices G) and

                     A784: [l3, l4] in ( Indices G) and

                     A785: (g2 /. n) = (G * (l1,l2)) and

                     A786: (g2 /. (n + 1)) = (G * (l3,l4));

                     [(i1 - (n + 1)), i2] in ( Indices G) & (g2 /. (n + 1)) = (G * (m2,i2)) by A706, A711, A712, A782;

                    then

                     A787: l3 = m2 & l4 = i2 by A784, A786, GOBOARD1: 5;

                     [(i1 - n), i2] in ( Indices G) & (g2 /. n) = (G * (m1,i2)) by A706, A711, A712, A781;

                    then l1 = m1 & l2 = i2 by A783, A785, GOBOARD1: 5;

                    

                    hence ( |.(l1 - l3).| + |.(l2 - l4).|) = ( |.((i1 - n) - (i1 - (n + 1))).| + 0 ) by A787, ABSVALUE: 2

                    .= 1 by ABSVALUE:def 1;

                  end;

                  now

                    let l1,l2,l3,l4 be Nat;

                    assume that

                     A788: [l1, l2] in ( Indices G) and

                     A789: [l3, l4] in ( Indices G) and

                     A790: (g1 /. ( len g1)) = (G * (l1,l2)) and

                     A791: (g2 /. 1) = (G * (l3,l4)) and ( len g1) in ( dom g1) and

                     A792: 1 in ( dom g2);

                    reconsider m1 = (i1 - 1) as Nat by A706, A712, A792;

                     [(i1 - 1), i2] in ( Indices G) & (g2 /. 1) = (G * (m1,i2)) by A706, A711, A712, A792;

                    then

                     A793: l3 = m1 & l4 = i2 by A789, A791, GOBOARD1: 5;

                    (f1 /. ( len f1)) = (f /. k) by A27, A14, A51, FINSEQ_4: 71;

                    then l1 = i1 & l2 = i2 by A46, A28, A29, A788, A790, GOBOARD1: 5;

                    

                    hence ( |.(l1 - l3).| + |.(l2 - l4).|) = ( |.(i1 - (i1 - 1)).| + 0 ) by A793, ABSVALUE: 2

                    .= 1 by ABSVALUE:def 1;

                  end;

                  then for n st n in ( dom g) & (n + 1) in ( dom g) holds for m, k, i, j st [m, k] in ( Indices G) & [i, j] in ( Indices G) & (g /. n) = (G * (m,k)) & (g /. (n + 1)) = (G * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1 by A48, A780, GOBOARD1: 24;

                  hence g is_sequence_on G by A714, GOBOARD1:def 9;

                  

                   A794: ( LSeg (f,k)) = ( LSeg (ppi,pj)) by A3, A24, A29, A21, A698, TOPREAL1:def 3;

                  

                   A795: not (f /. k) in ( rng g2)

                  proof

                    assume (f /. k) in ( rng g2);

                    then

                    consider n be Element of NAT such that

                     A796: n in ( dom g2) and

                     A797: (g2 /. n) = (f /. k) by PARTFUN2: 2;

                    reconsider n1 = (i1 - n) as Nat by A706, A711, A715, A796;

                     [(i1 - n), i2] in ( Indices G) & (g2 /. n) = (G * (n1,i2)) by A706, A711, A715, A796;

                    then

                     A798: n1 = i1 by A28, A29, A797, GOBOARD1: 5;

                     0 < n by A715, A796, FINSEQ_1: 1;

                    hence contradiction by A798;

                  end;

                  (( rng g1) /\ ( rng g2)) = {}

                  proof

                    set x = the Element of (( rng g1) /\ ( rng g2));

                    assume

                     A799: not thesis;

                    then

                     A800: x in ( rng g2) by XBOOLE_0:def 4;

                    

                     A801: x in ( rng g1) by A799, XBOOLE_0:def 4;

                    now

                      per cases by A24, XXREAL_0: 1;

                        suppose k = 1;

                        hence contradiction by A52, A795, A801, A800, TARSKI:def 1;

                      end;

                        suppose 1 < k;

                        then x in (( L~ f1) /\ ( LSeg (f,k))) & (( L~ f1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, A49, A775, A801, A800, GOBOARD2: 4, XBOOLE_0:def 4;

                        hence contradiction by A795, A800, TARSKI:def 1;

                      end;

                    end;

                    hence contradiction;

                  end;

                  then ( rng g1) misses ( rng g2);

                  hence g is one-to-one by A40, A772, FINSEQ_3: 91;

                  

                   A802: for n st 1 <= n & (n + 2) <= ( len g2) holds (( LSeg (g2,n)) /\ ( LSeg (g2,(n + 1)))) = {(g2 /. (n + 1))}

                  proof

                    let n;

                    assume that

                     A803: 1 <= n and

                     A804: (n + 2) <= ( len g2);

                    

                     A805: (n + 1) in ( dom g2) by A803, A804, SEQ_4: 135;

                    then (g2 /. (n + 1)) in ( rng g2) by PARTFUN2: 2;

                    then (g2 /. (n + 1)) in lk by A774, A775;

                    then

                    consider u1 be Point of ( TOP-REAL 2) such that

                     A806: (g2 /. (n + 1)) = u1 and

                     A807: (u1 `2 ) = (ppi `2 ) and (pj `1 ) <= (u1 `1 ) and (u1 `1 ) <= (ppi `1 );

                    

                     A808: (n + 2) in ( dom g2) by A803, A804, SEQ_4: 135;

                    then (g2 /. (n + 2)) in ( rng g2) by PARTFUN2: 2;

                    then (g2 /. (n + 2)) in lk by A774, A775;

                    then

                    consider u2 be Point of ( TOP-REAL 2) such that

                     A809: (g2 /. (n + 2)) = u2 and

                     A810: (u2 `2 ) = (ppi `2 ) and (pj `1 ) <= (u2 `1 ) and (u2 `1 ) <= (ppi `1 );

                    1 <= (n + 1) & ((n + 1) + 1) = (n + (1 + 1)) by NAT_1: 11;

                    then

                     A811: ( LSeg (g2,(n + 1))) = ( LSeg (u1,u2)) by A804, A806, A809, TOPREAL1:def 3;

                    (n + 1) < ((n + 1) + 1) by NAT_1: 13;

                    then

                     A812: (u2 `1 ) < (u1 `1 ) by A729, A805, A808, A806, A809;

                    

                     A813: n in ( dom g2) by A803, A804, SEQ_4: 135;

                    then (g2 /. n) in ( rng g2) by PARTFUN2: 2;

                    then (g2 /. n) in lk by A774, A775;

                    then

                    consider u be Point of ( TOP-REAL 2) such that

                     A814: (g2 /. n) = u and

                     A815: (u `2 ) = (ppi `2 ) and (pj `1 ) <= (u `1 ) and (u `1 ) <= (ppi `1 );

                    (n + 1) <= (n + 2) by XREAL_1: 6;

                    then (n + 1) <= ( len g2) by A804, XXREAL_0: 2;

                    then

                     A816: ( LSeg (g2,n)) = ( LSeg (u,u1)) by A803, A814, A806, TOPREAL1:def 3;

                    set lg = { w where w be Point of ( TOP-REAL 2) : (w `2 ) = (ppi `2 ) & (u2 `1 ) <= (w `1 ) & (w `1 ) <= (u `1 ) };

                    n < (n + 1) by NAT_1: 13;

                    then

                     A817: (u1 `1 ) < (u `1 ) by A729, A813, A805, A814, A806;

                    then

                     A818: u1 in lg by A807, A812;

                    u = |[(u `1 ), (u `2 )]| & u2 = |[(u2 `1 ), (u2 `2 )]| by EUCLID: 53;

                    then ( LSeg ((g2 /. n),(g2 /. (n + 2)))) = lg by A814, A815, A809, A810, A812, A817, TOPREAL3: 10, XXREAL_0: 2;

                    hence thesis by A814, A806, A809, A816, A811, A818, TOPREAL1: 8;

                  end;

                  thus g is unfolded

                  proof

                    let n be Nat;

                    assume that

                     A819: 1 <= n and

                     A820: (n + 2) <= ( len g);

                    

                     A821: ((n + 1) + 1) <= ( len g) by A820;

                    (n + 1) <= ((n + 1) + 1) by NAT_1: 11;

                    then

                     A822: (n + 1) <= ( len g) by A820, XXREAL_0: 2;

                    

                     A823: ( len g) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

                    ((n + 2) - ( len g1)) = ((n - ( len g1)) + 2);

                    then

                     A824: ((n - ( len g1)) + 2) <= ( len g2) by A820, A823, XREAL_1: 20;

                    

                     A825: 1 <= (n + 1) by NAT_1: 11;

                    

                     A826: n <= (n + 1) by NAT_1: 11;

                    

                     A827: (n + (1 + 1)) = ((n + 1) + 1);

                    per cases ;

                      suppose

                       A828: (n + 2) <= ( len g1);

                      

                       A829: (n + (1 + 1)) = ((n + 1) + 1);

                      

                       A830: (n + 1) in ( dom g1) by A819, A828, SEQ_4: 135;

                      then

                       A831: (g /. (n + 1)) = (g1 /. (n + 1)) by FINSEQ_4: 68;

                      n in ( dom g1) by A819, A828, SEQ_4: 135;

                      then

                       A832: ( LSeg (g1,n)) = ( LSeg (g,n)) by A830, TOPREAL3: 18;

                      (n + 2) in ( dom g1) by A819, A828, SEQ_4: 135;

                      then ( LSeg (g1,(n + 1))) = ( LSeg (g,(n + 1))) by A830, A829, TOPREAL3: 18;

                      hence thesis by A41, A819, A828, A832, A831;

                    end;

                      suppose ( len g1) < (n + 2);

                      then (( len g1) + 1) <= (n + 2) by NAT_1: 13;

                      then

                       A833: ( len g1) <= ((n + 2) - 1) by XREAL_1: 19;

                      thus thesis

                      proof

                        per cases ;

                          suppose

                           A834: ( len g1) = (n + 1);

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

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

                          then

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

                          then (g2 /. 1) in lk by A774, A775;

                          then

                          consider u1 be Point of ( TOP-REAL 2) such that

                           A836: (g2 /. 1) = u1 and (u1 `2 ) = (ppi `2 ) and (pj `1 ) <= (u1 `1 ) and (u1 `1 ) <= (ppi `1 );

                          ppi in ( LSeg (ppi,pj)) by RLTOPSP1: 68;

                          then

                           A837: ( LSeg (ppi,u1)) c= ( LSeg (f,k)) by A794, A775, A835, A836, TOPREAL1: 6;

                          1 <= (n + 1) by NAT_1: 11;

                          then

                           A838: (n + 1) in ( dom g1) by A834, FINSEQ_3: 25;

                          

                          then

                           A839: (g /. (n + 1)) = (f1 /. ( len f1)) by A46, A834, FINSEQ_4: 68

                          .= ppi by A27, A14, A51, A29, FINSEQ_4: 71;

                          now

                            1 < ( len g1) by A819, A834, NAT_1: 13;

                            then

                             A840: (1 + 1) <= ( len g1) by NAT_1: 13;

                            assume k = 1;

                            hence contradiction by A52, A840, TOPREAL1: 23;

                          end;

                          then 1 < k by A24, XXREAL_0: 1;

                          then

                           A841: (( L~ f1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, GOBOARD2: 4;

                          

                           A842: ( LSeg (g1,n)) c= ( L~ f1) by A44, TOPREAL3: 19;

                          n in ( dom g1) by A819, A826, A834, FINSEQ_3: 25;

                          then

                           A843: ( LSeg (g,n)) = ( LSeg (g1,n)) by A838, TOPREAL3: 18;

                          (g /. (n + 1)) in ( LSeg (g,n)) & (g /. (n + 1)) in ( LSeg (g,(n + 1))) by A819, A820, A825, A822, A827, TOPREAL1: 21;

                          then (g /. (n + 1)) in (( LSeg (g,n)) /\ ( LSeg (g,(n + 1)))) by XBOOLE_0:def 4;

                          then

                           A844: {(g /. (n + 1))} c= (( LSeg (g,n)) /\ ( LSeg (g,(n + 1)))) by ZFMISC_1: 31;

                          1 <= ( len g2) by A820, A827, A823, A834, XREAL_1: 6;

                          then (g /. (n + 2)) = (g2 /. 1) by A827, A834, SEQ_4: 136;

                          then ( LSeg (g,(n + 1))) = ( LSeg (ppi,u1)) by A820, A825, A827, A839, A836, TOPREAL1:def 3;

                          then (( LSeg (g,n)) /\ ( LSeg (g,(n + 1)))) c= {(g /. (n + 1))} by A29, A842, A841, A843, A839, A837, XBOOLE_1: 27;

                          hence thesis by A844;

                        end;

                          suppose ( len g1) <> (n + 1);

                          then ( len g1) < (n + 1) by A833, XXREAL_0: 1;

                          then

                           A845: ( len g1) <= n by NAT_1: 13;

                          then

                          reconsider n1 = (n - ( len g1)) as Element of NAT by INT_1: 5;

                          thus thesis

                          proof

                            per cases ;

                              suppose

                               A846: ( len g1) = n;

                              then

                               A847: 2 <= ( len g2) by A820, A823, XREAL_1: 6;

                              then 1 <= ( len g2) by XXREAL_0: 2;

                              then

                               A848: (g /. (n + 1)) = (g2 /. 1) by A846, SEQ_4: 136;

                              1 <= ( len g2) by A847, XXREAL_0: 2;

                              then

                               A849: 1 in ( dom g2) by FINSEQ_3: 25;

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

                              then (g2 /. 1) in lk by A774, A775;

                              then

                              consider u1 be Point of ( TOP-REAL 2) such that

                               A850: (g2 /. 1) = u1 and

                               A851: (u1 `2 ) = (ppi `2 ) and (pj `1 ) <= (u1 `1 ) and

                               A852: (u1 `1 ) <= (ppi `1 );

                              1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                              then ( len g1) in ( dom g1) by FINSEQ_3: 25;

                              

                              then (g /. n) = (f1 /. ( len f1)) by A46, A846, FINSEQ_4: 68

                              .= ppi by A27, A14, A51, A29, FINSEQ_4: 71;

                              then

                               A853: ( LSeg (g,n)) = ( LSeg (ppi,u1)) by A819, A822, A848, A850, TOPREAL1:def 3;

                              

                               A854: 2 in ( dom g2) by A847, FINSEQ_3: 25;

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

                              then (g2 /. 2) in lk by A774, A775;

                              then

                              consider u2 be Point of ( TOP-REAL 2) such that

                               A855: (g2 /. 2) = u2 and

                               A856: (u2 `2 ) = (ppi `2 ) and (pj `1 ) <= (u2 `1 ) and

                               A857: (u2 `1 ) <= (ppi `1 );

                              set lg = { w where w be Point of ( TOP-REAL 2) : (w `2 ) = (ppi `2 ) & (u2 `1 ) <= (w `1 ) & (w `1 ) <= (ppi `1 ) };

                              u2 = |[(u2 `1 ), (u2 `2 )]| by EUCLID: 53;

                              then

                               A858: ( LSeg (ppi,(g2 /. 2))) = lg by A705, A855, A856, A857, TOPREAL3: 10;

                              (u2 `1 ) < (u1 `1 ) by A729, A849, A854, A850, A855;

                              then

                               A859: u1 in lg by A851, A852;

                              (g /. (n + 2)) = (g2 /. 2) by A846, A847, SEQ_4: 136;

                              then ( LSeg (g,(n + 1))) = ( LSeg (u1,u2)) by A820, A825, A827, A848, A850, A855, TOPREAL1:def 3;

                              hence thesis by A848, A850, A855, A859, A853, A858, TOPREAL1: 8;

                            end;

                              suppose ( len g1) <> n;

                              then

                               A860: ( len g1) < n by A845, XXREAL_0: 1;

                              then (( len g1) + 1) <= n by NAT_1: 13;

                              then

                               A861: 1 <= n1 by XREAL_1: 19;

                              (n1 + ( len g1)) = n;

                              then

                               A862: ( LSeg (g,n)) = ( LSeg (g2,n1)) by A822, A860, GOBOARD2: 5;

                              

                               A863: (n + 1) = ((n1 + 1) + ( len g1));

                              ((n1 + 1) + ( len g1)) = (n + 1);

                              then (n1 + 1) <= ( len g2) by A822, A823, XREAL_1: 6;

                              then

                               A864: (g /. (n + 1)) = (g2 /. (n1 + 1)) by A863, NAT_1: 11, SEQ_4: 136;

                              ( len g1) < (n + 1) by A826, A860, XXREAL_0: 2;

                              then ( LSeg (g,(n + 1))) = ( LSeg (g2,(n1 + 1))) by A821, A863, GOBOARD2: 5;

                              hence thesis by A802, A824, A862, A864, A861;

                            end;

                          end;

                        end;

                      end;

                    end;

                  end;

                  

                   A865: ( L~ g2) c= ( LSeg (f,k))

                  proof

                    let x be object;

                    set ls = { ( LSeg (g2,m)) : 1 <= m & (m + 1) <= ( len g2) };

                    assume x in ( L~ g2);

                    then

                    consider X be set such that

                     A866: x in X and

                     A867: X in ls by TARSKI:def 4;

                    consider m such that

                     A868: X = ( LSeg (g2,m)) and

                     A869: 1 <= m & (m + 1) <= ( len g2) by A867;

                    reconsider q1 = (g2 /. m), q2 = (g2 /. (m + 1)) as Point of ( TOP-REAL 2);

                    

                     A870: ( LSeg (g2,m)) = ( LSeg (q1,q2)) by A869, TOPREAL1:def 3;

                    (m + 1) in ( dom g2) by A869, SEQ_4: 134;

                    then

                     A871: (g2 /. (m + 1)) in ( rng g2) by PARTFUN2: 2;

                    m in ( dom g2) by A869, SEQ_4: 134;

                    then (g2 /. m) in ( rng g2) by PARTFUN2: 2;

                    then ( LSeg (q1,q2)) c= ( LSeg (ppi,pj)) by A794, A775, A871, TOPREAL1: 6;

                    hence thesis by A794, A866, A868, A870;

                  end;

                  

                   A872: (( L~ g1) /\ ( L~ g2)) = {}

                  proof

                    per cases ;

                      suppose k = 1;

                      hence thesis by A52;

                    end;

                      suppose k <> 1;

                      then 1 < k by A24, XXREAL_0: 1;

                      then (( L~ g1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, A44, GOBOARD2: 4;

                      then

                       A873: (( L~ g1) /\ ( L~ g2)) c= {(f /. k)} by A865, XBOOLE_1: 26;

                      now

                        set x = the Element of (( L~ g1) /\ ( L~ g2));

                        assume (( L~ g1) /\ ( L~ g2)) <> {} ;

                        then x in {(f /. k)} & x in ( L~ g2) by A873, XBOOLE_0:def 4;

                        hence contradiction by A756, TARSKI:def 1;

                      end;

                      hence thesis;

                    end;

                  end;

                  for n, m st m > (n + 1) & n in ( dom g) & (n + 1) in ( dom g) & m in ( dom g) & (m + 1) in ( dom g) holds ( LSeg (g,n)) misses ( LSeg (g,m))

                  proof

                    

                     A874: 1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                    then ( len g1) in ( dom g1) by FINSEQ_3: 25;

                    

                    then

                     A875: (g /. ( len g1)) = (g1 /. ( len g1)) by FINSEQ_4: 68

                    .= ppi by A27, A14, A51, A46, A29, FINSEQ_4: 71;

                    reconsider qq = (g2 /. 1) as Point of ( TOP-REAL 2);

                    set l1 = { ( LSeg (g1,i)) : 1 <= i & (i + 1) <= ( len g1) }, l2 = { ( LSeg (g2,j)) : 1 <= j & (j + 1) <= ( len g2) };

                    let n, m;

                    assume that

                     A876: m > (n + 1) and

                     A877: n in ( dom g) and

                     A878: (n + 1) in ( dom g) and

                     A879: m in ( dom g) and

                     A880: (m + 1) in ( dom g);

                    

                     A881: 1 <= n by A877, FINSEQ_3: 25;

                    (j1 + 1) <= i1 by A699, NAT_1: 13;

                    then

                     A882: 1 <= l by XREAL_1: 19;

                    then

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

                    then

                     A884: (qq `2 ) = (ppi `2 ) & (qq `1 ) < (ppi `1 ) by A717;

                    

                     A885: (g /. (( len g1) + 1)) = qq by A711, A882, SEQ_4: 136;

                    

                     A886: (pj `1 ) <= (qq `1 ) by A717, A883;

                    

                     A887: (m + 1) <= ( len g) by A880, FINSEQ_3: 25;

                    

                     A888: 1 <= (m + 1) by A880, FINSEQ_3: 25;

                    

                     A889: 1 <= (n + 1) by A878, FINSEQ_3: 25;

                    

                     A890: (n + 1) <= ( len g) by A878, FINSEQ_3: 25;

                    

                     A891: qq = |[(qq `1 ), (qq `2 )]| by EUCLID: 53;

                    

                     A892: 1 <= m by A879, FINSEQ_3: 25;

                    set ql = { z where z be Point of ( TOP-REAL 2) : (z `2 ) = (ppi `2 ) & (qq `1 ) <= (z `1 ) & (z `1 ) <= (ppi `1 ) };

                    

                     A893: n <= (n + 1) by NAT_1: 11;

                    

                     A894: ( len g) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

                    then (( len g1) + 1) <= ( len g) by A711, A882, XREAL_1: 7;

                    

                    then

                     A895: ( LSeg (g,( len g1))) = ( LSeg (qq,ppi)) by A874, A875, A885, TOPREAL1:def 3

                    .= ql by A705, A884, A891, TOPREAL3: 10;

                    

                     A896: m <= (m + 1) by NAT_1: 11;

                    then

                     A897: (n + 1) <= (m + 1) by A876, XXREAL_0: 2;

                    now

                      per cases ;

                        suppose

                         A898: (m + 1) <= ( len g1);

                        then m <= ( len g1) by A896, XXREAL_0: 2;

                        then

                         A899: m in ( dom g1) by A892, FINSEQ_3: 25;

                        (m + 1) in ( dom g1) by A888, A898, FINSEQ_3: 25;

                        then

                         A900: ( LSeg (g,m)) = ( LSeg (g1,m)) by A899, TOPREAL3: 18;

                        

                         A901: (n + 1) <= ( len g1) by A897, A898, XXREAL_0: 2;

                        then n <= ( len g1) by A893, XXREAL_0: 2;

                        then

                         A902: n in ( dom g1) by A881, FINSEQ_3: 25;

                        (n + 1) in ( dom g1) by A889, A901, FINSEQ_3: 25;

                        then ( LSeg (g,n)) = ( LSeg (g1,n)) by A902, TOPREAL3: 18;

                        hence thesis by A42, A876, A900;

                      end;

                        suppose ( len g1) < (m + 1);

                        then

                         A903: ( len g1) <= m by NAT_1: 13;

                        then

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

                        now

                          per cases ;

                            suppose

                             A904: m = ( len g1);

                            

                             A905: ( LSeg (g,m)) c= ( LSeg (f,k))

                            proof

                              let x be object;

                              assume x in ( LSeg (g,m));

                              then

                              consider px be Point of ( TOP-REAL 2) such that

                               A906: px = x & (px `2 ) = (ppi `2 ) and

                               A907: (qq `1 ) <= (px `1 ) and

                               A908: (px `1 ) <= (ppi `1 ) by A895, A904;

                              (pj `1 ) <= (px `1 ) by A886, A907, XXREAL_0: 2;

                              hence thesis by A774, A906, A908;

                            end;

                            n <= ( len g1) by A876, A893, A904, XXREAL_0: 2;

                            then

                             A909: n in ( dom g1) by A881, FINSEQ_3: 25;

                            now

                              1 < ( len g1) by A876, A889, A904, XXREAL_0: 2;

                              then

                               A910: (1 + 1) <= ( len g1) by NAT_1: 13;

                              assume k = 1;

                              hence contradiction by A52, A910, TOPREAL1: 23;

                            end;

                            then 1 < k by A24, XXREAL_0: 1;

                            then

                             A911: (( L~ f1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, GOBOARD2: 4;

                            

                             A912: (n + 1) in ( dom g1) by A876, A889, A904, FINSEQ_3: 25;

                            then

                             A913: ( LSeg (g,n)) = ( LSeg (g1,n)) by A909, TOPREAL3: 18;

                            then ( LSeg (g,n)) in l1 by A876, A881, A904;

                            then ( LSeg (g,n)) c= ( L~ f1) by A44, ZFMISC_1: 74;

                            then

                             A914: (( LSeg (g,n)) /\ ( LSeg (g,m))) c= {(f /. k)} by A911, A905, XBOOLE_1: 27;

                            now

                              set x = the Element of (( LSeg (g,n)) /\ ( LSeg (g,m)));

                              assume

                               A915: (( LSeg (g,n)) /\ ( LSeg (g,m))) <> {} ;

                              then

                               A916: x in ( LSeg (g,n)) by XBOOLE_0:def 4;

                              x in {(f /. k)} by A914, A915;

                              then

                               A917: x = (f /. k) by TARSKI:def 1;

                              (f /. k) = (g1 /. ( len g1)) by A27, A14, A51, A46, FINSEQ_4: 71;

                              hence contradiction by A40, A41, A42, A876, A904, A909, A912, A913, A916, A917, GOBOARD2: 2;

                            end;

                            hence thesis;

                          end;

                            suppose m <> ( len g1);

                            then

                             A918: ( len g1) < m by A903, XXREAL_0: 1;

                            then (( len g1) + 1) <= m by NAT_1: 13;

                            then

                             A919: 1 <= m1 by XREAL_1: 19;

                            (m + 1) = ((m1 + 1) + ( len g1));

                            then

                             A920: (m1 + 1) <= ( len g2) by A887, A894, XREAL_1: 6;

                            m = (m1 + ( len g1));

                            then

                             A921: ( LSeg (g,m)) = ( LSeg (g2,m1)) by A887, A918, GOBOARD2: 5;

                            then ( LSeg (g,m)) in l2 by A919, A920;

                            then

                             A922: ( LSeg (g,m)) c= ( L~ g2) by ZFMISC_1: 74;

                            now

                              per cases ;

                                suppose

                                 A923: (n + 1) <= ( len g1);

                                then n <= ( len g1) by A893, XXREAL_0: 2;

                                then

                                 A924: n in ( dom g1) by A881, FINSEQ_3: 25;

                                (n + 1) in ( dom g1) by A889, A923, FINSEQ_3: 25;

                                then ( LSeg (g,n)) = ( LSeg (g1,n)) by A924, TOPREAL3: 18;

                                then ( LSeg (g,n)) in l1 by A881, A923;

                                then ( LSeg (g,n)) c= ( L~ g1) by ZFMISC_1: 74;

                                then (( LSeg (g,n)) /\ ( LSeg (g,m))) = {} by A872, A922, XBOOLE_1: 3, XBOOLE_1: 27;

                                hence thesis;

                              end;

                                suppose ( len g1) < (n + 1);

                                then

                                 A925: ( len g1) <= n by NAT_1: 13;

                                then

                                reconsider n1 = (n - ( len g1)) as Element of NAT by INT_1: 5;

                                

                                 A926: ((n - ( len g1)) + 1) = ((n + 1) - ( len g1));

                                

                                 A927: n = (n1 + ( len g1));

                                now

                                  per cases ;

                                    suppose

                                     A928: ( len g1) = n;

                                    now

                                      reconsider q1 = (g2 /. m1), q2 = (g2 /. (m1 + 1)) as Point of ( TOP-REAL 2);

                                      set x = the Element of (( LSeg (g,n)) /\ ( LSeg (g,m)));

                                      set q1l = { v where v be Point of ( TOP-REAL 2) : (v `2 ) = (ppi `2 ) & (q2 `1 ) <= (v `1 ) & (v `1 ) <= (q1 `1 ) };

                                      

                                       A929: q1 = |[(q1 `1 ), (q1 `2 )]| & q2 = |[(q2 `1 ), (q2 `2 )]| by EUCLID: 53;

                                      assume

                                       A930: (( LSeg (g,n)) /\ ( LSeg (g,m))) <> {} ;

                                      then

                                       A931: x in ( LSeg (g,m)) by XBOOLE_0:def 4;

                                      x in ( LSeg (g,n)) by A930, XBOOLE_0:def 4;

                                      then

                                       A932: ex qx be Point of ( TOP-REAL 2) st qx = x & (qx `2 ) = (ppi `2 ) & (qq `1 ) <= (qx `1 ) & (qx `1 ) <= (ppi `1 ) by A895, A928;

                                      

                                       A933: m1 in ( dom g2) by A919, A920, SEQ_4: 134;

                                      then

                                       A934: (q1 `2 ) = (ppi `2 ) by A717;

                                      

                                       A935: (m1 + 1) in ( dom g2) by A919, A920, SEQ_4: 134;

                                      then

                                       A936: (q2 `2 ) = (ppi `2 ) by A717;

                                      m1 < (m1 + 1) by NAT_1: 13;

                                      then

                                       A937: (q2 `1 ) < (q1 `1 ) by A729, A933, A935;

                                      ( LSeg (g2,m1)) = ( LSeg (q2,q1)) by A919, A920, TOPREAL1:def 3

                                      .= q1l by A934, A936, A937, A929, TOPREAL3: 10;

                                      then

                                       A938: ex qy be Point of ( TOP-REAL 2) st qy = x & (qy `2 ) = (ppi `2 ) & (q2 `1 ) <= (qy `1 ) & (qy `1 ) <= (q1 `1 ) by A921, A931;

                                      m1 > (n1 + 1) & (n1 + 1) >= 1 by A876, A926, NAT_1: 11, XREAL_1: 9;

                                      then m1 > 1 by XXREAL_0: 2;

                                      then (q1 `1 ) < (qq `1 ) by A729, A883, A933;

                                      hence contradiction by A932, A938, XXREAL_0: 2;

                                    end;

                                    hence thesis;

                                  end;

                                    suppose n <> ( len g1);

                                    then ( len g1) < n by A925, XXREAL_0: 1;

                                    then

                                     A939: ( LSeg (g,n)) = ( LSeg (g2,n1)) by A890, A927, GOBOARD2: 5;

                                    m1 > (n1 + 1) by A876, A926, XREAL_1: 9;

                                    hence thesis by A755, A921, A939;

                                  end;

                                end;

                                hence thesis;

                              end;

                            end;

                            hence thesis;

                          end;

                        end;

                        hence thesis;

                      end;

                    end;

                    hence thesis;

                  end;

                  hence g is s.n.c. by GOBOARD2: 1;

                  now

                    set p = (g1 /. ( len g1)), q = (g2 /. 1);

                    (j1 + 1) <= i1 by A699, NAT_1: 13;

                    then 1 <= l by XREAL_1: 19;

                    then 1 in ( dom g2) by A712, FINSEQ_1: 1;

                    then (q `2 ) = (ppi `2 ) by A717;

                    hence (p `1 ) = (q `1 ) or (p `2 ) = (q `2 ) by A27, A14, A51, A46, A29, FINSEQ_4: 71;

                  end;

                  hence g is special by A43, A726, GOBOARD2: 8;

                  thus ( L~ g) = ( L~ f)

                  proof

                    set lg = { ( LSeg (g,i)) : 1 <= i & (i + 1) <= ( len g) }, lf = { ( LSeg (f,j)) : 1 <= j & (j + 1) <= ( len f) };

                    

                     A940: ( len g) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

                     A941:

                    now

                      let j;

                      assume that

                       A942: ( len g1) <= j and

                       A943: j <= ( len g);

                      reconsider w = (j - ( len g1)) as Element of NAT by A942, INT_1: 5;

                      let p such that

                       A944: p = (g /. j);

                      per cases ;

                        suppose

                         A945: j = ( len g1);

                        1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                        then ( len g1) in ( dom g1) by FINSEQ_3: 25;

                        

                        then

                         A946: (g /. ( len g1)) = (f1 /. ( len f1)) by A46, FINSEQ_4: 68

                        .= (G * (i1,i2)) by A27, A14, A51, A29, FINSEQ_4: 71;

                        hence (p `2 ) = ((G * (i1,i2)) `2 ) by A944, A945;

                        thus ((G * (j1,i2)) `1 ) <= (p `1 ) & (p `1 ) <= ((G * (i1,i2)) `1 ) by A66, A23, A18, A69, A63, A64, A59, A699, A701, A703, A944, A945, A946, SEQM_3:def 1;

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

                        hence p in ( rng c1) by A66, A18, A59, A700, A944, A945, A946, PARTFUN2: 2;

                      end;

                        suppose j <> ( len g1);

                        then ( len g1) < j by A942, XXREAL_0: 1;

                        then (( len g1) + 1) <= j by NAT_1: 13;

                        then

                         A947: 1 <= w by XREAL_1: 19;

                        

                         A948: w <= ( len g2) by A940, A943, XREAL_1: 20;

                        then

                         A949: w in ( dom g2) by A947, FINSEQ_3: 25;

                        j = (w + ( len g1));

                        then (g /. j) = (g2 /. w) by A947, A948, SEQ_4: 136;

                        hence (p `2 ) = (ppi `2 ) & (pj `1 ) <= (p `1 ) & (p `1 ) <= (ppi `1 ) & p in ( rng c1) by A717, A944, A949;

                      end;

                    end;

                    thus ( L~ g) c= ( L~ f)

                    proof

                      let x be object;

                      assume x in ( L~ g);

                      then

                      consider X be set such that

                       A950: x in X and

                       A951: X in lg by TARSKI:def 4;

                      consider i such that

                       A952: X = ( LSeg (g,i)) and

                       A953: 1 <= i and

                       A954: (i + 1) <= ( len g) by A951;

                      per cases ;

                        suppose

                         A955: (i + 1) <= ( len g1);

                        i <= (i + 1) by NAT_1: 11;

                        then i <= ( len g1) by A955, XXREAL_0: 2;

                        then

                         A956: i in ( dom g1) by A953, FINSEQ_3: 25;

                        1 <= (i + 1) by NAT_1: 11;

                        then (i + 1) in ( dom g1) by A955, FINSEQ_3: 25;

                        then X = ( LSeg (g1,i)) by A952, A956, TOPREAL3: 18;

                        then X in { ( LSeg (g1,j)) : 1 <= j & (j + 1) <= ( len g1) } by A953, A955;

                        then

                         A957: x in ( L~ f1) by A44, A950, TARSKI:def 4;

                        ( L~ f1) c= ( L~ f) by TOPREAL3: 20;

                        hence thesis by A957;

                      end;

                        suppose

                         A958: (i + 1) > ( len g1);

                        reconsider q1 = (g /. i), q2 = (g /. (i + 1)) as Point of ( TOP-REAL 2);

                        

                         A959: i <= ( len g) by A954, NAT_1: 13;

                        

                         A960: ( len g1) <= i by A958, NAT_1: 13;

                        then

                         A961: (q1 `2 ) = (ppi `2 ) by A941, A959;

                        

                         A962: (q1 `1 ) <= (ppi `1 ) by A941, A960, A959;

                        

                         A963: (pj `1 ) <= (q1 `1 ) by A941, A960, A959;

                        (q2 `2 ) = (ppi `2 ) by A941, A954, A958;

                        then

                         A964: q2 = |[(q2 `1 ), (q1 `2 )]| by A961, EUCLID: 53;

                        

                         A965: (q2 `1 ) <= (ppi `1 ) by A941, A954, A958;

                        

                         A966: q1 = |[(q1 `1 ), (q1 `2 )]| & ( LSeg (g,i)) = ( LSeg (q2,q1)) by A953, A954, EUCLID: 53, TOPREAL1:def 3;

                        

                         A967: (pj `1 ) <= (q2 `1 ) by A941, A954, A958;

                        now

                          per cases by XXREAL_0: 1;

                            suppose (q1 `1 ) > (q2 `1 );

                            then ( LSeg (g,i)) = { p2 : (p2 `2 ) = (q1 `2 ) & (q2 `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q1 `1 ) } by A964, A966, TOPREAL3: 10;

                            then

                            consider p2 such that

                             A968: p2 = x & (p2 `2 ) = (q1 `2 ) and

                             A969: (q2 `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q1 `1 ) by A950, A952;

                            (pj `1 ) <= (p2 `1 ) & (p2 `1 ) <= (ppi `1 ) by A962, A967, A969, XXREAL_0: 2;

                            then

                             A970: x in ( LSeg (f,k)) by A774, A961, A968;

                            ( LSeg (f,k)) in lf by A3, A24;

                            hence thesis by A970, TARSKI:def 4;

                          end;

                            suppose (q1 `1 ) = (q2 `1 );

                            then ( LSeg (g,i)) = {q1} by A964, A966, RLTOPSP1: 70;

                            then x = q1 by A950, A952, TARSKI:def 1;

                            then

                             A971: x in ( LSeg (f,k)) by A774, A961, A963, A962;

                            ( LSeg (f,k)) in lf by A3, A24;

                            hence thesis by A971, TARSKI:def 4;

                          end;

                            suppose (q1 `1 ) < (q2 `1 );

                            then ( LSeg (g,i)) = { p1 : (p1 `2 ) = (q1 `2 ) & (q1 `1 ) <= (p1 `1 ) & (p1 `1 ) <= (q2 `1 ) } by A964, A966, TOPREAL3: 10;

                            then

                            consider p2 such that

                             A972: p2 = x & (p2 `2 ) = (q1 `2 ) and

                             A973: (q1 `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q2 `1 ) by A950, A952;

                            (pj `1 ) <= (p2 `1 ) & (p2 `1 ) <= (ppi `1 ) by A963, A965, A973, XXREAL_0: 2;

                            then

                             A974: x in ( LSeg (f,k)) by A774, A961, A972;

                            ( LSeg (f,k)) in lf by A3, A24;

                            hence thesis by A974, TARSKI:def 4;

                          end;

                        end;

                        hence thesis;

                      end;

                    end;

                    let x be object;

                    assume x in ( L~ f);

                    then

                     A975: x in (( L~ f1) \/ ( LSeg (f,k))) by A3, A13, GOBOARD2: 3;

                    per cases by A975, XBOOLE_0:def 3;

                      suppose

                       A976: x in ( L~ f1);

                      ( L~ g1) c= ( L~ g) by GOBOARD2: 6;

                      hence thesis by A44, A976;

                    end;

                      suppose x in ( LSeg (f,k));

                      then

                      consider p1 such that

                       A977: p1 = x and

                       A978: (p1 `2 ) = (ppi `2 ) and

                       A979: (pj `1 ) <= (p1 `1 ) and

                       A980: (p1 `1 ) <= (ppi `1 ) by A774;

                      defpred P2[ Nat] means ( len g1) <= $1 & $1 <= ( len g) & for q st q = (g /. $1) holds (q `1 ) >= (p1 `1 );

                       A981:

                      now

                        reconsider n = ( len g1) as Nat;

                        take n;

                        thus P2[n]

                        proof

                          thus ( len g1) <= n & n <= ( len g) by A940, XREAL_1: 31;

                          1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                          then

                           A982: ( len g1) in ( dom g1) by FINSEQ_3: 25;

                          let q;

                          assume q = (g /. n);

                          

                          then q = (f1 /. ( len f1)) by A46, A982, FINSEQ_4: 68

                          .= (G * (i1,i2)) by A27, A14, A51, A29, FINSEQ_4: 71;

                          hence thesis by A980;

                        end;

                      end;

                      

                       A983: for n be Nat holds P2[n] implies n <= ( len g);

                      consider ma be Nat such that

                       A984: P2[ma] & for n be Nat st P2[n] holds n <= ma from NAT_1:sch 6( A983, A981);

                      reconsider ma as Nat;

                      now

                        per cases ;

                          suppose

                           A985: ma = ( len g);

                          (j1 + 1) <= i1 by A699, NAT_1: 13;

                          then

                           A986: 1 <= l by XREAL_1: 19;

                          then (( len g1) + 1) <= ma by A711, A940, A985, XREAL_1: 7;

                          then

                           A987: ( len g1) <= (ma - 1) by XREAL_1: 19;

                          then ( 0 + 1) <= ma by XREAL_1: 19;

                          then

                          reconsider m1 = (ma - 1) as Element of NAT by INT_1: 5;

                          reconsider q = (g /. m1) as Point of ( TOP-REAL 2);

                          

                           A988: (ma - 1) <= ( len g) by A985, XREAL_1: 43;

                          then

                           A989: (q `2 ) = (ppi `2 ) by A941, A987;

                          

                           A990: (pj `1 ) <= (q `1 ) by A941, A988, A987;

                          set lq = { e where e be Point of ( TOP-REAL 2) : (e `2 ) = (ppi `2 ) & (pj `1 ) <= (e `1 ) & (e `1 ) <= (q `1 ) };

                          

                           A991: (i1 - l) = j1;

                          

                           A992: l in ( dom g2) by A711, A986, FINSEQ_3: 25;

                          

                          then

                           A993: (g /. ma) = (g2 /. l) by A711, A940, A985, FINSEQ_4: 69

                          .= pj by A711, A712, A992, A991;

                          then (p1 `1 ) <= (pj `1 ) by A984;

                          then

                           A994: (p1 `1 ) = (pj `1 ) by A979, XXREAL_0: 1;

                          1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                          then

                           A995: 1 <= m1 by A987, XXREAL_0: 2;

                          

                           A996: (m1 + 1) = ma;

                          then q = |[(q `1 ), (q `2 )]| & ( LSeg (g,m1)) = ( LSeg (pj,q)) by A985, A993, A995, EUCLID: 53, TOPREAL1:def 3;

                          then ( LSeg (g,m1)) = lq by A767, A773, A989, A990, TOPREAL3: 10;

                          then

                           A997: p1 in ( LSeg (g,m1)) by A978, A994, A990;

                          ( LSeg (g,m1)) in lg by A985, A995, A996;

                          hence thesis by A977, A997, TARSKI:def 4;

                        end;

                          suppose ma <> ( len g);

                          then ma < ( len g) by A984, XXREAL_0: 1;

                          then

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

                          reconsider qa = (g /. ma), qa1 = (g /. (ma + 1)) as Point of ( TOP-REAL 2);

                          set lma = { p2 : (p2 `2 ) = (ppi `2 ) & (qa1 `1 ) <= (p2 `1 ) & (p2 `1 ) <= (qa `1 ) };

                          

                           A999: qa1 = |[(qa1 `1 ), (qa1 `2 )]| by EUCLID: 53;

                          

                           A1000: (p1 `1 ) <= (qa `1 ) by A984;

                          

                           A1001: ( len g1) <= (ma + 1) by A984, NAT_1: 13;

                          then

                           A1002: (qa1 `2 ) = (ppi `2 ) by A941, A998;

                           A1003:

                          now

                            assume (p1 `1 ) <= (qa1 `1 );

                            then for q holds q = (g /. (ma + 1)) implies (p1 `1 ) <= (q `1 );

                            then (ma + 1) <= ma by A984, A998, A1001;

                            hence contradiction by XREAL_1: 29;

                          end;

                          

                           A1004: (qa `2 ) = (ppi `2 ) & qa = |[(qa `1 ), (qa `2 )]| by A941, A984, EUCLID: 53;

                          

                           A1005: 1 <= ma by A24, A14, A47, A984, NAT_1: 13;

                          

                          then ( LSeg (g,ma)) = ( LSeg (qa1,qa)) by A998, TOPREAL1:def 3

                          .= lma by A1000, A1003, A1002, A1004, A999, TOPREAL3: 10, XXREAL_0: 2;

                          then

                           A1006: x in ( LSeg (g,ma)) by A977, A978, A1000, A1003;

                          ( LSeg (g,ma)) in lg by A998, A1005;

                          hence thesis by A1006, TARSKI:def 4;

                        end;

                      end;

                      hence thesis;

                    end;

                  end;

                  

                   A1007: ( len g) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

                  1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                  then 1 in ( dom g1) by FINSEQ_3: 25;

                  

                  hence (g /. 1) = (f1 /. 1) by A45, FINSEQ_4: 68

                  .= (f /. 1) by A27, A25, FINSEQ_4: 71;

                  (j1 + 1) <= i1 by A699, NAT_1: 13;

                  then

                   A1008: 1 <= l by XREAL_1: 19;

                  then

                   A1009: l in ( dom g2) by A712, FINSEQ_1: 1;

                  

                  hence (g /. ( len g)) = (g2 /. l) by A711, A1007, FINSEQ_4: 69

                  .= (G * (m1,i2)) by A711, A712, A1009

                  .= (f /. ( len f)) by A3, A21, A698;

                  thus ( len f) <= ( len g) by A3, A14, A47, A711, A1008, A1007, XREAL_1: 7;

                end;

                  case

                   A1010: i1 = j1;

                  k <> (k + 1);

                  hence contradiction by A5, A27, A29, A19, A21, A698, A1010, PARTFUN2: 10;

                end;

                  case

                   A1011: i1 < j1;

                  (c1 /. i1) = (c1 . i1) by A66, A60, PARTFUN1:def 6;

                  then

                   A1012: (c1 /. i1) = ppi by A66, MATRIX_0:def 8;

                  then

                   A1013: (x2 . i1) = (ppi `1 ) by A66, A65, A60, GOBOARD1:def 1;

                  (c1 /. j1) = (c1 . j1) by A23, A60, PARTFUN1:def 6;

                  then

                   A1014: (c1 /. j1) = pj by A23, MATRIX_0:def 8;

                  then

                   A1015: (x2 . j1) = (pj `1 ) by A23, A65, A60, GOBOARD1:def 1;

                  then

                   A1016: (ppi `1 ) < (pj `1 ) by A66, A23, A69, A65, A60, A1011, A1013, SEQM_3:def 1;

                  reconsider l = (j1 - i1) as Element of NAT by A1011, INT_1: 5;

                  deffunc F( Nat) = (G * ((i1 + $1),i2));

                  consider g2 such that

                   A1017: ( len g2) = l & for n be Nat st n in ( dom g2) holds (g2 /. n) = F(n) from FINSEQ_4:sch 2;

                  take g = (g1 ^ g2);

                   A1018:

                  now

                    let n;

                    

                     A1019: n <= (i1 + n) by NAT_1: 11;

                    assume

                     A1020: n in ( Seg l);

                    then n <= l by FINSEQ_1: 1;

                    then

                     A1021: (i1 + n) <= (l + i1) by XREAL_1: 7;

                    j1 <= ( len G) by A23, FINSEQ_3: 25;

                    then

                     A1022: (i1 + n) <= ( len G) by A1021, XXREAL_0: 2;

                    1 <= n by A1020, FINSEQ_1: 1;

                    then 1 <= (i1 + n) by A1019, XXREAL_0: 2;

                    hence (i1 + n) in ( dom G) by A1022, FINSEQ_3: 25;

                    hence [(i1 + n), i2] in ( Indices G) by A22, A68, ZFMISC_1: 87;

                  end;

                  

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

                  now

                    let n such that

                     A1024: n in ( dom g2);

                    take m = (i1 + n), k = i2;

                    thus [m, k] in ( Indices G) & (g2 /. n) = (G * (m,k)) by A1017, A1018, A1023, A1024;

                  end;

                  then

                   A1025: for n st n in ( dom g) holds ex i, j st [i, j] in ( Indices G) & (g /. n) = (G * (i,j)) by A75, GOBOARD1: 23;

                  

                   A1026: (y2 . i1) = (ppi `2 ) by A66, A63, A64, A65, A61, A60, A1012, GOBOARD1:def 2;

                   A1027:

                  now

                    let n, p;

                    assume that

                     A1028: n in ( dom g2) and

                     A1029: (g2 /. n) = p;

                    

                     A1030: (g2 /. n) = (G * ((i1 + n),i2)) by A1017, A1028;

                    set n1 = (i1 + n);

                    set pn = (G * (n1,i2));

                    

                     A1031: (i1 + n) in ( dom G) by A1017, A1018, A1023, A1028;

                    then

                     A1032: (y2 . n1) = (y2 . i1) by A66, A70, A63, A64, A65, A61, A60, SEQM_3:def 10;

                    (c1 /. n1) = (c1 . n1) by A60, A1017, A1018, A1023, A1028, PARTFUN1:def 6;

                    then

                     A1033: (c1 /. n1) = pn by A1031, MATRIX_0:def 8;

                    then

                     A1034: (x2 . n1) = (pn `1 ) by A65, A60, A1031, GOBOARD1:def 1;

                    n <= ( len g2) by A1028, FINSEQ_3: 25;

                    then

                     A1035: n1 <= (i1 + ( len g2)) by XREAL_1: 7;

                    (y2 . n1) = (pn `2 ) by A63, A64, A65, A61, A60, A1031, A1033, GOBOARD1:def 2;

                    hence (p `2 ) = (ppi `2 ) & (ppi `1 ) <= (p `1 ) & (p `1 ) <= (pj `1 ) by A66, A23, A69, A65, A60, A1017, A1026, A1013, A1015, A1029, A1030, A1031, A1035, A1032, A1034, SEQ_4: 137, XREAL_1: 31;

                    thus p in ( rng c1) by A60, A1029, A1030, A1031, A1033, PARTFUN2: 2;

                    1 <= n by A1028, FINSEQ_3: 25;

                    then i1 < n1 by XREAL_1: 29;

                    hence (p `1 ) > (ppi `1 ) by A66, A69, A65, A60, A1013, A1029, A1030, A1031, A1034, SEQM_3:def 1;

                  end;

                  

                   A1036: g2 is special

                  proof

                    let n be Nat;

                    set p = (g2 /. n);

                    assume

                     A1037: 1 <= n & (n + 1) <= ( len g2);

                    then n in ( dom g2) by SEQ_4: 134;

                    then

                     A1038: (p `2 ) = (ppi `2 ) by A1027;

                    (n + 1) in ( dom g2) by A1037, SEQ_4: 134;

                    hence thesis by A1027, A1038;

                  end;

                  now

                    let n,m be Element of NAT ;

                    assume that

                     A1039: n in ( dom g2) & m in ( dom g2) and

                     A1040: n <> m;

                    

                     A1041: (g2 /. n) = (G * ((i1 + n),i2)) & (g2 /. m) = (G * ((i1 + m),i2)) by A1017, A1039;

                    assume

                     A1042: (g2 /. n) = (g2 /. m);

                     [(i1 + n), i2] in ( Indices G) & [(i1 + m), i2] in ( Indices G) by A1017, A1018, A1023, A1039;

                    then (i1 + n) = (i1 + m) by A1041, A1042, GOBOARD1: 5;

                    hence contradiction by A1040;

                  end;

                  then for n,m be Element of NAT st n in ( dom g2) & m in ( dom g2) & (g2 /. n) = (g2 /. m) holds n = m;

                  then

                   A1043: g2 is one-to-one by PARTFUN2: 9;

                  set lk = { w where w be Point of ( TOP-REAL 2) : (w `2 ) = (ppi `2 ) & (ppi `1 ) <= (w `1 ) & (w `1 ) <= (pj `1 ) };

                  

                   A1044: ppi = |[(ppi `1 ), (ppi `2 )]| by EUCLID: 53;

                   A1045:

                  now

                    let n, m, p, q;

                    assume that

                     A1046: n in ( dom g2) and

                     A1047: m in ( dom g2) and

                     A1048: n < m and

                     A1049: (g2 /. n) = p & (g2 /. m) = q;

                    

                     A1050: (i1 + n) in ( dom G) by A1017, A1018, A1023, A1046;

                    set n1 = (i1 + n), m1 = (i1 + m);

                    set pn = (G * (n1,i2)), pm = (G * (m1,i2));

                    

                     A1051: n1 < m1 by A1048, XREAL_1: 8;

                    (c1 /. n1) = (c1 . n1) by A60, A1017, A1018, A1023, A1046, PARTFUN1:def 6;

                    then (c1 /. n1) = pn by A1050, MATRIX_0:def 8;

                    then

                     A1052: (x2 . n1) = (pn `1 ) by A65, A60, A1050, GOBOARD1:def 1;

                    

                     A1053: (i1 + m) in ( dom G) by A1017, A1018, A1023, A1047;

                    (c1 /. m1) = (c1 . m1) by A60, A1017, A1018, A1023, A1047, PARTFUN1:def 6;

                    then (c1 /. m1) = pm by A1053, MATRIX_0:def 8;

                    then

                     A1054: (x2 . m1) = (pm `1 ) by A65, A60, A1053, GOBOARD1:def 1;

                    (g2 /. n) = (G * ((i1 + n),i2)) & (g2 /. m) = (G * ((i1 + m),i2)) by A1017, A1046, A1047;

                    hence (p `1 ) < (q `1 ) by A69, A65, A60, A1049, A1050, A1053, A1051, A1052, A1054, SEQM_3:def 1;

                  end;

                  for n, m st m > (n + 1) & n in ( dom g2) & (n + 1) in ( dom g2) & m in ( dom g2) & (m + 1) in ( dom g2) holds ( LSeg (g2,n)) misses ( LSeg (g2,m))

                  proof

                    let n, m;

                    assume that

                     A1055: m > (n + 1) and

                     A1056: n in ( dom g2) and

                     A1057: (n + 1) in ( dom g2) and

                     A1058: m in ( dom g2) and

                     A1059: (m + 1) in ( dom g2) and

                     A1060: (( LSeg (g2,n)) /\ ( LSeg (g2,m))) <> {} ;

                    reconsider p1 = (g2 /. n), p2 = (g2 /. (n + 1)), q1 = (g2 /. m), q2 = (g2 /. (m + 1)) as Point of ( TOP-REAL 2);

                    

                     A1061: (p1 `2 ) = (ppi `2 ) & (p2 `2 ) = (ppi `2 ) by A1027, A1056, A1057;

                    n < (n + 1) by NAT_1: 13;

                    then

                     A1062: (p1 `1 ) < (p2 `1 ) by A1045, A1056, A1057;

                    set lp = { w where w be Point of ( TOP-REAL 2) : (w `2 ) = (ppi `2 ) & (p1 `1 ) <= (w `1 ) & (w `1 ) <= (p2 `1 ) }, lq = { w where w be Point of ( TOP-REAL 2) : (w `2 ) = (ppi `2 ) & (q1 `1 ) <= (w `1 ) & (w `1 ) <= (q2 `1 ) };

                    

                     A1063: p1 = |[(p1 `1 ), (p1 `2 )]| & p2 = |[(p2 `1 ), (p2 `2 )]| by EUCLID: 53;

                    m < (m + 1) by NAT_1: 13;

                    then

                     A1064: (q1 `1 ) < (q2 `1 ) by A1045, A1058, A1059;

                    

                     A1065: q1 = |[(q1 `1 ), (q1 `2 )]| & q2 = |[(q2 `1 ), (q2 `2 )]| by EUCLID: 53;

                    set x = the Element of (( LSeg (g2,n)) /\ ( LSeg (g2,m)));

                    

                     A1066: x in ( LSeg (g2,n)) by A1060, XBOOLE_0:def 4;

                    

                     A1067: (q1 `2 ) = (ppi `2 ) & (q2 `2 ) = (ppi `2 ) by A1027, A1058, A1059;

                    

                     A1068: x in ( LSeg (g2,m)) by A1060, XBOOLE_0:def 4;

                    1 <= m & (m + 1) <= ( len g2) by A1058, A1059, FINSEQ_3: 25;

                    

                    then ( LSeg (g2,m)) = ( LSeg (q1,q2)) by TOPREAL1:def 3

                    .= lq by A1064, A1067, A1065, TOPREAL3: 10;

                    then

                     A1069: ex tm be Point of ( TOP-REAL 2) st tm = x & (tm `2 ) = (ppi `2 ) & (q1 `1 ) <= (tm `1 ) & (tm `1 ) <= (q2 `1 ) by A1068;

                    1 <= n & (n + 1) <= ( len g2) by A1056, A1057, FINSEQ_3: 25;

                    

                    then ( LSeg (g2,n)) = ( LSeg (p1,p2)) by TOPREAL1:def 3

                    .= lp by A1062, A1061, A1063, TOPREAL3: 10;

                    then

                     A1070: ex tn be Point of ( TOP-REAL 2) st tn = x & (tn `2 ) = (ppi `2 ) & (p1 `1 ) <= (tn `1 ) & (tn `1 ) <= (p2 `1 ) by A1066;

                    (p2 `1 ) < (q1 `1 ) by A1045, A1055, A1057, A1058;

                    hence contradiction by A1070, A1069, XXREAL_0: 2;

                  end;

                  then

                   A1071: g2 is s.n.c. by GOBOARD2: 1;

                  

                   A1072: not (f /. k) in ( L~ g2)

                  proof

                    set ls = { ( LSeg (g2,m)) : 1 <= m & (m + 1) <= ( len g2) };

                    assume (f /. k) in ( L~ g2);

                    then

                    consider X be set such that

                     A1073: (f /. k) in X and

                     A1074: X in ls by TARSKI:def 4;

                    consider m such that

                     A1075: X = ( LSeg (g2,m)) and

                     A1076: 1 <= m & (m + 1) <= ( len g2) by A1074;

                    reconsider q1 = (g2 /. m), q2 = (g2 /. (m + 1)) as Point of ( TOP-REAL 2);

                    

                     A1077: m in ( dom g2) by A1076, SEQ_4: 134;

                    then

                     A1078: (q1 `2 ) = (ppi `2 ) by A1027;

                    set lq = { w where w be Point of ( TOP-REAL 2) : (w `2 ) = (ppi `2 ) & (q1 `1 ) <= (w `1 ) & (w `1 ) <= (q2 `1 ) };

                    

                     A1079: q1 = |[(q1 `1 ), (q1 `2 )]| & q2 = |[(q2 `1 ), (q2 `2 )]| by EUCLID: 53;

                    

                     A1080: (m + 1) in ( dom g2) by A1076, SEQ_4: 134;

                    then

                     A1081: (q2 `2 ) = (ppi `2 ) by A1027;

                    m < (m + 1) by NAT_1: 13;

                    then

                     A1082: (q1 `1 ) < (q2 `1 ) by A1045, A1077, A1080;

                    ( LSeg (g2,m)) = ( LSeg (q1,q2)) by A1076, TOPREAL1:def 3

                    .= lq by A1078, A1081, A1082, A1079, TOPREAL3: 10;

                    then ex p st p = (f /. k) & (p `2 ) = (ppi `2 ) & (q1 `1 ) <= (p `1 ) & (p `1 ) <= (q2 `1 ) by A1073, A1075;

                    hence contradiction by A29, A1027, A1077;

                  end;

                  (y2 . j1) = (pj `2 ) by A23, A63, A64, A65, A61, A60, A1014, GOBOARD1:def 2;

                  then

                   A1083: (ppi `2 ) = (pj `2 ) by A66, A23, A70, A63, A64, A65, A61, A60, A1026, SEQM_3:def 10;

                   A1084:

                  now

                    let n;

                    assume that

                     A1085: n in ( dom g2) and

                     A1086: (n + 1) in ( dom g2);

                    let l1,l2,l3,l4 be Nat;

                    assume that

                     A1087: [l1, l2] in ( Indices G) and

                     A1088: [l3, l4] in ( Indices G) and

                     A1089: (g2 /. n) = (G * (l1,l2)) and

                     A1090: (g2 /. (n + 1)) = (G * (l3,l4));

                    (g2 /. (n + 1)) = (G * ((i1 + (n + 1)),i2)) & [(i1 + (n + 1)), i2] in ( Indices G) by A1017, A1018, A1023, A1086;

                    then

                     A1091: l3 = (i1 + (n + 1)) & l4 = i2 by A1088, A1090, GOBOARD1: 5;

                    (g2 /. n) = (G * ((i1 + n),i2)) & [(i1 + n), i2] in ( Indices G) by A1017, A1018, A1023, A1085;

                    then l1 = (i1 + n) & l2 = i2 by A1087, A1089, GOBOARD1: 5;

                    

                    hence ( |.(l1 - l3).| + |.(l2 - l4).|) = ( |.((i1 + n) - (i1 + (n + 1))).| + 0 ) by A1091, ABSVALUE: 2

                    .= |.( - 1).|

                    .= |.1.| by COMPLEX1: 52

                    .= 1 by ABSVALUE:def 1;

                  end;

                  now

                    let l1,l2,l3,l4 be Nat;

                    assume that

                     A1092: [l1, l2] in ( Indices G) and

                     A1093: [l3, l4] in ( Indices G) and

                     A1094: (g1 /. ( len g1)) = (G * (l1,l2)) and

                     A1095: (g2 /. 1) = (G * (l3,l4)) and ( len g1) in ( dom g1) and

                     A1096: 1 in ( dom g2);

                    (g2 /. 1) = (G * ((i1 + 1),i2)) & [(i1 + 1), i2] in ( Indices G) by A1017, A1018, A1023, A1096;

                    then

                     A1097: l3 = (i1 + 1) & l4 = i2 by A1093, A1095, GOBOARD1: 5;

                    (f1 /. ( len f1)) = (f /. k) by A27, A14, A51, FINSEQ_4: 71;

                    then l1 = i1 & l2 = i2 by A46, A28, A29, A1092, A1094, GOBOARD1: 5;

                    

                    hence ( |.(l1 - l3).| + |.(l2 - l4).|) = ( |.(i1 - (i1 + 1)).| + 0 ) by A1097, ABSVALUE: 2

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

                    .= |.1.| by COMPLEX1: 52

                    .= 1 by ABSVALUE:def 1;

                  end;

                  then for n st n in ( dom g) & (n + 1) in ( dom g) holds for m, k, i, j st [m, k] in ( Indices G) & [i, j] in ( Indices G) & (g /. n) = (G * (m,k)) & (g /. (n + 1)) = (G * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1 by A48, A1084, GOBOARD1: 24;

                  hence g is_sequence_on G by A1025, GOBOARD1:def 9;

                  

                   A1098: pj = |[(pj `1 ), (pj `2 )]| by EUCLID: 53;

                  

                   A1099: ( LSeg (f,k)) = ( LSeg (ppi,pj)) by A3, A24, A29, A21, A698, TOPREAL1:def 3

                  .= lk by A1016, A1083, A1044, A1098, TOPREAL3: 10;

                  

                   A1100: ( rng g2) c= ( LSeg (f,k))

                  proof

                    let x be object;

                    assume x in ( rng g2);

                    then

                    consider n be Element of NAT such that

                     A1101: n in ( dom g2) and

                     A1102: (g2 /. n) = x by PARTFUN2: 2;

                    set pn = (G * ((i1 + n),i2));

                    

                     A1103: (g2 /. n) = (G * ((i1 + n),i2)) by A1017, A1101;

                    then

                     A1104: (pn `1 ) <= (pj `1 ) by A1027, A1101;

                    (pn `2 ) = (ppi `2 ) & (ppi `1 ) <= (pn `1 ) by A1027, A1101, A1103;

                    hence thesis by A1099, A1102, A1103, A1104;

                  end;

                  

                   A1105: ( Seg l) = ( dom g2) by A1017, FINSEQ_1:def 3;

                  

                   A1106: not (f /. k) in ( rng g2)

                  proof

                    assume (f /. k) in ( rng g2);

                    then

                    consider n be Element of NAT such that

                     A1107: n in ( dom g2) and

                     A1108: (g2 /. n) = (f /. k) by PARTFUN2: 2;

                    (g2 /. n) = (G * ((i1 + n),i2)) & [(i1 + n), i2] in ( Indices G) by A1017, A1105, A1018, A1107;

                    then

                     A1109: (i1 + n) = i1 by A28, A29, A1108, GOBOARD1: 5;

                     0 < n by A1107, FINSEQ_3: 25;

                    hence contradiction by A1109;

                  end;

                  (( rng g1) /\ ( rng g2)) = {}

                  proof

                    set x = the Element of (( rng g1) /\ ( rng g2));

                    assume

                     A1110: not thesis;

                    then

                     A1111: x in ( rng g2) by XBOOLE_0:def 4;

                    

                     A1112: x in ( rng g1) by A1110, XBOOLE_0:def 4;

                    now

                      per cases by A24, XXREAL_0: 1;

                        suppose k = 1;

                        hence contradiction by A52, A1106, A1112, A1111, TARSKI:def 1;

                      end;

                        suppose 1 < k;

                        then x in (( L~ f1) /\ ( LSeg (f,k))) & (( L~ f1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, A49, A1100, A1112, A1111, GOBOARD2: 4, XBOOLE_0:def 4;

                        hence contradiction by A1106, A1111, TARSKI:def 1;

                      end;

                    end;

                    hence contradiction;

                  end;

                  then ( rng g1) misses ( rng g2);

                  hence g is one-to-one by A40, A1043, FINSEQ_3: 91;

                  

                   A1113: ( LSeg (f,k)) = ( LSeg (ppi,pj)) by A3, A24, A29, A21, A698, TOPREAL1:def 3;

                  

                   A1114: for n st 1 <= n & (n + 2) <= ( len g2) holds (( LSeg (g2,n)) /\ ( LSeg (g2,(n + 1)))) = {(g2 /. (n + 1))}

                  proof

                    let n;

                    assume that

                     A1115: 1 <= n and

                     A1116: (n + 2) <= ( len g2);

                    

                     A1117: (n + 1) in ( dom g2) by A1115, A1116, SEQ_4: 135;

                    then (g2 /. (n + 1)) in ( rng g2) by PARTFUN2: 2;

                    then (g2 /. (n + 1)) in lk by A1099, A1100;

                    then

                    consider u1 be Point of ( TOP-REAL 2) such that

                     A1118: (g2 /. (n + 1)) = u1 and

                     A1119: (u1 `2 ) = (ppi `2 ) and (ppi `1 ) <= (u1 `1 ) and (u1 `1 ) <= (pj `1 );

                    

                     A1120: (n + 2) in ( dom g2) by A1115, A1116, SEQ_4: 135;

                    then (g2 /. (n + 2)) in ( rng g2) by PARTFUN2: 2;

                    then (g2 /. (n + 2)) in lk by A1099, A1100;

                    then

                    consider u2 be Point of ( TOP-REAL 2) such that

                     A1121: (g2 /. (n + 2)) = u2 and

                     A1122: (u2 `2 ) = (ppi `2 ) and (ppi `1 ) <= (u2 `1 ) and (u2 `1 ) <= (pj `1 );

                    1 <= (n + 1) & ((n + 1) + 1) = (n + (1 + 1)) by NAT_1: 11;

                    then

                     A1123: ( LSeg (g2,(n + 1))) = ( LSeg (u1,u2)) by A1116, A1118, A1121, TOPREAL1:def 3;

                    (n + 1) < ((n + 1) + 1) by NAT_1: 13;

                    then

                     A1124: (u1 `1 ) < (u2 `1 ) by A1045, A1117, A1120, A1118, A1121;

                    

                     A1125: n in ( dom g2) by A1115, A1116, SEQ_4: 135;

                    then (g2 /. n) in ( rng g2) by PARTFUN2: 2;

                    then (g2 /. n) in lk by A1099, A1100;

                    then

                    consider u be Point of ( TOP-REAL 2) such that

                     A1126: (g2 /. n) = u and

                     A1127: (u `2 ) = (ppi `2 ) and (ppi `1 ) <= (u `1 ) and (u `1 ) <= (pj `1 );

                    (n + 1) <= (n + 2) by XREAL_1: 6;

                    then (n + 1) <= ( len g2) by A1116, XXREAL_0: 2;

                    then

                     A1128: ( LSeg (g2,n)) = ( LSeg (u,u1)) by A1115, A1126, A1118, TOPREAL1:def 3;

                    set lg = { w where w be Point of ( TOP-REAL 2) : (w `2 ) = (ppi `2 ) & (u `1 ) <= (w `1 ) & (w `1 ) <= (u2 `1 ) };

                    n < (n + 1) by NAT_1: 13;

                    then

                     A1129: (u `1 ) < (u1 `1 ) by A1045, A1125, A1117, A1126, A1118;

                    then

                     A1130: u1 in lg by A1119, A1124;

                    u = |[(u `1 ), (u `2 )]| & u2 = |[(u2 `1 ), (u2 `2 )]| by EUCLID: 53;

                    then ( LSeg ((g2 /. n),(g2 /. (n + 2)))) = lg by A1126, A1127, A1121, A1122, A1124, A1129, TOPREAL3: 10, XXREAL_0: 2;

                    hence thesis by A1126, A1118, A1121, A1128, A1123, A1130, TOPREAL1: 8;

                  end;

                  thus g is unfolded

                  proof

                    let n be Nat;

                    assume that

                     A1131: 1 <= n and

                     A1132: (n + 2) <= ( len g);

                    

                     A1133: ((n + 1) + 1) <= ( len g) by A1132;

                    (n + 1) <= ((n + 1) + 1) by NAT_1: 11;

                    then

                     A1134: (n + 1) <= ( len g) by A1132, XXREAL_0: 2;

                    

                     A1135: ( len g) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

                    ((n + 2) - ( len g1)) = ((n - ( len g1)) + 2);

                    then

                     A1136: ((n - ( len g1)) + 2) <= ( len g2) by A1132, A1135, XREAL_1: 20;

                    

                     A1137: 1 <= (n + 1) by NAT_1: 11;

                    

                     A1138: n <= (n + 1) by NAT_1: 11;

                    

                     A1139: (n + (1 + 1)) = ((n + 1) + 1);

                    per cases ;

                      suppose

                       A1140: (n + 2) <= ( len g1);

                      

                       A1141: (n + (1 + 1)) = ((n + 1) + 1);

                      

                       A1142: (n + 1) in ( dom g1) by A1131, A1140, SEQ_4: 135;

                      then

                       A1143: (g /. (n + 1)) = (g1 /. (n + 1)) by FINSEQ_4: 68;

                      n in ( dom g1) by A1131, A1140, SEQ_4: 135;

                      then

                       A1144: ( LSeg (g1,n)) = ( LSeg (g,n)) by A1142, TOPREAL3: 18;

                      (n + 2) in ( dom g1) by A1131, A1140, SEQ_4: 135;

                      then ( LSeg (g1,(n + 1))) = ( LSeg (g,(n + 1))) by A1142, A1141, TOPREAL3: 18;

                      hence thesis by A41, A1131, A1140, A1144, A1143;

                    end;

                      suppose ( len g1) < (n + 2);

                      then (( len g1) + 1) <= (n + 2) by NAT_1: 13;

                      then

                       A1145: ( len g1) <= ((n + 2) - 1) by XREAL_1: 19;

                      now

                        per cases ;

                          suppose

                           A1146: ( len g1) = (n + 1);

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

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

                          then

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

                          then (g2 /. 1) in lk by A1099, A1100;

                          then

                          consider u1 be Point of ( TOP-REAL 2) such that

                           A1148: (g2 /. 1) = u1 and (u1 `2 ) = (ppi `2 ) and (ppi `1 ) <= (u1 `1 ) and (u1 `1 ) <= (pj `1 );

                          ppi in ( LSeg (ppi,pj)) by RLTOPSP1: 68;

                          then

                           A1149: ( LSeg (ppi,u1)) c= ( LSeg (f,k)) by A1113, A1100, A1147, A1148, TOPREAL1: 6;

                          1 <= (n + 1) by NAT_1: 11;

                          then

                           A1150: (n + 1) in ( dom g1) by A1146, FINSEQ_3: 25;

                          

                          then

                           A1151: (g /. (n + 1)) = (f1 /. ( len f1)) by A46, A1146, FINSEQ_4: 68

                          .= ppi by A27, A14, A51, A29, FINSEQ_4: 71;

                          now

                            1 < ( len g1) by A1131, A1146, NAT_1: 13;

                            then

                             A1152: (1 + 1) <= ( len g1) by NAT_1: 13;

                            assume k = 1;

                            hence contradiction by A52, A1152, TOPREAL1: 23;

                          end;

                          then 1 < k by A24, XXREAL_0: 1;

                          then

                           A1153: (( L~ f1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, GOBOARD2: 4;

                          

                           A1154: ( LSeg (g1,n)) c= ( L~ f1) by A44, TOPREAL3: 19;

                          n in ( dom g1) by A1131, A1138, A1146, FINSEQ_3: 25;

                          then

                           A1155: ( LSeg (g,n)) = ( LSeg (g1,n)) by A1150, TOPREAL3: 18;

                          (g /. (n + 1)) in ( LSeg (g,n)) & (g /. (n + 1)) in ( LSeg (g,(n + 1))) by A1131, A1132, A1137, A1134, A1139, TOPREAL1: 21;

                          then (g /. (n + 1)) in (( LSeg (g,n)) /\ ( LSeg (g,(n + 1)))) by XBOOLE_0:def 4;

                          then

                           A1156: {(g /. (n + 1))} c= (( LSeg (g,n)) /\ ( LSeg (g,(n + 1)))) by ZFMISC_1: 31;

                          (n + 2) = (1 + ( len g1)) & 1 <= ( len g2) by A1132, A1139, A1135, A1146, XREAL_1: 6;

                          then (g /. (n + 2)) = (g2 /. 1) by SEQ_4: 136;

                          then ( LSeg (g,(n + 1))) = ( LSeg (ppi,u1)) by A1132, A1137, A1139, A1151, A1148, TOPREAL1:def 3;

                          then (( LSeg (g,n)) /\ ( LSeg (g,(n + 1)))) c= {(g /. (n + 1))} by A29, A1154, A1153, A1155, A1151, A1149, XBOOLE_1: 27;

                          hence thesis by A1156;

                        end;

                          suppose ( len g1) <> (n + 1);

                          then ( len g1) < (n + 1) by A1145, XXREAL_0: 1;

                          then

                           A1157: ( len g1) <= n by NAT_1: 13;

                          then

                          reconsider n1 = (n - ( len g1)) as Element of NAT by INT_1: 5;

                          now

                            per cases ;

                              suppose

                               A1158: ( len g1) = n;

                              then

                               A1159: 2 <= ( len g2) by A1132, A1135, XREAL_1: 6;

                              then 1 <= ( len g2) by XXREAL_0: 2;

                              then

                               A1160: (g /. (n + 1)) = (g2 /. 1) by A1158, SEQ_4: 136;

                              1 <= ( len g2) by A1159, XXREAL_0: 2;

                              then

                               A1161: 1 in ( dom g2) by FINSEQ_3: 25;

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

                              then (g2 /. 1) in lk by A1099, A1100;

                              then

                              consider u1 be Point of ( TOP-REAL 2) such that

                               A1162: (g2 /. 1) = u1 and

                               A1163: (u1 `2 ) = (ppi `2 ) & (ppi `1 ) <= (u1 `1 ) and (u1 `1 ) <= (pj `1 );

                              1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                              then ( len g1) in ( dom g1) by FINSEQ_3: 25;

                              

                              then (g /. n) = (f1 /. ( len f1)) by A46, A1158, FINSEQ_4: 68

                              .= ppi by A27, A14, A51, A29, FINSEQ_4: 71;

                              then

                               A1164: ( LSeg (g,n)) = ( LSeg (ppi,u1)) by A1131, A1134, A1160, A1162, TOPREAL1:def 3;

                              

                               A1165: 2 in ( dom g2) by A1159, FINSEQ_3: 25;

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

                              then (g2 /. 2) in lk by A1099, A1100;

                              then

                              consider u2 be Point of ( TOP-REAL 2) such that

                               A1166: (g2 /. 2) = u2 and

                               A1167: (u2 `2 ) = (ppi `2 ) & (ppi `1 ) <= (u2 `1 ) and (u2 `1 ) <= (pj `1 );

                              set lg = { w where w be Point of ( TOP-REAL 2) : (w `2 ) = (ppi `2 ) & (ppi `1 ) <= (w `1 ) & (w `1 ) <= (u2 `1 ) };

                              (u1 `1 ) < (u2 `1 ) by A1045, A1161, A1165, A1162, A1166;

                              then u2 = |[(u2 `1 ), (u2 `2 )]| & u1 in lg by A1163, EUCLID: 53;

                              then

                               A1168: u1 in ( LSeg (ppi,u2)) by A1044, A1167, TOPREAL3: 10;

                              (g /. (n + 2)) = (g2 /. 2) by A1158, A1159, SEQ_4: 136;

                              then ( LSeg (g,(n + 1))) = ( LSeg (u1,u2)) by A1132, A1137, A1139, A1160, A1162, A1166, TOPREAL1:def 3;

                              hence thesis by A1160, A1162, A1164, A1168, TOPREAL1: 8;

                            end;

                              suppose ( len g1) <> n;

                              then

                               A1169: ( len g1) < n by A1157, XXREAL_0: 1;

                              then (( len g1) + 1) <= n by NAT_1: 13;

                              then

                               A1170: 1 <= n1 by XREAL_1: 19;

                              (n1 + ( len g1)) = n;

                              then

                               A1171: ( LSeg (g,n)) = ( LSeg (g2,n1)) by A1134, A1169, GOBOARD2: 5;

                              

                               A1172: (n + 1) = ((n1 + 1) + ( len g1));

                              then (n1 + 1) <= ( len g2) by A1134, A1135, XREAL_1: 6;

                              then

                               A1173: (g /. (n + 1)) = (g2 /. (n1 + 1)) by A1172, NAT_1: 11, SEQ_4: 136;

                              ( len g1) < (n + 1) by A1138, A1169, XXREAL_0: 2;

                              then ( LSeg (g,(n + 1))) = ( LSeg (g2,(n1 + 1))) by A1133, A1172, GOBOARD2: 5;

                              hence thesis by A1114, A1136, A1171, A1173, A1170;

                            end;

                          end;

                          hence thesis;

                        end;

                      end;

                      hence thesis;

                    end;

                  end;

                  

                   A1174: ( L~ g2) c= ( LSeg (f,k))

                  proof

                    let x be object;

                    set ls = { ( LSeg (g2,m)) : 1 <= m & (m + 1) <= ( len g2) };

                    assume x in ( L~ g2);

                    then

                    consider X be set such that

                     A1175: x in X and

                     A1176: X in ls by TARSKI:def 4;

                    consider m such that

                     A1177: X = ( LSeg (g2,m)) and

                     A1178: 1 <= m & (m + 1) <= ( len g2) by A1176;

                    reconsider q1 = (g2 /. m), q2 = (g2 /. (m + 1)) as Point of ( TOP-REAL 2);

                    

                     A1179: ( LSeg (g2,m)) = ( LSeg (q1,q2)) by A1178, TOPREAL1:def 3;

                    (m + 1) in ( dom g2) by A1178, SEQ_4: 134;

                    then

                     A1180: (g2 /. (m + 1)) in ( rng g2) by PARTFUN2: 2;

                    m in ( dom g2) by A1178, SEQ_4: 134;

                    then (g2 /. m) in ( rng g2) by PARTFUN2: 2;

                    then ( LSeg (q1,q2)) c= ( LSeg (ppi,pj)) by A1113, A1100, A1180, TOPREAL1: 6;

                    hence thesis by A1113, A1175, A1177, A1179;

                  end;

                  

                   A1181: (( L~ g1) /\ ( L~ g2)) = {}

                  proof

                    per cases ;

                      suppose k = 1;

                      hence thesis by A52;

                    end;

                      suppose k <> 1;

                      then 1 < k by A24, XXREAL_0: 1;

                      then (( L~ g1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, A44, GOBOARD2: 4;

                      then

                       A1182: (( L~ g1) /\ ( L~ g2)) c= {(f /. k)} by A1174, XBOOLE_1: 26;

                      now

                        set x = the Element of (( L~ g1) /\ ( L~ g2));

                        assume (( L~ g1) /\ ( L~ g2)) <> {} ;

                        then x in {(f /. k)} & x in ( L~ g2) by A1182, XBOOLE_0:def 4;

                        hence contradiction by A1072, TARSKI:def 1;

                      end;

                      hence thesis;

                    end;

                  end;

                  for n, m st m > (n + 1) & n in ( dom g) & (n + 1) in ( dom g) & m in ( dom g) & (m + 1) in ( dom g) holds ( LSeg (g,n)) misses ( LSeg (g,m))

                  proof

                    

                     A1183: 1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                    then ( len g1) in ( dom g1) by FINSEQ_3: 25;

                    

                    then

                     A1184: (g /. ( len g1)) = (g1 /. ( len g1)) by FINSEQ_4: 68

                    .= ppi by A27, A14, A51, A46, A29, FINSEQ_4: 71;

                    reconsider qq = (g2 /. 1) as Point of ( TOP-REAL 2);

                    set l1 = { ( LSeg (g1,i)) : 1 <= i & (i + 1) <= ( len g1) }, l2 = { ( LSeg (g2,j)) : 1 <= j & (j + 1) <= ( len g2) };

                    let n, m;

                    assume that

                     A1185: m > (n + 1) and

                     A1186: n in ( dom g) and

                     A1187: (n + 1) in ( dom g) and

                     A1188: m in ( dom g) and

                     A1189: (m + 1) in ( dom g);

                    

                     A1190: 1 <= n by A1186, FINSEQ_3: 25;

                    (i1 + 1) <= j1 by A1011, NAT_1: 13;

                    then

                     A1191: 1 <= l by XREAL_1: 19;

                    then

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

                    then

                     A1193: (qq `2 ) = (ppi `2 ) & (qq `1 ) > (ppi `1 ) by A1027;

                    

                     A1194: (g /. (( len g1) + 1)) = qq by A1017, A1191, SEQ_4: 136;

                    

                     A1195: (qq `1 ) <= (pj `1 ) by A1027, A1192;

                    

                     A1196: (m + 1) <= ( len g) by A1189, FINSEQ_3: 25;

                    

                     A1197: 1 <= (m + 1) by A1189, FINSEQ_3: 25;

                    

                     A1198: 1 <= (n + 1) by A1187, FINSEQ_3: 25;

                    

                     A1199: (n + 1) <= ( len g) by A1187, FINSEQ_3: 25;

                    

                     A1200: qq = |[(qq `1 ), (qq `2 )]| by EUCLID: 53;

                    

                     A1201: 1 <= m by A1188, FINSEQ_3: 25;

                    set ql = { z where z be Point of ( TOP-REAL 2) : (z `2 ) = (ppi `2 ) & (ppi `1 ) <= (z `1 ) & (z `1 ) <= (qq `1 ) };

                    

                     A1202: n <= (n + 1) by NAT_1: 11;

                    

                     A1203: ( len g) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

                    then (( len g1) + 1) <= ( len g) by A1017, A1191, XREAL_1: 7;

                    

                    then

                     A1204: ( LSeg (g,( len g1))) = ( LSeg (ppi,qq)) by A1183, A1184, A1194, TOPREAL1:def 3

                    .= ql by A1044, A1193, A1200, TOPREAL3: 10;

                    

                     A1205: m <= (m + 1) by NAT_1: 11;

                    then

                     A1206: (n + 1) <= (m + 1) by A1185, XXREAL_0: 2;

                    now

                      per cases ;

                        suppose

                         A1207: (m + 1) <= ( len g1);

                        then m <= ( len g1) by A1205, XXREAL_0: 2;

                        then

                         A1208: m in ( dom g1) by A1201, FINSEQ_3: 25;

                        (m + 1) in ( dom g1) by A1197, A1207, FINSEQ_3: 25;

                        then

                         A1209: ( LSeg (g,m)) = ( LSeg (g1,m)) by A1208, TOPREAL3: 18;

                        

                         A1210: (n + 1) <= ( len g1) by A1206, A1207, XXREAL_0: 2;

                        then n <= ( len g1) by A1202, XXREAL_0: 2;

                        then

                         A1211: n in ( dom g1) by A1190, FINSEQ_3: 25;

                        (n + 1) in ( dom g1) by A1198, A1210, FINSEQ_3: 25;

                        then ( LSeg (g,n)) = ( LSeg (g1,n)) by A1211, TOPREAL3: 18;

                        hence thesis by A42, A1185, A1209;

                      end;

                        suppose ( len g1) < (m + 1);

                        then

                         A1212: ( len g1) <= m by NAT_1: 13;

                        then

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

                        now

                          per cases ;

                            suppose

                             A1213: m = ( len g1);

                            

                             A1214: ( LSeg (g,m)) c= ( LSeg (f,k))

                            proof

                              let x be object;

                              assume x in ( LSeg (g,m));

                              then

                              consider px be Point of ( TOP-REAL 2) such that

                               A1215: px = x & (px `2 ) = (ppi `2 ) & (ppi `1 ) <= (px `1 ) and

                               A1216: (px `1 ) <= (qq `1 ) by A1204, A1213;

                              (pj `1 ) >= (px `1 ) by A1195, A1216, XXREAL_0: 2;

                              hence thesis by A1099, A1215;

                            end;

                            n <= ( len g1) by A1185, A1202, A1213, XXREAL_0: 2;

                            then

                             A1217: n in ( dom g1) by A1190, FINSEQ_3: 25;

                            now

                              1 < ( len g1) by A1185, A1198, A1213, XXREAL_0: 2;

                              then

                               A1218: (1 + 1) <= ( len g1) by NAT_1: 13;

                              assume k = 1;

                              hence contradiction by A52, A1218, TOPREAL1: 23;

                            end;

                            then 1 < k by A24, XXREAL_0: 1;

                            then

                             A1219: (( L~ f1) /\ ( LSeg (f,k))) = {(f /. k)} by A3, A6, A7, GOBOARD2: 4;

                            

                             A1220: (n + 1) in ( dom g1) by A1185, A1198, A1213, FINSEQ_3: 25;

                            then

                             A1221: ( LSeg (g,n)) = ( LSeg (g1,n)) by A1217, TOPREAL3: 18;

                            then ( LSeg (g,n)) in l1 by A1185, A1190, A1213;

                            then ( LSeg (g,n)) c= ( L~ f1) by A44, ZFMISC_1: 74;

                            then

                             A1222: (( LSeg (g,n)) /\ ( LSeg (g,m))) c= {(f /. k)} by A1219, A1214, XBOOLE_1: 27;

                            now

                              set x = the Element of (( LSeg (g,n)) /\ ( LSeg (g,m)));

                              assume

                               A1223: (( LSeg (g,n)) /\ ( LSeg (g,m))) <> {} ;

                              then

                               A1224: x in ( LSeg (g,n)) by XBOOLE_0:def 4;

                              x in {(f /. k)} by A1222, A1223;

                              then

                               A1225: x = (f /. k) by TARSKI:def 1;

                              (f /. k) = (g1 /. ( len g1)) by A27, A14, A51, A46, FINSEQ_4: 71;

                              hence contradiction by A40, A41, A42, A1185, A1213, A1217, A1220, A1221, A1224, A1225, GOBOARD2: 2;

                            end;

                            hence thesis;

                          end;

                            suppose m <> ( len g1);

                            then

                             A1226: ( len g1) < m by A1212, XXREAL_0: 1;

                            then (( len g1) + 1) <= m by NAT_1: 13;

                            then

                             A1227: 1 <= m1 by XREAL_1: 19;

                            (m + 1) = ((m1 + 1) + ( len g1));

                            then

                             A1228: (m1 + 1) <= ( len g2) by A1196, A1203, XREAL_1: 6;

                            m = (m1 + ( len g1));

                            then

                             A1229: ( LSeg (g,m)) = ( LSeg (g2,m1)) by A1196, A1226, GOBOARD2: 5;

                            then ( LSeg (g,m)) in l2 by A1227, A1228;

                            then

                             A1230: ( LSeg (g,m)) c= ( L~ g2) by ZFMISC_1: 74;

                            now

                              per cases ;

                                suppose

                                 A1231: (n + 1) <= ( len g1);

                                then n <= ( len g1) by A1202, XXREAL_0: 2;

                                then

                                 A1232: n in ( dom g1) by A1190, FINSEQ_3: 25;

                                (n + 1) in ( dom g1) by A1198, A1231, FINSEQ_3: 25;

                                then ( LSeg (g,n)) = ( LSeg (g1,n)) by A1232, TOPREAL3: 18;

                                then ( LSeg (g,n)) in l1 by A1190, A1231;

                                then ( LSeg (g,n)) c= ( L~ g1) by ZFMISC_1: 74;

                                then (( LSeg (g,n)) /\ ( LSeg (g,m))) = {} by A1181, A1230, XBOOLE_1: 3, XBOOLE_1: 27;

                                hence thesis;

                              end;

                                suppose ( len g1) < (n + 1);

                                then

                                 A1233: ( len g1) <= n by NAT_1: 13;

                                then

                                reconsider n1 = (n - ( len g1)) as Element of NAT by INT_1: 5;

                                

                                 A1234: ((n - ( len g1)) + 1) = ((n + 1) - ( len g1));

                                

                                 A1235: n = (n1 + ( len g1));

                                now

                                  per cases ;

                                    suppose

                                     A1236: ( len g1) = n;

                                    now

                                      reconsider q1 = (g2 /. m1), q2 = (g2 /. (m1 + 1)) as Point of ( TOP-REAL 2);

                                      set x = the Element of (( LSeg (g,n)) /\ ( LSeg (g,m)));

                                      set q1l = { v where v be Point of ( TOP-REAL 2) : (v `2 ) = (ppi `2 ) & (q1 `1 ) <= (v `1 ) & (v `1 ) <= (q2 `1 ) };

                                      

                                       A1237: q1 = |[(q1 `1 ), (q1 `2 )]| & q2 = |[(q2 `1 ), (q2 `2 )]| by EUCLID: 53;

                                      assume

                                       A1238: (( LSeg (g,n)) /\ ( LSeg (g,m))) <> {} ;

                                      then

                                       A1239: x in ( LSeg (g,m)) by XBOOLE_0:def 4;

                                      x in ( LSeg (g,n)) by A1238, XBOOLE_0:def 4;

                                      then

                                       A1240: ex qx be Point of ( TOP-REAL 2) st qx = x & (qx `2 ) = (ppi `2 ) & (ppi `1 ) <= (qx `1 ) & (qx `1 ) <= (qq `1 ) by A1204, A1236;

                                      

                                       A1241: m1 in ( dom g2) by A1227, A1228, SEQ_4: 134;

                                      then

                                       A1242: (q1 `2 ) = (ppi `2 ) by A1027;

                                      

                                       A1243: (m1 + 1) in ( dom g2) by A1227, A1228, SEQ_4: 134;

                                      then

                                       A1244: (q2 `2 ) = (ppi `2 ) by A1027;

                                      m1 < (m1 + 1) by NAT_1: 13;

                                      then

                                       A1245: (q1 `1 ) < (q2 `1 ) by A1045, A1241, A1243;

                                      ( LSeg (g2,m1)) = ( LSeg (q1,q2)) by A1227, A1228, TOPREAL1:def 3

                                      .= q1l by A1242, A1244, A1245, A1237, TOPREAL3: 10;

                                      then

                                       A1246: ex qy be Point of ( TOP-REAL 2) st qy = x & (qy `2 ) = (ppi `2 ) & (q1 `1 ) <= (qy `1 ) & (qy `1 ) <= (q2 `1 ) by A1229, A1239;

                                      m1 > (n1 + 1) & (n1 + 1) >= 1 by A1185, A1234, NAT_1: 11, XREAL_1: 9;

                                      then m1 > 1 by XXREAL_0: 2;

                                      then (qq `1 ) < (q1 `1 ) by A1045, A1192, A1241;

                                      hence contradiction by A1240, A1246, XXREAL_0: 2;

                                    end;

                                    hence thesis;

                                  end;

                                    suppose n <> ( len g1);

                                    then ( len g1) < n by A1233, XXREAL_0: 1;

                                    then

                                     A1247: ( LSeg (g,n)) = ( LSeg (g2,n1)) by A1199, A1235, GOBOARD2: 5;

                                    m1 > (n1 + 1) by A1185, A1234, XREAL_1: 9;

                                    hence thesis by A1071, A1229, A1247;

                                  end;

                                end;

                                hence thesis;

                              end;

                            end;

                            hence thesis;

                          end;

                        end;

                        hence thesis;

                      end;

                    end;

                    hence thesis;

                  end;

                  hence g is s.n.c. by GOBOARD2: 1;

                  now

                    set p = (g1 /. ( len g1)), q = (g2 /. 1);

                    (i1 + 1) <= j1 by A1011, NAT_1: 13;

                    then 1 <= l by XREAL_1: 19;

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

                    then (q `2 ) = (ppi `2 ) by A1027;

                    hence (p `1 ) = (q `1 ) or (p `2 ) = (q `2 ) by A27, A14, A51, A46, A29, FINSEQ_4: 71;

                  end;

                  hence g is special by A43, A1036, GOBOARD2: 8;

                  thus ( L~ g) = ( L~ f)

                  proof

                    set lg = { ( LSeg (g,i)) : 1 <= i & (i + 1) <= ( len g) }, lf = { ( LSeg (f,j)) : 1 <= j & (j + 1) <= ( len f) };

                    

                     A1248: ( len g) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

                     A1249:

                    now

                      let j;

                      assume that

                       A1250: ( len g1) <= j and

                       A1251: j <= ( len g);

                      reconsider w = (j - ( len g1)) as Element of NAT by A1250, INT_1: 5;

                      let p such that

                       A1252: p = (g /. j);

                      now

                        per cases ;

                          suppose

                           A1253: j = ( len g1);

                          1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                          then ( len g1) in ( dom g1) by FINSEQ_3: 25;

                          

                          then

                           A1254: (g /. ( len g1)) = (f1 /. ( len f1)) by A46, FINSEQ_4: 68

                          .= (G * (i1,i2)) by A27, A14, A51, A29, FINSEQ_4: 71;

                          hence (p `2 ) = ((G * (i1,i2)) `2 ) by A1252, A1253;

                          thus ((G * (i1,i2)) `1 ) <= (p `1 ) & (p `1 ) <= ((G * (j1,i2)) `1 ) by A66, A23, A69, A65, A60, A1011, A1013, A1015, A1252, A1253, A1254, SEQM_3:def 1;

                          thus p in ( rng c1) by A66, A60, A1012, A1252, A1253, A1254, PARTFUN2: 2;

                        end;

                          suppose j <> ( len g1);

                          then ( len g1) < j by A1250, XXREAL_0: 1;

                          then (( len g1) + 1) <= j by NAT_1: 13;

                          then

                           A1255: 1 <= w by XREAL_1: 19;

                          

                           A1256: w <= ( len g2) by A1248, A1251, XREAL_1: 20;

                          then

                           A1257: w in ( dom g2) by A1255, FINSEQ_3: 25;

                          j = (w + ( len g1));

                          then (g /. j) = (g2 /. w) by A1255, A1256, SEQ_4: 136;

                          hence (p `2 ) = (ppi `2 ) & (ppi `1 ) <= (p `1 ) & (p `1 ) <= (pj `1 ) & p in ( rng c1) by A1027, A1252, A1257;

                        end;

                      end;

                      hence (p `2 ) = (ppi `2 ) & (ppi `1 ) <= (p `1 ) & (p `1 ) <= (pj `1 ) & p in ( rng c1);

                    end;

                    thus ( L~ g) c= ( L~ f)

                    proof

                      let x be object;

                      assume x in ( L~ g);

                      then

                      consider X be set such that

                       A1258: x in X and

                       A1259: X in lg by TARSKI:def 4;

                      consider i such that

                       A1260: X = ( LSeg (g,i)) and

                       A1261: 1 <= i and

                       A1262: (i + 1) <= ( len g) by A1259;

                      now

                        per cases ;

                          suppose

                           A1263: (i + 1) <= ( len g1);

                          i <= (i + 1) by NAT_1: 11;

                          then i <= ( len g1) by A1263, XXREAL_0: 2;

                          then

                           A1264: i in ( dom g1) by A1261, FINSEQ_3: 25;

                          1 <= (i + 1) by NAT_1: 11;

                          then (i + 1) in ( dom g1) by A1263, FINSEQ_3: 25;

                          then X = ( LSeg (g1,i)) by A1260, A1264, TOPREAL3: 18;

                          then X in { ( LSeg (g1,j)) : 1 <= j & (j + 1) <= ( len g1) } by A1261, A1263;

                          then

                           A1265: x in ( L~ f1) by A44, A1258, TARSKI:def 4;

                          ( L~ f1) c= ( L~ f) by TOPREAL3: 20;

                          hence thesis by A1265;

                        end;

                          suppose

                           A1266: (i + 1) > ( len g1);

                          reconsider q1 = (g /. i), q2 = (g /. (i + 1)) as Point of ( TOP-REAL 2);

                          

                           A1267: i <= ( len g) by A1262, NAT_1: 13;

                          

                           A1268: ( len g1) <= i by A1266, NAT_1: 13;

                          then

                           A1269: (q1 `2 ) = (ppi `2 ) by A1249, A1267;

                          

                           A1270: (q1 `1 ) <= (pj `1 ) by A1249, A1268, A1267;

                          

                           A1271: (ppi `1 ) <= (q1 `1 ) by A1249, A1268, A1267;

                          (q2 `2 ) = (ppi `2 ) by A1249, A1262, A1266;

                          then

                           A1272: q2 = |[(q2 `1 ), (q1 `2 )]| by A1269, EUCLID: 53;

                          

                           A1273: (q2 `1 ) <= (pj `1 ) by A1249, A1262, A1266;

                          

                           A1274: q1 = |[(q1 `1 ), (q1 `2 )]| & ( LSeg (g,i)) = ( LSeg (q2,q1)) by A1261, A1262, EUCLID: 53, TOPREAL1:def 3;

                          

                           A1275: (ppi `1 ) <= (q2 `1 ) by A1249, A1262, A1266;

                          now

                            per cases by XXREAL_0: 1;

                              suppose (q1 `1 ) > (q2 `1 );

                              then ( LSeg (g,i)) = { p2 : (p2 `2 ) = (q1 `2 ) & (q2 `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q1 `1 ) } by A1272, A1274, TOPREAL3: 10;

                              then

                              consider p2 such that

                               A1276: p2 = x & (p2 `2 ) = (q1 `2 ) and

                               A1277: (q2 `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q1 `1 ) by A1258, A1260;

                              (ppi `1 ) <= (p2 `1 ) & (p2 `1 ) <= (pj `1 ) by A1270, A1275, A1277, XXREAL_0: 2;

                              then

                               A1278: x in ( LSeg (f,k)) by A1099, A1269, A1276;

                              ( LSeg (f,k)) in lf by A3, A24;

                              hence thesis by A1278, TARSKI:def 4;

                            end;

                              suppose (q1 `1 ) = (q2 `1 );

                              then ( LSeg (g,i)) = {q1} by A1272, A1274, RLTOPSP1: 70;

                              then x = q1 by A1258, A1260, TARSKI:def 1;

                              then

                               A1279: x in ( LSeg (f,k)) by A1099, A1269, A1271, A1270;

                              ( LSeg (f,k)) in lf by A3, A24;

                              hence thesis by A1279, TARSKI:def 4;

                            end;

                              suppose (q1 `1 ) < (q2 `1 );

                              then ( LSeg (g,i)) = { p1 : (p1 `2 ) = (q1 `2 ) & (q1 `1 ) <= (p1 `1 ) & (p1 `1 ) <= (q2 `1 ) } by A1272, A1274, TOPREAL3: 10;

                              then

                              consider p2 such that

                               A1280: p2 = x & (p2 `2 ) = (q1 `2 ) and

                               A1281: (q1 `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q2 `1 ) by A1258, A1260;

                              (ppi `1 ) <= (p2 `1 ) & (p2 `1 ) <= (pj `1 ) by A1271, A1273, A1281, XXREAL_0: 2;

                              then

                               A1282: x in ( LSeg (f,k)) by A1099, A1269, A1280;

                              ( LSeg (f,k)) in lf by A3, A24;

                              hence thesis by A1282, TARSKI:def 4;

                            end;

                          end;

                          hence thesis;

                        end;

                      end;

                      hence thesis;

                    end;

                    let x be object;

                    assume x in ( L~ f);

                    then

                     A1283: x in (( L~ f1) \/ ( LSeg (f,k))) by A3, A13, GOBOARD2: 3;

                    now

                      per cases by A1283, XBOOLE_0:def 3;

                        suppose

                         A1284: x in ( L~ f1);

                        ( L~ g1) c= ( L~ g) by GOBOARD2: 6;

                        hence thesis by A44, A1284;

                      end;

                        suppose x in ( LSeg (f,k));

                        then

                        consider p1 such that

                         A1285: p1 = x and

                         A1286: (p1 `2 ) = (ppi `2 ) and

                         A1287: (ppi `1 ) <= (p1 `1 ) and

                         A1288: (p1 `1 ) <= (pj `1 ) by A1099;

                        defpred P2[ Nat] means ( len g1) <= $1 & $1 <= ( len g) & for q st q = (g /. $1) holds (q `1 ) <= (p1 `1 );

                         A1289:

                        now

                          reconsider n = ( len g1) as Nat;

                          take n;

                          thus P2[n]

                          proof

                            thus ( len g1) <= n & n <= ( len g) by A1248, XREAL_1: 31;

                            1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                            then

                             A1290: ( len g1) in ( dom g1) by FINSEQ_3: 25;

                            let q;

                            assume q = (g /. n);

                            

                            then q = (f1 /. ( len f1)) by A46, A1290, FINSEQ_4: 68

                            .= (G * (i1,i2)) by A27, A14, A51, A29, FINSEQ_4: 71;

                            hence thesis by A1287;

                          end;

                        end;

                        

                         A1291: for n be Nat holds P2[n] implies n <= ( len g);

                        consider ma be Nat such that

                         A1292: P2[ma] & for n be Nat st P2[n] holds n <= ma from NAT_1:sch 6( A1291, A1289);

                        reconsider ma as Nat;

                        now

                          per cases ;

                            suppose

                             A1293: ma = ( len g);

                            (i1 + 1) <= j1 by A1011, NAT_1: 13;

                            then

                             A1294: 1 <= l by XREAL_1: 19;

                            then (( len g1) + 1) <= ma by A1017, A1248, A1293, XREAL_1: 7;

                            then

                             A1295: ( len g1) <= (ma - 1) by XREAL_1: 19;

                            then ( 0 + 1) <= ma by XREAL_1: 19;

                            then

                            reconsider m1 = (ma - 1) as Element of NAT by INT_1: 5;

                            reconsider q = (g /. m1) as Point of ( TOP-REAL 2);

                            

                             A1296: (ma - 1) <= ( len g) by A1293, XREAL_1: 43;

                            then

                             A1297: (q `2 ) = (ppi `2 ) by A1249, A1295;

                            

                             A1298: (q `1 ) <= (pj `1 ) by A1249, A1296, A1295;

                            set lq = { e where e be Point of ( TOP-REAL 2) : (e `2 ) = (ppi `2 ) & (q `1 ) <= (e `1 ) & (e `1 ) <= (pj `1 ) };

                            

                             A1299: (i1 + l) = j1;

                            

                             A1300: l in ( dom g2) by A1017, A1294, FINSEQ_3: 25;

                            

                            then

                             A1301: (g /. ma) = (g2 /. l) by A1017, A1248, A1293, FINSEQ_4: 69

                            .= pj by A1017, A1300, A1299;

                            then (pj `1 ) <= (p1 `1 ) by A1292;

                            then

                             A1302: (p1 `1 ) = (pj `1 ) by A1288, XXREAL_0: 1;

                            1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                            then

                             A1303: 1 <= m1 by A1295, XXREAL_0: 2;

                            

                             A1304: (m1 + 1) = ma;

                            then q = |[(q `1 ), (q `2 )]| & ( LSeg (g,m1)) = ( LSeg (q,pj)) by A1293, A1301, A1303, EUCLID: 53, TOPREAL1:def 3;

                            then ( LSeg (g,m1)) = lq by A1083, A1098, A1297, A1298, TOPREAL3: 10;

                            then

                             A1305: p1 in ( LSeg (g,m1)) by A1286, A1302, A1298;

                            ( LSeg (g,m1)) in lg by A1293, A1303, A1304;

                            hence thesis by A1285, A1305, TARSKI:def 4;

                          end;

                            suppose ma <> ( len g);

                            then ma < ( len g) by A1292, XXREAL_0: 1;

                            then

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

                            reconsider qa = (g /. ma), qa1 = (g /. (ma + 1)) as Point of ( TOP-REAL 2);

                            set lma = { p2 : (p2 `2 ) = (ppi `2 ) & (qa `1 ) <= (p2 `1 ) & (p2 `1 ) <= (qa1 `1 ) };

                            

                             A1307: qa1 = |[(qa1 `1 ), (qa1 `2 )]| by EUCLID: 53;

                            

                             A1308: (qa `1 ) <= (p1 `1 ) by A1292;

                            

                             A1309: ( len g1) <= (ma + 1) by A1292, NAT_1: 13;

                            then

                             A1310: (qa1 `2 ) = (ppi `2 ) by A1249, A1306;

                             A1311:

                            now

                              assume (qa1 `1 ) <= (p1 `1 );

                              then for q holds q = (g /. (ma + 1)) implies (q `1 ) <= (p1 `1 );

                              then (ma + 1) <= ma by A1292, A1306, A1309;

                              hence contradiction by XREAL_1: 29;

                            end;

                            

                             A1312: (qa `2 ) = (ppi `2 ) & qa = |[(qa `1 ), (qa `2 )]| by A1249, A1292, EUCLID: 53;

                            

                             A1313: 1 <= ma by A24, A14, A47, A1292, NAT_1: 13;

                            

                            then ( LSeg (g,ma)) = ( LSeg (qa,qa1)) by A1306, TOPREAL1:def 3

                            .= lma by A1308, A1311, A1310, A1312, A1307, TOPREAL3: 10, XXREAL_0: 2;

                            then

                             A1314: x in ( LSeg (g,ma)) by A1285, A1286, A1308, A1311;

                            ( LSeg (g,ma)) in lg by A1306, A1313;

                            hence thesis by A1314, TARSKI:def 4;

                          end;

                        end;

                        hence thesis;

                      end;

                    end;

                    hence thesis;

                  end;

                  1 <= ( len g1) by A24, A14, A47, XXREAL_0: 2;

                  then 1 in ( dom g1) by FINSEQ_3: 25;

                  

                  hence (g /. 1) = (f1 /. 1) by A45, FINSEQ_4: 68

                  .= (f /. 1) by A27, A25, FINSEQ_4: 71;

                  

                   A1315: ( len g) = (( len g1) + l) by A1017, FINSEQ_1: 22;

                  (i1 + 1) <= j1 by A1011, NAT_1: 13;

                  then

                   A1316: 1 <= l by XREAL_1: 19;

                  then

                   A1317: l in ( dom g2) by A1017, FINSEQ_3: 25;

                  

                  hence (g /. ( len g)) = (g2 /. l) by A1315, FINSEQ_4: 69

                  .= (G * ((i1 + l),i2)) by A1017, A1317

                  .= (f /. ( len f)) by A3, A21, A698;

                  thus ( len f) <= ( len g) by A3, A14, A47, A1316, A1315, XREAL_1: 7;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

      

       A1318: P[ 0 ]

      proof

        let f such that

         A1319: ( len f) = 0 and

         A1320: (for n st n in ( dom f) holds ex i, j st [i, j] in ( Indices G) & (f /. n) = (G * (i,j))) & f is one-to-one unfolded s.n.c. special;

        take g = f;

        f = {} by A1319;

        then for n holds n in ( dom g) & (n + 1) in ( dom g) implies for m, k, i, j st [m, k] in ( Indices G) & [i, j] in ( Indices G) & (g /. n) = (G * (m,k)) & (g /. (n + 1)) = (G * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1;

        hence thesis by A1320, GOBOARD1:def 9;

      end;

      for k holds P[k] from NAT_1:sch 2( A1318, A1);

      hence thesis;

    end;

    theorem :: GOBOARD3:2

    (for n st n in ( dom f) holds ex i, j st [i, j] in ( Indices G) & (f /. n) = (G * (i,j))) & f is being_S-Seq implies ex g st g is_sequence_on G & g is being_S-Seq & ( L~ f) = ( L~ g) & (f /. 1) = (g /. 1) & (f /. ( len f)) = (g /. ( len g)) & ( len f) <= ( len g)

    proof

      assume that

       A1: for n st n in ( dom f) holds ex i, j st [i, j] in ( Indices G) & (f /. n) = (G * (i,j)) and

       A2: f is being_S-Seq;

      f is one-to-one & f is unfolded s.n.c. special by A2;

      then

      consider g such that

       A3: g is_sequence_on G and

       A4: g is one-to-one unfolded s.n.c. special and

       A5: ( L~ f) = ( L~ g) & (f /. 1) = (g /. 1) & (f /. ( len f)) = (g /. ( len g)) and

       A6: ( len f) <= ( len g) by A1, Th1;

      take g;

      thus g is_sequence_on G by A3;

      2 <= ( len f) by A2;

      then 2 <= ( len g) by A6, XXREAL_0: 2;

      hence g is being_S-Seq by A4;

      thus thesis by A5, A6;

    end;