goboard2.miz



    begin

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

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

r,s for Real,

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

G for Go-board,

x for set;

    theorem :: GOBOARD2:1

    (for n, m st m > (n + 1) & n in ( dom f) & (n + 1) in ( dom f) & m in ( dom f) & (m + 1) in ( dom f) holds ( LSeg (f,n)) misses ( LSeg (f,m))) implies f is s.n.c.

    proof

      assume

       A1: for n, m st m > (n + 1) & n in ( dom f) & (n + 1) in ( dom f) & m in ( dom f) & (m + 1) in ( dom f) holds ( LSeg (f,n)) misses ( LSeg (f,m));

      let n,m be Nat such that

       A2: m > (n + 1);

      

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

      per cases ;

        suppose n in ( dom f) & (n + 1) in ( dom f) & m in ( dom f) & (m + 1) in ( dom f);

        hence thesis by A1, A2;

      end;

        suppose not (n in ( dom f) & (n + 1) in ( dom f) & m in ( dom f) & (m + 1) in ( dom f));

        then not (1 <= n & n <= ( len f) & 1 <= (n + 1) & (n + 1) <= ( len f) & 1 <= m & m <= ( len f) & 1 <= (m + 1) & (m + 1) <= ( len f)) by FINSEQ_3: 25;

        then not (1 <= n & (n + 1) <= ( len f) & 1 <= m & (m + 1) <= ( len f)) by A3, XXREAL_0: 2;

        then ( LSeg (f,m)) = {} or ( LSeg (f,n)) = {} by TOPREAL1:def 3;

        hence thesis;

      end;

    end;

    theorem :: GOBOARD2:2

    f is unfolded s.n.c. one-to-one & (f /. ( len f)) in ( LSeg (f,i)) & i in ( dom f) & (i + 1) in ( dom f) implies (i + 1) = ( len f)

    proof

      assume that

       A1: f is unfolded and

       A2: f is s.n.c. and

       A3: f is one-to-one and

       A4: (f /. ( len f)) in ( LSeg (f,i)) and

       A5: i in ( dom f) and

       A6: (i + 1) in ( dom f) and

       A7: (i + 1) <> ( len f);

      

       A8: 1 <= i by A5, FINSEQ_3: 25;

      

       A9: i <= ( len f) by A5, FINSEQ_3: 25;

      then

      reconsider l = (( len f) - 1) as Element of NAT by A8, INT_1: 5, XXREAL_0: 2;

      1 <= ( len f) by A8, A9, XXREAL_0: 2;

      then

       A10: (l + 1) in ( dom f) by FINSEQ_3: 25;

      

       A11: (i + 1) <= ( len f) by A6, FINSEQ_3: 25;

      then (i + 1) < ( len f) by A7, XXREAL_0: 1;

      then

       A12: ((i + 1) + 1) <= ( len f) by NAT_1: 13;

      then

       A13: (i + 1) <= (( len f) - 1) by XREAL_1: 19;

      i <= l by A11, XREAL_1: 19;

      then

       A14: 1 <= l by A8, XXREAL_0: 2;

      then

       A15: (f /. (l + 1)) in ( LSeg (f,l)) by TOPREAL1: 21;

      1 <= (i + 1) by A6, FINSEQ_3: 25;

      then

       A16: (f /. (i + 2)) in ( LSeg (f,(i + 1))) by A12, TOPREAL1: 21;

      l <= ( len f) by XREAL_1: 43;

      then

       A17: l in ( dom f) by A14, FINSEQ_3: 25;

      l <> (l + 1);

      then

       A18: (f /. l) <> (f /. (l + 1)) by A3, A17, A10, PARTFUN2: 10;

      ((i + 1) + 1) = (i + (1 + 1));

      then

       A19: (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) = {(f /. (i + 1))} by A1, A8, A12;

      now

        per cases ;

          suppose

           A20: l = (i + 1);

          then (f /. ( len f)) in (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) by A4, A16, XBOOLE_0:def 4;

          hence contradiction by A18, A19, A20, TARSKI:def 1;

        end;

          suppose l <> (i + 1);

          then (i + 1) < l by A13, XXREAL_0: 1;

          then ( LSeg (f,i)) misses ( LSeg (f,l)) by A2;

          then (( LSeg (f,i)) /\ ( LSeg (f,l))) = {} ;

          hence contradiction by A4, A15, XBOOLE_0:def 4;

        end;

      end;

      hence contradiction;

    end;

    theorem :: GOBOARD2:3

    

     Th3: k <> 0 & ( len f) = (k + 1) implies ( L~ f) = (( L~ (f | k)) \/ ( LSeg (f,k)))

    proof

      assume that

       A1: k <> 0 and

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

      

       A3: ( 0 + 1) <= k by A1, NAT_1: 13;

      set f1 = (f | k), lf = { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) }, l1 = { ( LSeg (f1,j)) : 1 <= j & (j + 1) <= ( len f1) };

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

      then

       A4: ( len (f | k)) = k by FINSEQ_1: 59;

      thus ( L~ f) c= (( L~ (f | k)) \/ ( LSeg (f,k)))

      proof

        let x be object;

        assume x in ( L~ f);

        then

        consider X be set such that

         A5: x in X and

         A6: X in lf by TARSKI:def 4;

        consider n such that

         A7: X = ( LSeg (f,n)) and

         A8: 1 <= n and

         A9: (n + 1) <= ( len f) by A6;

        now

          per cases ;

            suppose (n + 1) = ( len f);

            hence thesis by A2, A5, A7, XBOOLE_0:def 3;

          end;

            suppose

             A10: (n + 1) <> ( len f);

            

             A11: 1 <= (n + 1) by A8, NAT_1: 13;

            n <= k by A2, A9, XREAL_1: 6;

            then

             A12: n in ( dom f1) by A4, A8, FINSEQ_3: 25;

            

             A13: (n + 1) < ( len f) by A9, A10, XXREAL_0: 1;

            then (n + 1) <= k by A2, NAT_1: 13;

            then (n + 1) in ( dom f1) by A4, A11, FINSEQ_3: 25;

            then

             A14: X = ( LSeg (f1,n)) by A7, A12, TOPREAL3: 17;

            (n + 1) <= k by A2, A13, NAT_1: 13;

            then X in l1 by A4, A8, A14;

            then x in ( union l1) by A5, TARSKI:def 4;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        hence thesis;

      end;

      

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

      let x be object such that

       A16: x in (( L~ f1) \/ ( LSeg (f,k)));

      now

        per cases by A16, XBOOLE_0:def 3;

          suppose x in ( L~ f1);

          then

          consider X be set such that

           A17: x in X and

           A18: X in l1 by TARSKI:def 4;

          consider n such that

           A19: X = ( LSeg (f1,n)) and

           A20: 1 <= n and

           A21: (n + 1) <= ( len f1) by A18;

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

          then n <= ( len f1) by A21, XXREAL_0: 2;

          then

           A22: n in ( dom f1) by A20, FINSEQ_3: 25;

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

          then (n + 1) in ( dom f1) by A21, FINSEQ_3: 25;

          then

           A23: X = ( LSeg (f,n)) by A19, A22, TOPREAL3: 17;

          (n + 1) <= ( len f) by A2, A15, A4, A21, XXREAL_0: 2;

          then X in lf by A20, A23;

          hence thesis by A17, TARSKI:def 4;

        end;

          suppose

           A24: x in ( LSeg (f,k));

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

          hence thesis by A24, TARSKI:def 4;

        end;

      end;

      hence thesis;

    end;

    theorem :: GOBOARD2:4

    1 < k & ( len f) = (k + 1) & f is unfolded s.n.c. implies (( L~ (f | k)) /\ ( LSeg (f,k))) = {(f /. k)}

    proof

      assume that

       A1: 1 < k and

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

       A3: f is unfolded and

       A4: f is s.n.c.;

      set f1 = (f | k);

      

       A5: ( len f1) = k by A2, FINSEQ_1: 59, NAT_1: 11;

      reconsider k1 = (k - 1) as Element of NAT by A1, INT_1: 5;

      set f2 = (f1 | k1), l2 = { ( LSeg (f2,m)) : 1 <= m & (m + 1) <= ( len f2) };

      

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

      

       A7: k in ( Seg k) by A1, FINSEQ_1: 1;

      

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

      

       A9: k1 < k by XREAL_1: 44;

      

       A10: k1 <= k by XREAL_1: 44;

      then

       A11: ( len f2) = k1 by A5, FINSEQ_1: 59;

      

       A12: ( Seg k1) c= ( Seg k) by A10, FINSEQ_1: 5;

      ( L~ f2) misses ( LSeg (f,k))

      proof

        assume not thesis;

        then

        consider x be object such that

         A13: x in ( L~ f2) and

         A14: x in ( LSeg (f,k)) by XBOOLE_0: 3;

        consider X be set such that

         A15: x in X and

         A16: X in l2 by A13, TARSKI:def 4;

        consider n such that

         A17: X = ( LSeg (f2,n)) and

         A18: 1 <= n and

         A19: (n + 1) <= ( len f2) by A16;

        

         A20: n in ( dom f2) & (n + 1) in ( dom f2) by A18, A19, SEQ_4: 134;

        then ( LSeg (f2,n)) = ( LSeg (f1,n)) by TOPREAL3: 17;

        then ( LSeg (f2,n)) = ( LSeg (f,n)) by A6, A12, A8, A5, A11, A20, TOPREAL3: 17;

        then

         A21: ( LSeg (f,n)) meets ( LSeg (f,k)) by A14, A15, A17, XBOOLE_0: 3;

        (n + 1) < k by A9, A11, A19, XXREAL_0: 2;

        hence contradiction by A4, A21;

      end;

      then

       A22: (( L~ f2) /\ ( LSeg (f,k))) = {} ;

      

       A23: (k + 1) = (k1 + (1 + 1));

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

      then

       A24: 1 <= k1 by XREAL_1: 19;

      then

       A25: k1 in ( Seg k) by A10, FINSEQ_1: 1;

      (k1 + 1) in ( Seg k) by A1, FINSEQ_1: 1;

      then ( L~ f1) = (( L~ f2) \/ ( LSeg (f1,k1))) by A24, A5, Th3;

      

      hence (( L~ f1) /\ ( LSeg (f,k))) = ( {} \/ (( LSeg (f1,k1)) /\ ( LSeg (f,k)))) by A22, XBOOLE_1: 23

      .= (( LSeg (f,k1)) /\ ( LSeg (f,(k1 + 1)))) by A6, A7, A25, A5, TOPREAL3: 17

      .= {(f /. k)} by A2, A3, A24, A23;

    end;

    theorem :: GOBOARD2:5

    ( len f1) < n & (n + 1) <= ( len (f1 ^ f2)) & (m + ( len f1)) = n implies ( LSeg ((f1 ^ f2),n)) = ( LSeg (f2,m))

    proof

      set f = (f1 ^ f2);

      assume that

       A1: ( len f1) < n and

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

       A3: (m + ( len f1)) = n;

      

       A4: 1 <= m by A1, A3, NAT_1: 19;

      reconsider p = (f /. n), q = (f /. (n + 1)) as Point of ( TOP-REAL 2);

      

       A5: (n + 1) = ((m + 1) + ( len f1)) by A3;

      ( len f) = (( len f1) + ( len f2)) by FINSEQ_1: 22;

      then

       A6: (m + 1) <= ( len f2) by A2, A5, XREAL_1: 6;

      then

       A7: (f /. (n + 1)) = (f2 /. (m + 1)) by A5, NAT_1: 11, SEQ_4: 136;

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

      then m <= ( len f2) by A6, XXREAL_0: 2;

      then

       A8: (f /. n) = (f2 /. m) by A3, A4, SEQ_4: 136;

      ( 0 + 1) <= n by A1, NAT_1: 13;

      

      hence ( LSeg (f,n)) = ( LSeg (p,q)) by A2, TOPREAL1:def 3

      .= ( LSeg (f2,m)) by A4, A6, A8, A7, TOPREAL1:def 3;

    end;

    theorem :: GOBOARD2:6

    

     Th6: ( L~ f) c= ( L~ (f ^ g))

    proof

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

      let x be object;

      assume x in ( L~ f);

      then

      consider X be set such that

       A1: x in X and

       A2: X in lf by TARSKI:def 4;

      consider n such that

       A3: X = ( LSeg (f,n)) and

       A4: 1 <= n and

       A5: (n + 1) <= ( len f) by A2;

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

      then n <= ( len f) by A5, XXREAL_0: 2;

      then

       A6: n in ( dom f) by A4, FINSEQ_3: 25;

      ( len f1) = (( len f) + ( len g)) by FINSEQ_1: 22;

      then ( len f) <= ( len f1) by XREAL_1: 31;

      then

       A7: (n + 1) <= ( len f1) by A5, XXREAL_0: 2;

      1 <= (n + 1) by XREAL_1: 31;

      then (n + 1) in ( dom f) by A5, FINSEQ_3: 25;

      then X = ( LSeg (f1,n)) by A3, A6, TOPREAL3: 18;

      then X in l1 by A4, A7;

      hence thesis by A1, TARSKI:def 4;

    end;

    theorem :: GOBOARD2:7

    f is s.n.c. implies (f | i) is s.n.c.

    proof

      assume

       A1: f is s.n.c.;

      set f1 = (f | i);

      let n,m be Nat;

      assume m > (n + 1);

      then ( LSeg (f,n)) misses ( LSeg (f,m)) by A1;

      then

       A2: (( LSeg (f,n)) /\ ( LSeg (f,m))) = {} ;

      now

        

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

        

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

        now

          per cases ;

            suppose

             A5: n in ( dom f1);

            now

              per cases ;

                suppose (n + 1) in ( dom f1);

                then

                 A6: ( LSeg (f,n)) = ( LSeg (f1,n)) by A5, TOPREAL3: 17;

                now

                  per cases ;

                    suppose

                     A7: m in ( dom f1);

                    now

                      per cases ;

                        suppose (m + 1) in ( dom f1);

                        hence (( LSeg (f1,n)) /\ ( LSeg (f1,m))) = {} by A2, A6, A7, TOPREAL3: 17;

                      end;

                        suppose not (m + 1) in ( dom f1);

                        then not (1 <= (m + 1) & (m + 1) <= ( len f1)) by FINSEQ_3: 25;

                        then ( LSeg (f1,m)) = {} by NAT_1: 11, TOPREAL1:def 3;

                        hence (( LSeg (f1,n)) /\ ( LSeg (f1,m))) = {} ;

                      end;

                    end;

                    hence thesis;

                  end;

                    suppose not m in ( dom f1);

                    then not (1 <= m & m <= ( len f1)) by FINSEQ_3: 25;

                    then not (1 <= m & (m + 1) <= ( len f1)) by A3, XXREAL_0: 2;

                    then ( LSeg (f1,m)) = {} by TOPREAL1:def 3;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

                suppose not (n + 1) in ( dom f1);

                then not (1 <= (n + 1) & (n + 1) <= ( len f1)) by FINSEQ_3: 25;

                then ( LSeg (f1,n)) = {} by NAT_1: 11, TOPREAL1:def 3;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

            suppose not n in ( dom f1);

            then not (1 <= n & n <= ( len f1)) by FINSEQ_3: 25;

            then not (1 <= n & (n + 1) <= ( len f1)) by A4, XXREAL_0: 2;

            then ( LSeg (f1,n)) = {} by TOPREAL1:def 3;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: GOBOARD2:8

    f1 is special & f2 is special & (((f1 /. ( len f1)) `1 ) = ((f2 /. 1) `1 ) or ((f1 /. ( len f1)) `2 ) = ((f2 /. 1) `2 )) implies (f1 ^ f2) is special

    proof

      assume that

       A1: f1 is special and

       A2: f2 is special and

       A3: ((f1 /. ( len f1)) `1 ) = ((f2 /. 1) `1 ) or ((f1 /. ( len f1)) `2 ) = ((f2 /. 1) `2 );

      let n be Nat;

      set f = (f1 ^ f2);

      assume that

       A4: 1 <= n and

       A5: (n + 1) <= ( len f);

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

      set p = (f /. n), q = (f /. (n + 1));

      

       A6: ( len f) = (( len f1) + ( len f2)) by FINSEQ_1: 22;

      per cases ;

        suppose

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

        then (n + 1) in ( dom f1) by A4, SEQ_4: 134;

        then

         A8: (f1 /. (n + 1)) = q by FINSEQ_4: 68;

        n in ( dom f1) by A4, A7, SEQ_4: 134;

        then (f1 /. n) = p by FINSEQ_4: 68;

        hence thesis by A1, A4, A7, A8;

      end;

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

        then

         A9: ( len f1) <= n by NAT_1: 13;

        then

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

        now

          per cases ;

            suppose

             A10: n = ( len f1);

            then n in ( dom f1) by A4, FINSEQ_3: 25;

            then

             A11: p = (f1 /. n) by FINSEQ_4: 68;

            ( len f2) >= 1 by A5, A6, A10, XREAL_1: 6;

            hence (p `1 ) = (q `1 ) or (p `2 ) = (q `2 ) by A3, A10, A11, SEQ_4: 136;

          end;

            suppose n <> ( len f1);

            then ( len f1) < n by A9, XXREAL_0: 1;

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

            then

             A12: 1 <= n1 by XREAL_1: 19;

            

             A13: (n + 1) = ((n1 + 1) + ( len f1));

            then

             A14: (n1 + 1) <= ( len f2) by A5, A6, XREAL_1: 6;

            then

             A15: (f2 /. (n1 + 1)) = q by A13, NAT_1: 11, SEQ_4: 136;

            (n1 + 1) >= n1 by NAT_1: 11;

            then n = (n1 + ( len f1)) & n1 <= ( len f2) by A14, XXREAL_0: 2;

            then (f2 /. n1) = p by A12, SEQ_4: 136;

            hence (p `1 ) = (q `1 ) or (p `2 ) = (q `2 ) by A2, A12, A14, A15;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: GOBOARD2:9

    

     Th9: f <> {} implies ( X_axis f) <> {}

    proof

      

       A1: ( len ( X_axis f)) = ( len f) by GOBOARD1:def 1;

      assume f <> {} & ( X_axis f) = {} ;

      hence contradiction by A1;

    end;

    theorem :: GOBOARD2:10

    

     Th10: f <> {} implies ( Y_axis f) <> {}

    proof

      

       A1: ( len ( Y_axis f)) = ( len f) by GOBOARD1:def 2;

      assume f <> {} & ( Y_axis f) = {} ;

      hence contradiction by A1;

    end;

    registration

      let f be non empty FinSequence of ( TOP-REAL 2);

      cluster ( X_axis f) -> non empty;

      coherence by Th9;

      cluster ( Y_axis f) -> non empty;

      coherence by Th10;

    end

    theorem :: GOBOARD2:11

    

     Th11: f is special implies for n be Nat st n in ( dom f) & (n + 1) in ( dom f) holds for i,j,m,k be Nat st [i, j] in ( Indices G) & [m, k] in ( Indices G) & (f /. n) = (G * (i,j)) & (f /. (n + 1)) = (G * (m,k)) holds i = m or k = j

    proof

      assume

       A1: f is special;

      let n be Nat;

      assume n in ( dom f) & (n + 1) in ( dom f);

      then

       A2: 1 <= n & (n + 1) <= ( len f) by FINSEQ_3: 25;

      let i,j,m,k be Nat such that

       A3: [i, j] in ( Indices G) and

       A4: [m, k] in ( Indices G) and

       A5: (f /. n) = (G * (i,j)) & (f /. (n + 1)) = (G * (m,k));

      reconsider cj = ( Col (G,j)), lm = ( Line (G,m)) as FinSequence of ( TOP-REAL 2);

      set xj = ( X_axis cj), yj = ( Y_axis cj), xm = ( X_axis lm), ym = ( Y_axis lm);

      ( len cj) = ( len G) by MATRIX_0:def 8;

      then

       A6: ( dom cj) = ( dom G) by FINSEQ_3: 29;

      assume that

       A7: i <> m and

       A8: k <> j;

      

       A9: ( len xm) = ( len lm) & ( dom xm) = ( Seg ( len xm)) by FINSEQ_1:def 3, GOBOARD1:def 1;

      

       A10: ( len xj) = ( len cj) by GOBOARD1:def 1;

      then

       A11: ( dom xj) = ( dom cj) by FINSEQ_3: 29;

      

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

      then

       A13: i in ( dom G) by A3, ZFMISC_1: 87;

      then (cj /. i) = (cj . i) by A6, PARTFUN1:def 6;

      then

       A14: (G * (i,j)) = (cj /. i) by A13, MATRIX_0:def 8;

      then

       A15: (xj . i) = ((G * (i,j)) `1 ) by A13, A6, A11, GOBOARD1:def 1;

      

       A16: m in ( dom G) by A4, A12, ZFMISC_1: 87;

      then (cj /. m) = (cj . m) by A6, PARTFUN1:def 6;

      then

       A17: (G * (m,j)) = (cj /. m) by A16, MATRIX_0:def 8;

      then

       A18: (xj . m) = ((G * (m,j)) `1 ) by A16, A6, A11, GOBOARD1:def 1;

      

       A19: ym is increasing by A16, GOBOARD1:def 6;

      

       A20: xm is constant by A16, GOBOARD1:def 4;

      

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

      

       A22: ( dom xj) = ( Seg ( len xj)) & ( len yj) = ( len cj) by FINSEQ_1:def 3, GOBOARD1:def 2;

      then

       A23: (yj . m) = ((G * (m,j)) `2 ) by A16, A10, A21, A6, A11, A17, GOBOARD1:def 2;

      

       A24: j in ( Seg ( width G)) by A3, A12, ZFMISC_1: 87;

      then

       A25: xj is increasing by GOBOARD1:def 7;

      

       A26: ( len lm) = ( width G) by MATRIX_0:def 7;

      then

       A27: ( dom lm) = ( Seg ( width G)) by FINSEQ_1:def 3;

      then (lm /. j) = (lm . j) by A24, PARTFUN1:def 6;

      then

       A28: (G * (m,j)) = (lm /. j) by A24, MATRIX_0:def 7;

      then

       A29: (xm . j) = ((G * (m,j)) `1 ) by A24, A26, A9, GOBOARD1:def 1;

      

       A30: k in ( Seg ( width G)) by A4, A12, ZFMISC_1: 87;

      then (lm /. k) = (lm . k) by A27, PARTFUN1:def 6;

      then

       A31: (G * (m,k)) = (lm /. k) by A30, MATRIX_0:def 7;

      then

       A32: (xm . k) = ((G * (m,k)) `1 ) by A30, A26, A9, GOBOARD1:def 1;

      

       A33: yj is constant by A24, GOBOARD1:def 5;

      

       A34: ( len ym) = ( len lm) & ( dom ym) = ( Seg ( len ym)) by FINSEQ_1:def 3, GOBOARD1:def 2;

      then

       A35: (ym . j) = ((G * (m,j)) `2 ) by A24, A26, A28, GOBOARD1:def 2;

      

       A36: (ym . k) = ((G * (m,k)) `2 ) by A30, A26, A34, A31, GOBOARD1:def 2;

      

       A37: (yj . i) = ((G * (i,j)) `2 ) by A13, A10, A22, A21, A6, A11, A14, GOBOARD1:def 2;

      now

        per cases by A1, A5, A2;

          suppose

           A38: ((G * (i,j)) `1 ) = ((G * (m,k)) `1 );

          now

            per cases by A7, XXREAL_0: 1;

              suppose i > m;

              then ((G * (m,j)) `1 ) < ((G * (i,j)) `1 ) by A13, A16, A6, A11, A25, A15, A18, SEQM_3:def 1;

              hence contradiction by A24, A30, A26, A9, A20, A29, A32, A38, SEQM_3:def 10;

            end;

              suppose i < m;

              then ((G * (m,j)) `1 ) > ((G * (i,j)) `1 ) by A13, A16, A6, A11, A25, A15, A18, SEQM_3:def 1;

              hence contradiction by A24, A30, A26, A9, A20, A29, A32, A38, SEQM_3:def 10;

            end;

          end;

          hence contradiction;

        end;

          suppose

           A39: ((G * (i,j)) `2 ) = ((G * (m,k)) `2 );

          now

            per cases by A8, XXREAL_0: 1;

              suppose k > j;

              then ((G * (m,j)) `2 ) < ((G * (m,k)) `2 ) by A24, A30, A26, A34, A19, A35, A36, SEQM_3:def 1;

              hence contradiction by A13, A16, A10, A22, A21, A6, A11, A33, A37, A23, A39, SEQM_3:def 10;

            end;

              suppose k < j;

              then ((G * (m,j)) `2 ) > ((G * (m,k)) `2 ) by A24, A30, A26, A34, A19, A35, A36, SEQM_3:def 1;

              hence contradiction by A13, A16, A10, A22, A21, A6, A11, A33, A37, A23, A39, SEQM_3:def 10;

            end;

          end;

          hence contradiction;

        end;

      end;

      hence contradiction;

    end;

    theorem :: GOBOARD2:12

    (for n be Nat st n in ( dom f) holds ex i,j be Nat st [i, j] in ( Indices G) & (f /. n) = (G * (i,j))) & f is special & (for n be Nat st n in ( dom f) & (n + 1) in ( dom f) holds (f /. n) <> (f /. (n + 1))) implies ex g st g is_sequence_on G & ( L~ f) = ( L~ g) & (g /. 1) = (f /. 1) & (g /. ( len g)) = (f /. ( len f)) & ( len f) <= ( len g)

    proof

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

      

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

      proof

        let k be Nat such that

         A2: P[k];

        let f such that

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

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

         A5: f is special and

         A6: for n be Nat st n in ( dom f) & (n + 1) in ( dom f) holds (f /. n) <> (f /. (n + 1));

        

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

        now

          per cases ;

            suppose

             A8: k = 0 ;

            take g = f;

            

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

            now

              let n be Nat;

              assume that

               A10: n in ( dom g) and

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

              n = 1 by A9, A10, 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 A9, A11, TARSKI:def 1;

            end;

            hence g is_sequence_on G by A4;

            thus ( L~ f) = ( L~ g) & (g /. 1) = (f /. 1) & (g /. ( len g)) = (f /. ( len f)) & ( len f) <= ( len g);

          end;

            suppose

             A12: k <> 0 ;

            then

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

            then

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

            

             A15: 1 in ( Seg k) by A13, FINSEQ_1: 1;

            

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

            then

             A17: k in ( dom f) by A3, A7, A13, FINSEQ_1: 1;

            then

            consider i1,i2 be Nat such that

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

             A19: (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);

            

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

            ( len y2) = ( len c1) by GOBOARD1:def 2;

            then

             A21: ( dom y2) = ( dom c1) by FINSEQ_3: 29;

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

            then

             A22: ( dom x2) = ( dom c1) by FINSEQ_3: 29;

            set f1 = (f | k);

            

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

            

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

             A25:

            now

              let n be Nat;

              assume

               A26: n in ( dom f1);

              then n in ( dom f) by A17, A23, A24, FINSEQ_4: 71;

              then

              consider i,j be Nat such that

               A27: [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 A17, A23, A24, A26, A27, FINSEQ_4: 71;

            end;

            

             A28: f1 is special

            proof

              let n be Nat;

              assume that

               A29: 1 <= n and

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

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

              then n <= ( len f1) by A30, XXREAL_0: 2;

              then n in ( dom f1) by A29, FINSEQ_3: 25;

              then

               A31: (f1 /. n) = (f /. n) by A17, A23, A24, FINSEQ_4: 71;

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

              then (n + 1) in ( dom f1) by A30, FINSEQ_3: 25;

              then

               A32: (f1 /. (n + 1)) = (f /. (n + 1)) by A17, A23, A24, FINSEQ_4: 71;

              (n + 1) <= ( len f) by A3, A16, A23, A30, XXREAL_0: 2;

              hence thesis by A5, A29, A31, A32;

            end;

            now

              let n be Nat;

              assume

               A33: n in ( dom f1) & (n + 1) in ( dom f1);

              then

               A34: (f1 /. n) = (f /. n) & (f1 /. (n + 1)) = (f /. (n + 1)) by A17, A23, A24, FINSEQ_4: 71;

              n in ( dom f) & (n + 1) in ( dom f) by A17, A23, A24, A33, FINSEQ_4: 71;

              hence (f1 /. n) <> (f1 /. (n + 1)) by A6, A34;

            end;

            then

            consider g1 such that

             A35: g1 is_sequence_on G and

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

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

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

             A39: ( len f1) <= ( len g1) by A2, A23, A25, A28;

            

             A40: for n be Nat st n in ( dom g1) holds ex m,k be Nat st [m, k] in ( Indices G) & (g1 /. n) = (G * (m,k)) by A35;

            

             A41: for n be Nat st n in ( dom g1) & (n + 1) in ( dom g1) holds for m,k,i,j be Nat 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 A35;

            

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

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

            then

             A43: ( dom c1) = ( dom G) by FINSEQ_3: 29;

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

            then

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

            then

            consider j1,j2 be Nat such that

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

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

            

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

            then

             A48: j1 in ( dom G) by A45, ZFMISC_1: 87;

            

             A49: i1 in ( dom G) by A18, A47, ZFMISC_1: 87;

            then

             A50: x1 is constant by GOBOARD1:def 4;

            

             A51: i2 in ( Seg ( width G)) by A18, A47, ZFMISC_1: 87;

            then

             A52: x2 is increasing by GOBOARD1:def 7;

            

             A53: y2 is constant by A51, GOBOARD1:def 5;

            

             A54: y1 is increasing by A49, GOBOARD1:def 6;

            

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

            

             A56: j2 in ( Seg ( width G)) by A45, A47, ZFMISC_1: 87;

            

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

            now

              per cases by A5, A17, A18, A19, A44, A45, A46, Th11;

                suppose

                 A58: i1 = j1;

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

                now

                  per cases by XXREAL_0: 1;

                    case

                     A59: i2 > j2;

                    j2 in ( dom l1) by A56, A55, FINSEQ_1:def 3;

                    then (l1 /. j2) = (l1 . j2) by PARTFUN1:def 6;

                    then

                     A60: (l1 /. j2) = pj by A56, MATRIX_0:def 7;

                    then

                     A61: (y1 . j2) = (pj `2 ) by A56, A20, A55, GOBOARD1:def 2;

                    i2 in ( dom l1) by A51, A55, FINSEQ_1:def 3;

                    then (l1 /. i2) = (l1 . i2) by PARTFUN1:def 6;

                    then

                     A62: (l1 /. i2) = ppi by A51, MATRIX_0:def 7;

                    then

                     A63: (y1 . i2) = (ppi `2 ) by A51, A20, A55, GOBOARD1:def 2;

                    then

                     A64: (pj `2 ) < (ppi `2 ) by A51, A56, A54, A20, A55, A59, A61, SEQM_3:def 1;

                    

                     A65: (x1 . j2) = (pj `1 ) by A56, A42, A55, A60, GOBOARD1:def 1;

                    (x1 . i2) = (ppi `1 ) by A51, A42, A55, A62, GOBOARD1:def 1;

                    then

                     A66: (ppi `1 ) = (pj `1 ) by A51, A56, A50, A42, A55, A65, SEQM_3:def 10;

                    reconsider l = (i2 - j2) as Element of NAT by A59, 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 ) };

                    

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

                     A68:

                    now

                      let n;

                      assume n in ( Seg l);

                      then

                       A69: n <= l by FINSEQ_1: 1;

                      l <= i2 by XREAL_1: 43;

                      then

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

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

                      then

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

                      

                       A71: 1 <= j2 by A56, FINSEQ_1: 1;

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

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

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

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

                    end;

                     A72:

                    now

                      let n be Nat;

                      assume n in ( Seg l);

                      then

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

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

                      thus P1[n, p];

                    end;

                    consider g2 such that

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

                    take g = (g1 ^ g2);

                    

                     A74: ( dom g2) = ( Seg l) by A73, FINSEQ_1:def 3;

                     A75:

                    now

                      let n be Nat;

                      assume that

                       A76: n in ( dom g2) and

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

                      reconsider m1 = (i2 - n), m2 = (i2 - (n + 1)) as Element of NAT by A68, A74, A76, A77;

                      let l1,l2,l3,l4 be Nat;

                      assume that

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

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

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

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

                       [i1, (i2 - (n + 1))] in ( Indices G) & (g2 /. (n + 1)) = (G * (i1,m2)) by A68, A73, A74, A77;

                      then

                       A82: l3 = i1 & l4 = m2 by A79, A81, GOBOARD1: 5;

                       [i1, (i2 - n)] in ( Indices G) & (g2 /. n) = (G * (i1,m1)) by A68, A73, A74, A76;

                      then l1 = i1 & l2 = m1 by A78, A80, GOBOARD1: 5;

                      

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

                      .= 1 by ABSVALUE:def 1;

                    end;

                    now

                      let n be Nat;

                      assume

                       A83: n in ( dom g2);

                      then

                      reconsider m = (i2 - n) as Element of NAT by A68, A74;

                      reconsider k = i1, m as Nat;

                      take k, m;

                      thus [k, m] in ( Indices G) & (g2 /. n) = (G * (k,m)) by A68, A73, A74, A83;

                    end;

                    then

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

                    now

                      let l1,l2,l3,l4 be Nat;

                      assume that

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

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

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

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

                       A89: 1 in ( dom g2);

                      reconsider m1 = (i2 - 1) as Element of NAT by A68, A74, A89;

                       [i1, (i2 - 1)] in ( Indices G) & (g2 /. 1) = (G * (i1,m1)) by A68, A73, A74, A89;

                      then

                       A90: l3 = i1 & l4 = m1 by A86, A88, GOBOARD1: 5;

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

                      then l1 = i1 & l2 = i2 by A38, A18, A19, A85, A87, GOBOARD1: 5;

                      

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

                      .= 1 by ABSVALUE:def 1;

                    end;

                    then for n be Nat st n in ( dom g) & (n + 1) in ( dom g) holds for m,k,i,j be Nat 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 A41, A75, GOBOARD1: 24;

                    hence g is_sequence_on G by A84;

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

                    

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

                    

                     A92: ( LSeg (f,k)) = ( LSeg (pj,ppi)) by A3, A13, A19, A46, A58, TOPREAL1:def 3

                    .= lk by A64, A66, A67, A91, TOPREAL3: 9;

                    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) };

                      

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

                       A94:

                      now

                        let j;

                        assume that

                         A95: ( len g1) <= j and

                         A96: j <= ( len g);

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

                        let p such that

                         A97: p = (g /. j);

                        

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

                        now

                          per cases ;

                            suppose

                             A99: j = ( len g1);

                            1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

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

                            

                            then

                             A100: (g /. ( len g1)) = (f1 /. ( len f1)) by A38, FINSEQ_4: 68

                            .= (G * (i1,i2)) by A17, A23, A14, A19, FINSEQ_4: 71;

                            hence (p `1 ) = ((G * (i1,i2)) `1 ) by A97, A99;

                            thus ((G * (i1,j2)) `2 ) <= (p `2 ) & (p `2 ) <= ((G * (i1,i2)) `2 ) by A51, A56, A54, A20, A55, A59, A63, A61, A97, A99, A100, SEQM_3:def 1;

                            thus p in ( rng l1) by A51, A55, A62, A97, A98, A99, A100, PARTFUN2: 2;

                          end;

                            suppose

                             A101: j <> ( len g1);

                            

                             A102: (w + ( len g1)) = j;

                            then

                             A103: w <= ( len g2) by A93, A96, XREAL_1: 6;

                            

                             A104: (j - ( len g1)) <> 0 by A101;

                            then

                             A105: w >= 1 by NAT_1: 14;

                            then

                             A106: w in ( dom g2) by A103, FINSEQ_3: 25;

                            then

                            reconsider u = (i2 - w) as Element of NAT by A68, A74;

                            

                             A107: (g /. j) = (g2 /. w) by A105, A102, A103, SEQ_4: 136;

                            

                             A108: (x1 . i2) = (ppi `1 ) by A51, A42, A55, A62, GOBOARD1:def 1;

                            

                             A109: u < i2 by A104, XREAL_1: 44;

                            

                             A110: (g2 /. w) = (G * (i1,u)) by A73, A74, A106;

                            

                             A111: (i2 - w) in ( Seg ( width G)) by A68, A74, A106;

                            then u in ( dom l1) by A55, FINSEQ_1:def 3;

                            then (l1 /. u) = (l1 . u) by PARTFUN1:def 6;

                            then

                             A112: (l1 /. u) = (G * (i1,u)) by A111, MATRIX_0:def 7;

                            then

                             A113: (y1 . u) = ((G * (i1,u)) `2 ) by A20, A55, A111, GOBOARD1:def 2;

                            (x1 . u) = ((G * (i1,u)) `1 ) by A42, A55, A111, A112, GOBOARD1:def 1;

                            hence (p `1 ) = ((G * (i1,i2)) `1 ) by A51, A50, A42, A55, A97, A107, A111, A110, A108, SEQM_3:def 10;

                            

                             A114: (y1 . j2) = (pj `2 ) by A56, A20, A55, A60, GOBOARD1:def 2;

                            now

                              per cases ;

                                suppose u = j2;

                                hence ((G * (i1,j2)) `2 ) <= (p `2 ) by A97, A105, A102, A103, A110, SEQ_4: 136;

                              end;

                                suppose

                                 A115: u <> j2;

                                (i2 - ( len g2)) <= u by A103, XREAL_1: 13;

                                then j2 < u by A73, A115, XXREAL_0: 1;

                                hence ((G * (i1,j2)) `2 ) <= (p `2 ) by A56, A54, A20, A55, A97, A107, A111, A110, A113, A114, SEQM_3:def 1;

                              end;

                            end;

                            hence ((G * (i1,j2)) `2 ) <= (p `2 );

                            (y1 . i2) = (ppi `2 ) by A51, A20, A55, A62, GOBOARD1:def 2;

                            hence (p `2 ) <= ((G * (i1,i2)) `2 ) by A51, A54, A20, A55, A97, A107, A111, A110, A113, A109, SEQM_3:def 1;

                            thus p in ( rng l1) by A55, A97, A98, A107, A111, A110, A112, PARTFUN2: 2;

                          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

                         A116: x in X and

                         A117: X in lg by TARSKI:def 4;

                        consider i such that

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

                         A119: 1 <= i and

                         A120: (i + 1) <= ( len g) by A117;

                        now

                          per cases ;

                            suppose

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

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

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

                            then

                             A122: i in ( dom g1) by A119, FINSEQ_3: 25;

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

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

                            then X = ( LSeg (g1,i)) by A118, A122, TOPREAL3: 18;

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

                            then

                             A123: x in ( L~ f1) by A36, A116, TARSKI:def 4;

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

                            hence thesis by A123;

                          end;

                            suppose

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

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

                            

                             A125: i <= ( len g) by A120, NAT_1: 13;

                            

                             A126: ( len g1) <= i by A124, NAT_1: 13;

                            then

                             A127: (q1 `1 ) = (ppi `1 ) by A94, A125;

                            

                             A128: (q1 `2 ) <= (ppi `2 ) by A94, A126, A125;

                            

                             A129: (pj `2 ) <= (q1 `2 ) by A94, A126, A125;

                            (q2 `1 ) = (ppi `1 ) by A94, A120, A124;

                            then

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

                            

                             A131: (q2 `2 ) <= (ppi `2 ) by A94, A120, A124;

                            

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

                            

                             A133: (pj `2 ) <= (q2 `2 ) by A94, A120, A124;

                            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 A130, A132, TOPREAL3: 9;

                                then

                                consider p2 such that

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

                                 A135: (q2 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q1 `2 ) by A116, A118;

                                (pj `2 ) <= (p2 `2 ) & (p2 `2 ) <= (ppi `2 ) by A128, A133, A135, XXREAL_0: 2;

                                then

                                 A136: x in ( LSeg (f,k)) by A92, A127, A134;

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

                                hence thesis by A136, TARSKI:def 4;

                              end;

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

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

                                then x = q1 by A116, A118, TARSKI:def 1;

                                then

                                 A137: x in ( LSeg (f,k)) by A92, A127, A129, A128;

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

                                hence thesis by A137, 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 A130, A132, TOPREAL3: 9;

                                then

                                consider p2 such that

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

                                 A139: (q1 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q2 `2 ) by A116, A118;

                                (pj `2 ) <= (p2 `2 ) & (p2 `2 ) <= (ppi `2 ) by A129, A131, A139, XXREAL_0: 2;

                                then

                                 A140: x in ( LSeg (f,k)) by A92, A127, A138;

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

                                hence thesis by A140, TARSKI:def 4;

                              end;

                            end;

                            hence thesis;

                          end;

                        end;

                        hence thesis;

                      end;

                      let x be object;

                      assume x in ( L~ f);

                      then

                       A141: x in (( L~ f1) \/ ( LSeg (f,k))) by A3, A12, Th3;

                      now

                        per cases by A141, XBOOLE_0:def 3;

                          suppose

                           A142: x in ( L~ f1);

                          ( L~ g1) c= ( L~ g) by Th6;

                          hence thesis by A36, A142;

                        end;

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

                          then

                          consider p1 such that

                           A143: p1 = x and

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

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

                           A146: (p1 `2 ) <= (ppi `2 ) by A92;

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

                           A147:

                          now

                            reconsider n = ( len g1) as Nat;

                            take n;

                            thus P2[n]

                            proof

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

                              1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

                              then

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

                              let q;

                              assume q = (g /. n);

                              

                              then q = (f1 /. ( len f1)) by A38, A148, FINSEQ_4: 68

                              .= (G * (i1,i2)) by A17, A23, A14, A19, FINSEQ_4: 71;

                              hence thesis by A146;

                            end;

                          end;

                          

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

                          consider ma be Nat such that

                           A150: P2[ma] & for n be Nat st P2[n] holds n <= ma from NAT_1:sch 6( A149, A147);

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

                          now

                            per cases ;

                              suppose

                               A151: ma = ( len g);

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

                              then

                               A152: 1 <= l by XREAL_1: 19;

                              then ( 0 + 1) <= ma by A73, A93, A151, XREAL_1: 7;

                              then

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

                              

                               A153: (m1 + 1) = ma;

                              (( len g1) + 1) <= ma by A73, A93, A151, A152, XREAL_1: 7;

                              then

                               A154: m1 >= ( len g1) by A153, XREAL_1: 6;

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

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

                              

                               A155: (i2 - l) = j2;

                              

                               A156: l in ( dom g2) by A74, A152, FINSEQ_1: 1;

                              

                              then

                               A157: (g /. ma) = (g2 /. l) by A73, A93, A151, FINSEQ_4: 69

                              .= pj by A73, A74, A156, A155;

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

                              then

                               A158: (p1 `2 ) = (pj `2 ) by A145, XXREAL_0: 1;

                              

                               A159: m1 <= ( len g) by A151, A153, NAT_1: 11;

                              then

                               A160: (q `1 ) = (ppi `1 ) by A94, A154;

                              

                               A161: (pj `2 ) <= (q `2 ) by A94, A154, A159;

                              1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

                              then

                               A162: 1 <= m1 by A154, XXREAL_0: 2;

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

                              then ( LSeg (g,m1)) = lq by A66, A91, A160, A161, TOPREAL3: 9;

                              then

                               A163: p1 in ( LSeg (g,m1)) by A144, A158, A161;

                              ( LSeg (g,m1)) in lg by A151, A153, A162;

                              hence thesis by A143, A163, TARSKI:def 4;

                            end;

                              suppose ma <> ( len g);

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

                              then

                               A164: (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 ) };

                              

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

                              

                               A166: (p1 `2 ) <= (qa `2 ) by A150;

                              

                               A167: ( len g1) <= (ma + 1) by A150, NAT_1: 13;

                              then

                               A168: (qa1 `1 ) = (ppi `1 ) by A94, A164;

                               A169:

                              now

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

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

                                then (ma + 1) <= ma by A150, A164, A167;

                                hence contradiction by XREAL_1: 29;

                              end;

                              

                               A170: (qa `1 ) = (ppi `1 ) & qa = |[(qa `1 ), (qa `2 )]| by A94, A150, EUCLID: 53;

                              

                               A171: 1 <= ma by A13, A23, A39, A150, NAT_1: 13;

                              

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

                              .= lma by A166, A169, A168, A170, A165, TOPREAL3: 9, XXREAL_0: 2;

                              then

                               A172: x in ( LSeg (g,ma)) by A143, A144, A166, A169;

                              ( LSeg (g,ma)) in lg by A171, A164;

                              hence thesis by A172, TARSKI:def 4;

                            end;

                          end;

                          hence thesis;

                        end;

                      end;

                      hence thesis;

                    end;

                    1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

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

                    

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

                    .= (f /. 1) by A17, A15, FINSEQ_4: 71;

                    

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

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

                    then

                     A174: 1 <= l by XREAL_1: 19;

                    then

                     A175: l in ( dom g2) by A74, FINSEQ_1: 1;

                    

                    hence (g /. ( len g)) = (g2 /. l) by A73, A173, FINSEQ_4: 69

                    .= (G * (i1,m1)) by A73, A74, A175

                    .= (f /. ( len f)) by A3, A46, A58;

                    thus ( len f) <= ( len g) by A3, A23, A39, A73, A174, A173, XREAL_1: 7;

                  end;

                    case i2 = j2;

                    hence contradiction by A6, A17, A19, A44, A46, A58;

                  end;

                    case

                     A176: i2 < j2;

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

                    

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

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

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

                    consider g2 such that

                     A178: ( 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);

                     A179:

                    now

                      let n;

                      

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

                      assume

                       A181: n in ( Seg l);

                      then n <= l by FINSEQ_1: 1;

                      then

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

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

                      then

                       A183: (i2 + n) <= ( width G) by A182, XXREAL_0: 2;

                      1 <= n by A181, FINSEQ_1: 1;

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

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

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

                    end;

                    

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

                    now

                      let n be Nat such that

                       A185: n in ( dom g2);

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

                      thus [m, k] in ( Indices G) & (g2 /. n) = (G * (m,k)) by A178, A179, A184, A185;

                    end;

                    then

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

                     A187:

                    now

                      let n be Nat;

                      assume that

                       A188: n in ( dom g2) and

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

                      let l1,l2,l3,l4 be Nat;

                      assume that

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

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

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

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

                      (g2 /. (n + 1)) = (G * (i1,(i2 + (n + 1)))) & [i1, (i2 + (n + 1))] in ( Indices G) by A178, A179, A184, A189;

                      then

                       A194: l3 = i1 & l4 = (i2 + (n + 1)) by A191, A193, GOBOARD1: 5;

                      (g2 /. n) = (G * (i1,(i2 + n))) & [i1, (i2 + n)] in ( Indices G) by A178, A179, A184, A188;

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

                      

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

                      .= |.( - 1).|

                      .= |.1.| by COMPLEX1: 52

                      .= 1 by ABSVALUE:def 1;

                    end;

                    now

                      let l1,l2,l3,l4 be Nat;

                      assume that

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

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

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

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

                       A199: 1 in ( dom g2);

                      (g2 /. 1) = (G * (i1,(i2 + 1))) & [i1, (i2 + 1)] in ( Indices G) by A178, A179, A184, A199;

                      then

                       A200: l3 = i1 & l4 = (i2 + 1) by A196, A198, GOBOARD1: 5;

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

                      then l1 = i1 & l2 = i2 by A38, A18, A19, A195, A197, GOBOARD1: 5;

                      

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

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

                      .= |.1.| by COMPLEX1: 52

                      .= 1 by ABSVALUE:def 1;

                    end;

                    then for n be Nat st n in ( dom g) & (n + 1) in ( dom g) holds for m,k,i,j be Nat 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 A41, A187, GOBOARD1: 24;

                    hence g is_sequence_on G by A186;

                    

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

                    j2 in ( dom l1) by A56, A55, FINSEQ_1:def 3;

                    then (l1 /. j2) = (l1 . j2) by PARTFUN1:def 6;

                    then

                     A202: (l1 /. j2) = pj by A56, MATRIX_0:def 7;

                    then

                     A203: (y1 . j2) = (pj `2 ) by A56, A20, A55, GOBOARD1:def 2;

                    i2 in ( dom l1) by A51, A55, FINSEQ_1:def 3;

                    then (l1 /. i2) = (l1 . i2) by PARTFUN1:def 6;

                    then

                     A204: (l1 /. i2) = ppi by A51, MATRIX_0:def 7;

                    then

                     A205: (y1 . i2) = (ppi `2 ) by A51, A20, A55, GOBOARD1:def 2;

                    then

                     A206: (ppi `2 ) < (pj `2 ) by A51, A56, A54, A20, A55, A176, A203, SEQM_3:def 1;

                    

                     A207: (x1 . j2) = (pj `1 ) by A56, A42, A55, A202, GOBOARD1:def 1;

                    (x1 . i2) = (ppi `1 ) by A51, A42, A55, A204, GOBOARD1:def 1;

                    then

                     A208: (ppi `1 ) = (pj `1 ) by A51, A56, A50, A42, A55, A207, SEQM_3:def 10;

                    

                     A209: ( LSeg (f,k)) = ( LSeg (ppi,pj)) by A3, A13, A19, A46, A58, TOPREAL1:def 3

                    .= lk by A206, A208, A177, A201, TOPREAL3: 9;

                    

                     A210: ( dom g2) = ( Seg l) by A178, FINSEQ_1:def 3;

                    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) };

                      

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

                       A212:

                      now

                        let j;

                        assume that

                         A213: ( len g1) <= j and

                         A214: j <= ( len g);

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

                        let p such that

                         A215: p = (g /. j);

                        set u = (i2 + w);

                        

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

                        now

                          per cases ;

                            suppose

                             A217: j = ( len g1);

                            1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

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

                            

                            then

                             A218: (g /. ( len g1)) = (f1 /. ( len f1)) by A38, FINSEQ_4: 68

                            .= (G * (i1,i2)) by A17, A23, A14, A19, FINSEQ_4: 71;

                            hence (p `1 ) = ((G * (i1,i2)) `1 ) by A215, A217;

                            thus ((G * (i1,i2)) `2 ) <= (p `2 ) & (p `2 ) <= ((G * (i1,j2)) `2 ) by A51, A56, A54, A20, A55, A176, A205, A203, A215, A217, A218, SEQM_3:def 1;

                            thus p in ( rng l1) by A51, A55, A204, A215, A216, A217, A218, PARTFUN2: 2;

                          end;

                            suppose

                             A219: j <> ( len g1);

                            

                             A220: (w + ( len g1)) = j;

                            then

                             A221: w <= ( len g2) by A211, A214, XREAL_1: 6;

                            

                             A222: (x1 . i2) = (ppi `1 ) by A51, A42, A55, A204, GOBOARD1:def 1;

                            

                             A223: (j - ( len g1)) <> 0 by A219;

                            then

                             A224: w >= 1 by NAT_1: 14;

                            then

                             A225: (g /. j) = (g2 /. w) by A220, A221, SEQ_4: 136;

                            

                             A226: i2 < u by A223, XREAL_1: 29;

                            

                             A227: w in ( dom g2) by A224, A221, FINSEQ_3: 25;

                            then

                             A228: u in ( Seg ( width G)) by A210, A179;

                            u in ( Seg ( width G)) by A210, A179, A227;

                            then u in ( dom l1) by A55, FINSEQ_1:def 3;

                            then (l1 /. u) = (l1 . u) by PARTFUN1:def 6;

                            then

                             A229: (l1 /. u) = (G * (i1,u)) by A228, MATRIX_0:def 7;

                            then

                             A230: (y1 . u) = ((G * (i1,u)) `2 ) by A20, A55, A228, GOBOARD1:def 2;

                            

                             A231: (g2 /. w) = (G * (i1,u)) by A178, A227;

                            (x1 . u) = ((G * (i1,u)) `1 ) by A42, A55, A228, A229, GOBOARD1:def 1;

                            hence (p `1 ) = ((G * (i1,i2)) `1 ) by A51, A50, A42, A55, A215, A225, A231, A228, A222, SEQM_3:def 10;

                            (y1 . i2) = (ppi `2 ) by A51, A20, A55, A204, GOBOARD1:def 2;

                            hence ((G * (i1,i2)) `2 ) <= (p `2 ) by A51, A54, A20, A55, A215, A225, A231, A228, A230, A226, SEQM_3:def 1;

                            

                             A232: (y1 . j2) = (pj `2 ) by A56, A20, A55, A202, GOBOARD1:def 2;

                            now

                              per cases ;

                                suppose u = j2;

                                hence (p `2 ) <= ((G * (i1,j2)) `2 ) by A215, A224, A220, A221, A231, SEQ_4: 136;

                              end;

                                suppose

                                 A233: u <> j2;

                                u <= (i2 + l) by A178, A221, XREAL_1: 7;

                                then u < j2 by A233, XXREAL_0: 1;

                                hence (p `2 ) <= ((G * (i1,j2)) `2 ) by A56, A54, A20, A55, A215, A225, A231, A228, A230, A232, SEQM_3:def 1;

                              end;

                            end;

                            hence (p `2 ) <= ((G * (i1,j2)) `2 );

                            thus p in ( rng l1) by A55, A215, A216, A225, A231, A228, A229, PARTFUN2: 2;

                          end;

                        end;

                        hence (p `1 ) = (ppi `1 ) & (ppi `2 ) <= (p `2 ) & (p `2 ) <= (pj `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

                         A234: x in X and

                         A235: X in lg by TARSKI:def 4;

                        consider i such that

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

                         A237: 1 <= i and

                         A238: (i + 1) <= ( len g) by A235;

                        now

                          per cases ;

                            suppose

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

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

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

                            then

                             A240: i in ( dom g1) by A237, FINSEQ_3: 25;

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

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

                            then X = ( LSeg (g1,i)) by A236, A240, TOPREAL3: 18;

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

                            then

                             A241: x in ( L~ f1) by A36, A234, TARSKI:def 4;

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

                            hence thesis by A241;

                          end;

                            suppose

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

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

                            

                             A243: i <= ( len g) by A238, NAT_1: 13;

                            

                             A244: ( len g1) <= i by A242, NAT_1: 13;

                            then

                             A245: (q1 `1 ) = (ppi `1 ) by A212, A243;

                            

                             A246: (q1 `2 ) <= (pj `2 ) by A212, A244, A243;

                            

                             A247: (ppi `2 ) <= (q1 `2 ) by A212, A244, A243;

                            (q2 `1 ) = (ppi `1 ) by A212, A238, A242;

                            then

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

                            

                             A249: (q2 `2 ) <= (pj `2 ) by A212, A238, A242;

                            

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

                            

                             A251: (ppi `2 ) <= (q2 `2 ) by A212, A238, A242;

                            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 A248, A250, TOPREAL3: 9;

                                then

                                consider p2 such that

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

                                 A253: (q2 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q1 `2 ) by A234, A236;

                                (ppi `2 ) <= (p2 `2 ) & (p2 `2 ) <= (pj `2 ) by A246, A251, A253, XXREAL_0: 2;

                                then

                                 A254: x in ( LSeg (f,k)) by A209, A245, A252;

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

                                hence thesis by A254, TARSKI:def 4;

                              end;

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

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

                                then x = q1 by A234, A236, TARSKI:def 1;

                                then

                                 A255: x in ( LSeg (f,k)) by A209, A245, A247, A246;

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

                                hence thesis by A255, 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 A248, A250, TOPREAL3: 9;

                                then

                                consider p2 such that

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

                                 A257: (q1 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q2 `2 ) by A234, A236;

                                (ppi `2 ) <= (p2 `2 ) & (p2 `2 ) <= (pj `2 ) by A247, A249, A257, XXREAL_0: 2;

                                then

                                 A258: x in ( LSeg (f,k)) by A209, A245, A256;

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

                                hence thesis by A258, TARSKI:def 4;

                              end;

                            end;

                            hence thesis;

                          end;

                        end;

                        hence thesis;

                      end;

                      let x be object;

                      assume x in ( L~ f);

                      then

                       A259: x in (( L~ f1) \/ ( LSeg (f,k))) by A3, A12, Th3;

                      now

                        per cases by A259, XBOOLE_0:def 3;

                          suppose

                           A260: x in ( L~ f1);

                          ( L~ g1) c= ( L~ g) by Th6;

                          hence thesis by A36, A260;

                        end;

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

                          then

                          consider p1 such that

                           A261: p1 = x and

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

                           A263: (ppi `2 ) <= (p1 `2 ) and

                           A264: (p1 `2 ) <= (pj `2 ) by A209;

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

                           A265:

                          now

                            reconsider n = ( len g1) as Nat;

                            take n;

                            thus P2[n]

                            proof

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

                              1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

                              then

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

                              let q;

                              assume q = (g /. n);

                              

                              then q = (f1 /. ( len f1)) by A38, A266, FINSEQ_4: 68

                              .= (G * (i1,i2)) by A17, A23, A14, A19, FINSEQ_4: 71;

                              hence thesis by A263;

                            end;

                          end;

                          

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

                          consider ma be Nat such that

                           A268: P2[ma] & for n be Nat st P2[n] holds n <= ma from NAT_1:sch 6( A267, A265);

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

                          now

                            per cases ;

                              suppose

                               A269: ma = ( len g);

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

                              then

                               A270: 1 <= l by XREAL_1: 19;

                              then ( 0 + 1) <= ma by A178, A211, A269, XREAL_1: 7;

                              then

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

                              

                               A271: (m1 + 1) = ma;

                              (( len g1) + 1) <= ma by A178, A211, A269, A270, XREAL_1: 7;

                              then

                               A272: m1 >= ( len g1) by A271, XREAL_1: 6;

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

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

                              

                               A273: (i2 + l) = j2;

                              

                               A274: l in ( dom g2) by A178, A270, FINSEQ_3: 25;

                              

                              then

                               A275: (g /. ma) = (g2 /. l) by A178, A211, A269, FINSEQ_4: 69

                              .= pj by A178, A274, A273;

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

                              then

                               A276: (p1 `2 ) = (pj `2 ) by A264, XXREAL_0: 1;

                              

                               A277: m1 <= ( len g) by A269, A271, NAT_1: 11;

                              then

                               A278: (q `1 ) = (ppi `1 ) by A212, A272;

                              

                               A279: (q `2 ) <= (pj `2 ) by A212, A272, A277;

                              1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

                              then

                               A280: 1 <= m1 by A272, XXREAL_0: 2;

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

                              then ( LSeg (g,m1)) = lq by A208, A201, A278, A279, TOPREAL3: 9;

                              then

                               A281: p1 in ( LSeg (g,m1)) by A262, A276, A279;

                              ( LSeg (g,m1)) in lg by A269, A271, A280;

                              hence thesis by A261, A281, TARSKI:def 4;

                            end;

                              suppose ma <> ( len g);

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

                              then

                               A282: (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 ) };

                              

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

                              

                               A284: (qa `2 ) <= (p1 `2 ) by A268;

                              

                               A285: ( len g1) <= (ma + 1) by A268, NAT_1: 13;

                              then

                               A286: (qa1 `1 ) = (ppi `1 ) by A212, A282;

                               A287:

                              now

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

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

                                then (ma + 1) <= ma by A268, A282, A285;

                                hence contradiction by XREAL_1: 29;

                              end;

                              

                               A288: (qa `1 ) = (ppi `1 ) & qa = |[(qa `1 ), (qa `2 )]| by A212, A268, EUCLID: 53;

                              

                               A289: 1 <= ma by A13, A23, A39, A268, NAT_1: 13;

                              

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

                              .= lma by A284, A287, A286, A288, A283, TOPREAL3: 9, XXREAL_0: 2;

                              then

                               A290: x in ( LSeg (g,ma)) by A261, A262, A284, A287;

                              ( LSeg (g,ma)) in lg by A289, A282;

                              hence thesis by A290, TARSKI:def 4;

                            end;

                          end;

                          hence thesis;

                        end;

                      end;

                      hence thesis;

                    end;

                    1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

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

                    

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

                    .= (f /. 1) by A17, A15, FINSEQ_4: 71;

                    

                     A291: ( len g) = (( len g1) + l) by A178, FINSEQ_1: 22;

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

                    then

                     A292: 1 <= l by XREAL_1: 19;

                    then

                     A293: l in ( dom g2) by A178, A184, FINSEQ_1: 1;

                    

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

                    .= (G * (i1,(i2 + l))) by A178, A293

                    .= (f /. ( len f)) by A3, A46, A58;

                    thus ( len f) <= ( len g) by A3, A23, A39, A292, A291, XREAL_1: 7;

                  end;

                end;

                hence thesis;

              end;

                suppose

                 A294: i2 = j2;

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

                now

                  per cases by XXREAL_0: 1;

                    case

                     A295: i1 > j1;

                    (c1 /. j1) = (c1 . j1) by A48, A43, PARTFUN1:def 6;

                    then

                     A296: (c1 /. j1) = pj by A48, MATRIX_0:def 8;

                    then

                     A297: (x2 . j1) = (pj `1 ) by A48, A43, A22, GOBOARD1:def 1;

                    (c1 /. i1) = (c1 . i1) by A49, A43, PARTFUN1:def 6;

                    then

                     A298: (c1 /. i1) = ppi by A49, MATRIX_0:def 8;

                    then

                     A299: (x2 . i1) = (ppi `1 ) by A49, A43, A22, GOBOARD1:def 1;

                    then

                     A300: (pj `1 ) < (ppi `1 ) by A49, A48, A52, A43, A22, A295, A297, SEQM_3:def 1;

                    

                     A301: (y2 . j1) = (pj `2 ) by A48, A43, A21, A296, GOBOARD1:def 2;

                    (y2 . i1) = (ppi `2 ) by A49, A43, A21, A298, GOBOARD1:def 2;

                    then

                     A302: (ppi `2 ) = (pj `2 ) by A49, A48, A53, A43, A21, A301, SEQM_3:def 10;

                    reconsider l = (i1 - j1) as Element of NAT by A295, 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 ) };

                    

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

                     A304:

                    now

                      let n;

                      assume n in ( Seg l);

                      then

                       A305: n <= l by FINSEQ_1: 1;

                      l <= i1 by XREAL_1: 43;

                      then

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

                      (i1 - n) <= i1 & i1 <= ( len G) by A49, FINSEQ_3: 25, XREAL_1: 43;

                      then

                       A306: w <= ( len G) by XXREAL_0: 2;

                      

                       A307: 1 <= j1 by A48, FINSEQ_3: 25;

                      (i1 - l) <= (i1 - n) by A305, XREAL_1: 13;

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

                      then w in ( dom G) by A306, FINSEQ_3: 25;

                      hence (i1 - n) is Element of NAT & [(i1 - n), i2] in ( Indices G) & (i1 - n) in ( dom G) by A47, A51, ZFMISC_1: 87;

                    end;

                     A308:

                    now

                      let n be Nat;

                      assume n in ( Seg l);

                      then

                      reconsider m = (i1 - n) as Element of NAT by A304;

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

                      thus P1[n, p];

                    end;

                    consider g2 such that

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

                    take g = (g1 ^ g2);

                    

                     A310: ( dom g2) = ( Seg l) by A309, FINSEQ_1:def 3;

                     A311:

                    now

                      let n be Nat;

                      assume that

                       A312: n in ( dom g2) and

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

                      reconsider m1 = (i1 - n), m2 = (i1 - (n + 1)) as Element of NAT by A304, A310, A312, A313;

                      let l1,l2,l3,l4 be Nat;

                      assume that

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

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

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

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

                       [(i1 - (n + 1)), i2] in ( Indices G) & (g2 /. (n + 1)) = (G * (m2,i2)) by A304, A309, A310, A313;

                      then

                       A318: l3 = m2 & l4 = i2 by A315, A317, GOBOARD1: 5;

                       [(i1 - n), i2] in ( Indices G) & (g2 /. n) = (G * (m1,i2)) by A304, A309, A310, A312;

                      then l1 = m1 & l2 = i2 by A314, A316, GOBOARD1: 5;

                      

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

                      .= 1 by ABSVALUE:def 1;

                    end;

                    now

                      let n be Nat;

                      assume

                       A319: n in ( dom g2);

                      then

                      reconsider m = (i1 - n) as Element of NAT by A304, A310;

                      reconsider m, k = i2 as Nat;

                      take m, k;

                      thus [m, k] in ( Indices G) & (g2 /. n) = (G * (m,k)) by A304, A309, A310, A319;

                    end;

                    then

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

                    now

                      let l1,l2,l3,l4 be Nat;

                      assume that

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

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

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

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

                       A325: 1 in ( dom g2);

                      reconsider m1 = (i1 - 1) as Element of NAT by A304, A310, A325;

                       [(i1 - 1), i2] in ( Indices G) & (g2 /. 1) = (G * (m1,i2)) by A304, A309, A310, A325;

                      then

                       A326: l3 = m1 & l4 = i2 by A322, A324, GOBOARD1: 5;

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

                      then l1 = i1 & l2 = i2 by A38, A18, A19, A321, A323, GOBOARD1: 5;

                      

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

                      .= 1 by ABSVALUE:def 1;

                    end;

                    then for n be Nat st n in ( dom g) & (n + 1) in ( dom g) holds for m,k,i,j be Nat 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 A41, A311, GOBOARD1: 24;

                    hence g is_sequence_on G by A320;

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

                    

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

                    

                     A328: ( LSeg (f,k)) = ( LSeg (pj,ppi)) by A3, A13, A19, A46, A294, TOPREAL1:def 3

                    .= lk by A300, A302, A303, A327, TOPREAL3: 10;

                    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) };

                      

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

                       A330:

                      now

                        let j;

                        assume that

                         A331: ( len g1) <= j and

                         A332: j <= ( len g);

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

                        let p such that

                         A333: p = (g /. j);

                        now

                          per cases ;

                            suppose

                             A334: j = ( len g1);

                            1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

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

                            

                            then

                             A335: (g /. ( len g1)) = (f1 /. ( len f1)) by A38, FINSEQ_4: 68

                            .= (G * (i1,i2)) by A17, A23, A14, A19, FINSEQ_4: 71;

                            hence (p `2 ) = ((G * (i1,i2)) `2 ) by A333, A334;

                            thus ((G * (j1,i2)) `1 ) <= (p `1 ) & (p `1 ) <= ((G * (i1,i2)) `1 ) by A49, A48, A52, A43, A22, A295, A299, A297, A333, A334, A335, SEQM_3:def 1;

                            thus p in ( rng c1) by A49, A43, A298, A333, A334, A335, PARTFUN2: 2;

                          end;

                            suppose

                             A336: j <> ( len g1);

                            

                             A337: (w + ( len g1)) = j;

                            then

                             A338: w <= ( len g2) by A329, A332, XREAL_1: 6;

                            

                             A339: (j - ( len g1)) <> 0 by A336;

                            then

                             A340: w >= 1 by NAT_1: 14;

                            then

                             A341: w in ( dom g2) by A338, FINSEQ_3: 25;

                            then

                            reconsider u = (i1 - w) as Element of NAT by A304, A310;

                            

                             A342: (g /. j) = (g2 /. w) by A340, A337, A338, SEQ_4: 136;

                            

                             A343: u < i1 by A339, XREAL_1: 44;

                            

                             A344: (g2 /. w) = (G * (u,i2)) by A309, A310, A341;

                            

                             A345: (y2 . i1) = ((G * (i1,i2)) `2 ) by A49, A43, A21, A298, GOBOARD1:def 2;

                            

                             A346: (i1 - w) in ( dom G) by A304, A310, A341;

                            (c1 /. u) = (c1 . u) by A43, A304, A310, A341, PARTFUN1:def 6;

                            then

                             A347: (c1 /. u) = (G * (u,i2)) by A346, MATRIX_0:def 8;

                            then

                             A348: (x2 . u) = ((G * (u,i2)) `1 ) by A43, A22, A346, GOBOARD1:def 1;

                            (y2 . u) = ((G * (u,i2)) `2 ) by A43, A21, A346, A347, GOBOARD1:def 2;

                            hence (p `2 ) = ((G * (i1,i2)) `2 ) by A49, A53, A43, A21, A333, A342, A346, A344, A345, SEQM_3:def 10;

                            

                             A349: (x2 . j1) = ((G * (j1,i2)) `1 ) by A48, A43, A22, A296, GOBOARD1:def 1;

                            now

                              per cases ;

                                suppose u = j1;

                                hence ((G * (j1,i2)) `1 ) <= (p `1 ) by A333, A340, A337, A338, A344, SEQ_4: 136;

                              end;

                                suppose

                                 A350: u <> j1;

                                (i1 - ( len g2)) <= u by A338, XREAL_1: 13;

                                then j1 < u by A309, A350, XXREAL_0: 1;

                                hence ((G * (j1,i2)) `1 ) <= (p `1 ) by A48, A52, A43, A22, A333, A342, A346, A344, A348, A349, SEQM_3:def 1;

                              end;

                            end;

                            hence ((G * (j1,i2)) `1 ) <= (p `1 );

                            (x2 . i1) = ((G * (i1,i2)) `1 ) by A49, A43, A22, A298, GOBOARD1:def 1;

                            hence (p `1 ) <= ((G * (i1,i2)) `1 ) by A49, A52, A43, A22, A333, A342, A346, A344, A348, A343, SEQM_3:def 1;

                            thus p in ( rng c1) by A43, A333, A342, A346, A344, A347, PARTFUN2: 2;

                          end;

                        end;

                        hence (p `2 ) = (ppi `2 ) & (pj `1 ) <= (p `1 ) & (p `1 ) <= (ppi `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

                         A351: x in X and

                         A352: X in lg by TARSKI:def 4;

                        consider i such that

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

                         A354: 1 <= i and

                         A355: (i + 1) <= ( len g) by A352;

                        now

                          per cases ;

                            suppose

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

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

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

                            then

                             A357: i in ( dom g1) by A354, FINSEQ_3: 25;

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

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

                            then X = ( LSeg (g1,i)) by A353, A357, TOPREAL3: 18;

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

                            then

                             A358: x in ( L~ f1) by A36, A351, TARSKI:def 4;

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

                            hence thesis by A358;

                          end;

                            suppose

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

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

                            

                             A360: i <= ( len g) by A355, NAT_1: 13;

                            

                             A361: ( len g1) <= i by A359, NAT_1: 13;

                            then

                             A362: (q1 `2 ) = (ppi `2 ) by A330, A360;

                            

                             A363: (q1 `1 ) <= (ppi `1 ) by A330, A361, A360;

                            

                             A364: (pj `1 ) <= (q1 `1 ) by A330, A361, A360;

                            (q2 `2 ) = (ppi `2 ) by A330, A355, A359;

                            then

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

                            

                             A366: (q2 `1 ) <= (ppi `1 ) by A330, A355, A359;

                            

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

                            

                             A368: (pj `1 ) <= (q2 `1 ) by A330, A355, A359;

                            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 A365, A367, TOPREAL3: 10;

                                then

                                consider p2 such that

                                 A369: p2 = x & (p2 `2 ) = (q1 `2 ) and

                                 A370: (q2 `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q1 `1 ) by A351, A353;

                                (pj `1 ) <= (p2 `1 ) & (p2 `1 ) <= (ppi `1 ) by A363, A368, A370, XXREAL_0: 2;

                                then

                                 A371: x in ( LSeg (f,k)) by A328, A362, A369;

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

                                hence thesis by A371, TARSKI:def 4;

                              end;

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

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

                                then x = q1 by A351, A353, TARSKI:def 1;

                                then

                                 A372: x in ( LSeg (f,k)) by A328, A362, A364, A363;

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

                                hence thesis by A372, 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 A365, A367, TOPREAL3: 10;

                                then

                                consider p2 such that

                                 A373: p2 = x & (p2 `2 ) = (q1 `2 ) and

                                 A374: (q1 `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q2 `1 ) by A351, A353;

                                (pj `1 ) <= (p2 `1 ) & (p2 `1 ) <= (ppi `1 ) by A364, A366, A374, XXREAL_0: 2;

                                then

                                 A375: x in ( LSeg (f,k)) by A328, A362, A373;

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

                                hence thesis by A375, TARSKI:def 4;

                              end;

                            end;

                            hence thesis;

                          end;

                        end;

                        hence thesis;

                      end;

                      let x be object;

                      assume x in ( L~ f);

                      then

                       A376: x in (( L~ f1) \/ ( LSeg (f,k))) by A3, A12, Th3;

                      now

                        per cases by A376, XBOOLE_0:def 3;

                          suppose

                           A377: x in ( L~ f1);

                          ( L~ g1) c= ( L~ g) by Th6;

                          hence thesis by A36, A377;

                        end;

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

                          then

                          consider p1 such that

                           A378: p1 = x and

                           A379: (p1 `2 ) = (ppi `2 ) and

                           A380: (pj `1 ) <= (p1 `1 ) and

                           A381: (p1 `1 ) <= (ppi `1 ) by A328;

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

                           A382:

                          now

                            reconsider n = ( len g1) as Nat;

                            take n;

                            thus P2[n]

                            proof

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

                              1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

                              then

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

                              let q;

                              assume q = (g /. n);

                              

                              then q = (f1 /. ( len f1)) by A38, A383, FINSEQ_4: 68

                              .= (G * (i1,i2)) by A17, A23, A14, A19, FINSEQ_4: 71;

                              hence thesis by A381;

                            end;

                          end;

                          

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

                          consider ma be Nat such that

                           A385: P2[ma] & for n be Nat st P2[n] holds n <= ma from NAT_1:sch 6( A384, A382);

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

                          now

                            per cases ;

                              suppose

                               A386: ma = ( len g);

                              (j1 + 1) <= i1 by A295, NAT_1: 13;

                              then

                               A387: 1 <= l by XREAL_1: 19;

                              then ( 0 + 1) <= ma by A309, A329, A386, XREAL_1: 7;

                              then

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

                              

                               A388: (m1 + 1) = ma;

                              (( len g1) + 1) <= ma by A309, A329, A386, A387, XREAL_1: 7;

                              then

                               A389: m1 >= ( len g1) by A388, XREAL_1: 6;

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

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

                              

                               A390: (i1 - l) = j1;

                              

                               A391: l in ( dom g2) by A310, A387, FINSEQ_1: 1;

                              

                              then

                               A392: (g /. ma) = (g2 /. l) by A309, A329, A386, FINSEQ_4: 69

                              .= pj by A309, A310, A391, A390;

                              then (p1 `1 ) <= (pj `1 ) by A385;

                              then

                               A393: (p1 `1 ) = (pj `1 ) by A380, XXREAL_0: 1;

                              

                               A394: m1 <= ( len g) by A386, A388, NAT_1: 11;

                              then

                               A395: (q `2 ) = (ppi `2 ) by A330, A389;

                              

                               A396: (pj `1 ) <= (q `1 ) by A330, A389, A394;

                              1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

                              then

                               A397: 1 <= m1 by A389, XXREAL_0: 2;

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

                              then ( LSeg (g,m1)) = lq by A302, A327, A395, A396, TOPREAL3: 10;

                              then

                               A398: p1 in ( LSeg (g,m1)) by A379, A393, A396;

                              ( LSeg (g,m1)) in lg by A386, A388, A397;

                              hence thesis by A378, A398, TARSKI:def 4;

                            end;

                              suppose ma <> ( len g);

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

                              then

                               A399: (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 ) };

                              

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

                              

                               A401: (p1 `1 ) <= (qa `1 ) by A385;

                              

                               A402: ( len g1) <= (ma + 1) by A385, NAT_1: 13;

                              then

                               A403: (qa1 `2 ) = (ppi `2 ) by A330, A399;

                               A404:

                              now

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

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

                                then (ma + 1) <= ma by A385, A399, A402;

                                hence contradiction by XREAL_1: 29;

                              end;

                              

                               A405: (qa `2 ) = (ppi `2 ) & qa = |[(qa `1 ), (qa `2 )]| by A330, A385, EUCLID: 53;

                              

                               A406: 1 <= ma by A13, A23, A39, A385, NAT_1: 13;

                              

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

                              .= lma by A401, A404, A403, A405, A400, TOPREAL3: 10, XXREAL_0: 2;

                              then

                               A407: x in ( LSeg (g,ma)) by A378, A379, A401, A404;

                              ( LSeg (g,ma)) in lg by A406, A399;

                              hence thesis by A407, TARSKI:def 4;

                            end;

                          end;

                          hence thesis;

                        end;

                      end;

                      hence thesis;

                    end;

                    1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

                    then 1 in ( dom g1) by A57, FINSEQ_1: 1;

                    

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

                    .= (f /. 1) by A17, A15, FINSEQ_4: 71;

                    

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

                    (j1 + 1) <= i1 by A295, NAT_1: 13;

                    then

                     A409: 1 <= l by XREAL_1: 19;

                    then

                     A410: l in ( dom g2) by A310, FINSEQ_1: 1;

                    

                    hence (g /. ( len g)) = (g2 /. l) by A309, A408, FINSEQ_4: 69

                    .= (G * (m1,i2)) by A309, A310, A410

                    .= (f /. ( len f)) by A3, A46, A294;

                    thus ( len f) <= ( len g) by A3, A23, A39, A309, A409, A408, XREAL_1: 7;

                  end;

                    case i1 = j1;

                    hence contradiction by A6, A17, A19, A44, A46, A294;

                  end;

                    case

                     A411: i1 < j1;

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

                    

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

                    reconsider l = (j1 - i1) as Element of NAT by A411, INT_1: 5;

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

                    consider g2 such that

                     A413: ( 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);

                     A414:

                    now

                      let n;

                      

                       A415: n <= (i1 + n) by NAT_1: 11;

                      assume

                       A416: n in ( Seg l);

                      then n <= l by FINSEQ_1: 1;

                      then

                       A417: (i1 + n) <= (l + i1) by XREAL_1: 7;

                      j1 <= ( len G) by A48, FINSEQ_3: 25;

                      then

                       A418: (i1 + n) <= ( len G) by A417, XXREAL_0: 2;

                      1 <= n by A416, FINSEQ_1: 1;

                      then 1 <= (i1 + n) by A415, XXREAL_0: 2;

                      hence (i1 + n) in ( dom G) by A418, FINSEQ_3: 25;

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

                    end;

                    

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

                    now

                      let n be Nat such that

                       A420: n in ( dom g2);

                      reconsider m = (i1 + n), k = i2 as Nat;

                      take m, k;

                      thus [m, k] in ( Indices G) & (g2 /. n) = (G * (m,k)) by A413, A414, A419, A420;

                    end;

                    then

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

                     A422:

                    now

                      let n be Nat;

                      assume that

                       A423: n in ( dom g2) and

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

                      let l1,l2,l3,l4 be Nat;

                      assume that

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

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

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

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

                      (g2 /. (n + 1)) = (G * ((i1 + (n + 1)),i2)) & [(i1 + (n + 1)), i2] in ( Indices G) by A413, A414, A419, A424;

                      then

                       A429: l3 = (i1 + (n + 1)) & l4 = i2 by A426, A428, GOBOARD1: 5;

                      (g2 /. n) = (G * ((i1 + n),i2)) & [(i1 + n), i2] in ( Indices G) by A413, A414, A419, A423;

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

                      

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

                      .= |.( - 1).|

                      .= |.1.| by COMPLEX1: 52

                      .= 1 by ABSVALUE:def 1;

                    end;

                    now

                      let l1,l2,l3,l4 be Nat;

                      assume that

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

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

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

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

                       A434: 1 in ( dom g2);

                      (g2 /. 1) = (G * ((i1 + 1),i2)) & [(i1 + 1), i2] in ( Indices G) by A413, A414, A419, A434;

                      then

                       A435: l3 = (i1 + 1) & l4 = i2 by A431, A433, GOBOARD1: 5;

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

                      then l1 = i1 & l2 = i2 by A38, A18, A19, A430, A432, GOBOARD1: 5;

                      

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

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

                      .= |.1.| by COMPLEX1: 52

                      .= 1 by ABSVALUE:def 1;

                    end;

                    then for n be Nat st n in ( dom g) & (n + 1) in ( dom g) holds for m,k,i,j be Nat 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 A41, A422, GOBOARD1: 24;

                    hence g is_sequence_on G by A421;

                    

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

                    (c1 /. j1) = (c1 . j1) by A48, A43, PARTFUN1:def 6;

                    then

                     A437: (c1 /. j1) = pj by A48, MATRIX_0:def 8;

                    then

                     A438: (x2 . j1) = (pj `1 ) by A48, A43, A22, GOBOARD1:def 1;

                    (c1 /. i1) = (c1 . i1) by A49, A43, PARTFUN1:def 6;

                    then

                     A439: (c1 /. i1) = ppi by A49, MATRIX_0:def 8;

                    then

                     A440: (x2 . i1) = (ppi `1 ) by A49, A43, A22, GOBOARD1:def 1;

                    then

                     A441: (ppi `1 ) < (pj `1 ) by A49, A48, A52, A43, A22, A411, A438, SEQM_3:def 1;

                    

                     A442: (y2 . j1) = (pj `2 ) by A48, A43, A21, A437, GOBOARD1:def 2;

                    (y2 . i1) = (ppi `2 ) by A49, A43, A21, A439, GOBOARD1:def 2;

                    then

                     A443: (ppi `2 ) = (pj `2 ) by A49, A48, A53, A43, A21, A442, SEQM_3:def 10;

                    

                     A444: ( LSeg (f,k)) = ( LSeg (ppi,pj)) by A3, A13, A19, A46, A294, TOPREAL1:def 3

                    .= lk by A441, A443, A412, A436, TOPREAL3: 10;

                    

                     A445: ( dom g2) = ( Seg l) by A413, FINSEQ_1:def 3;

                    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) };

                      

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

                       A447:

                      now

                        let j;

                        assume that

                         A448: ( len g1) <= j and

                         A449: j <= ( len g);

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

                        set u = (i1 + w);

                        let p such that

                         A450: p = (g /. j);

                        now

                          per cases ;

                            suppose

                             A451: j = ( len g1);

                            1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

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

                            

                            then

                             A452: (g /. ( len g1)) = (f1 /. ( len f1)) by A38, FINSEQ_4: 68

                            .= (G * (i1,i2)) by A17, A23, A14, A19, FINSEQ_4: 71;

                            hence (p `2 ) = ((G * (i1,i2)) `2 ) by A450, A451;

                            thus ((G * (i1,i2)) `1 ) <= (p `1 ) & (p `1 ) <= ((G * (j1,i2)) `1 ) by A49, A48, A52, A43, A22, A411, A440, A438, A450, A451, A452, SEQM_3:def 1;

                            thus p in ( rng c1) by A49, A43, A439, A450, A451, A452, PARTFUN2: 2;

                          end;

                            suppose

                             A453: j <> ( len g1);

                            

                             A454: (w + ( len g1)) = j;

                            then

                             A455: w <= ( len g2) by A446, A449, XREAL_1: 6;

                            

                             A456: (y2 . i1) = ((G * (i1,i2)) `2 ) by A49, A43, A21, A439, GOBOARD1:def 2;

                            

                             A457: (j - ( len g1)) <> 0 by A453;

                            then

                             A458: w >= 1 by NAT_1: 14;

                            then

                             A459: (g /. j) = (g2 /. w) by A454, A455, SEQ_4: 136;

                            

                             A460: i1 < u by A457, XREAL_1: 29;

                            

                             A461: w in ( dom g2) by A458, A455, FINSEQ_3: 25;

                            then

                             A462: u in ( dom G) by A445, A414;

                            (c1 /. u) = (c1 . u) by A43, A445, A414, A461, PARTFUN1:def 6;

                            then

                             A463: (c1 /. u) = (G * (u,i2)) by A462, MATRIX_0:def 8;

                            then

                             A464: (x2 . u) = ((G * (u,i2)) `1 ) by A43, A22, A462, GOBOARD1:def 1;

                            

                             A465: (g2 /. w) = (G * (u,i2)) by A413, A461;

                            (y2 . u) = ((G * (u,i2)) `2 ) by A43, A21, A462, A463, GOBOARD1:def 2;

                            hence (p `2 ) = ((G * (i1,i2)) `2 ) by A49, A53, A43, A21, A450, A459, A465, A462, A456, SEQM_3:def 10;

                            (x2 . i1) = ((G * (i1,i2)) `1 ) by A49, A43, A22, A439, GOBOARD1:def 1;

                            hence ((G * (i1,i2)) `1 ) <= (p `1 ) by A49, A52, A43, A22, A450, A459, A465, A462, A464, A460, SEQM_3:def 1;

                            

                             A466: (x2 . j1) = ((G * (j1,i2)) `1 ) by A48, A43, A22, A437, GOBOARD1:def 1;

                            now

                              per cases ;

                                suppose u = j1;

                                hence (p `1 ) <= ((G * (j1,i2)) `1 ) by A450, A458, A454, A455, A465, SEQ_4: 136;

                              end;

                                suppose

                                 A467: u <> j1;

                                u <= (i1 + l) by A413, A455, XREAL_1: 7;

                                then u < j1 by A467, XXREAL_0: 1;

                                hence (p `1 ) <= ((G * (j1,i2)) `1 ) by A48, A52, A43, A22, A450, A459, A465, A462, A464, A466, SEQM_3:def 1;

                              end;

                            end;

                            hence (p `1 ) <= ((G * (j1,i2)) `1 );

                            thus p in ( rng c1) by A43, A450, A459, A465, A462, A463, PARTFUN2: 2;

                          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

                         A468: x in X and

                         A469: X in lg by TARSKI:def 4;

                        consider i such that

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

                         A471: 1 <= i and

                         A472: (i + 1) <= ( len g) by A469;

                        now

                          per cases ;

                            suppose

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

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

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

                            then

                             A474: i in ( dom g1) by A471, FINSEQ_3: 25;

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

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

                            then X = ( LSeg (g1,i)) by A470, A474, TOPREAL3: 18;

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

                            then

                             A475: x in ( L~ f1) by A36, A468, TARSKI:def 4;

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

                            hence thesis by A475;

                          end;

                            suppose

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

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

                            

                             A477: i <= ( len g) by A472, NAT_1: 13;

                            

                             A478: ( len g1) <= i by A476, NAT_1: 13;

                            then

                             A479: (q1 `2 ) = (ppi `2 ) by A447, A477;

                            

                             A480: (q1 `1 ) <= (pj `1 ) by A447, A478, A477;

                            

                             A481: (ppi `1 ) <= (q1 `1 ) by A447, A478, A477;

                            (q2 `2 ) = (ppi `2 ) by A447, A472, A476;

                            then

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

                            

                             A483: (q2 `1 ) <= (pj `1 ) by A447, A472, A476;

                            

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

                            

                             A485: (ppi `1 ) <= (q2 `1 ) by A447, A472, A476;

                            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 A482, A484, TOPREAL3: 10;

                                then

                                consider p2 such that

                                 A486: p2 = x & (p2 `2 ) = (q1 `2 ) and

                                 A487: (q2 `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q1 `1 ) by A468, A470;

                                (ppi `1 ) <= (p2 `1 ) & (p2 `1 ) <= (pj `1 ) by A480, A485, A487, XXREAL_0: 2;

                                then

                                 A488: x in ( LSeg (f,k)) by A444, A479, A486;

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

                                hence thesis by A488, TARSKI:def 4;

                              end;

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

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

                                then x = q1 by A468, A470, TARSKI:def 1;

                                then

                                 A489: x in ( LSeg (f,k)) by A444, A479, A481, A480;

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

                                hence thesis by A489, 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 A482, A484, TOPREAL3: 10;

                                then

                                consider p2 such that

                                 A490: p2 = x & (p2 `2 ) = (q1 `2 ) and

                                 A491: (q1 `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q2 `1 ) by A468, A470;

                                (ppi `1 ) <= (p2 `1 ) & (p2 `1 ) <= (pj `1 ) by A481, A483, A491, XXREAL_0: 2;

                                then

                                 A492: x in ( LSeg (f,k)) by A444, A479, A490;

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

                                hence thesis by A492, TARSKI:def 4;

                              end;

                            end;

                            hence thesis;

                          end;

                        end;

                        hence thesis;

                      end;

                      let x be object;

                      assume x in ( L~ f);

                      then

                       A493: x in (( L~ f1) \/ ( LSeg (f,k))) by A3, A12, Th3;

                      now

                        per cases by A493, XBOOLE_0:def 3;

                          suppose

                           A494: x in ( L~ f1);

                          ( L~ g1) c= ( L~ g) by Th6;

                          hence thesis by A36, A494;

                        end;

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

                          then

                          consider p1 such that

                           A495: p1 = x and

                           A496: (p1 `2 ) = (ppi `2 ) and

                           A497: (ppi `1 ) <= (p1 `1 ) and

                           A498: (p1 `1 ) <= (pj `1 ) by A444;

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

                           A499:

                          now

                            reconsider n = ( len g1) as Nat;

                            take n;

                            thus P2[n]

                            proof

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

                              1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

                              then

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

                              let q;

                              assume q = (g /. n);

                              

                              then q = (f1 /. ( len f1)) by A38, A500, FINSEQ_4: 68

                              .= (G * (i1,i2)) by A17, A23, A14, A19, FINSEQ_4: 71;

                              hence thesis by A497;

                            end;

                          end;

                          

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

                          consider ma be Nat such that

                           A502: P2[ma] & for n be Nat st P2[n] holds n <= ma from NAT_1:sch 6( A501, A499);

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

                          now

                            per cases ;

                              suppose

                               A503: ma = ( len g);

                              (i1 + 1) <= j1 by A411, NAT_1: 13;

                              then

                               A504: 1 <= l by XREAL_1: 19;

                              then ( 0 + 1) <= ma by A413, A446, A503, XREAL_1: 7;

                              then

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

                              

                               A505: (m1 + 1) = ma;

                              (( len g1) + 1) <= ma by A413, A446, A503, A504, XREAL_1: 7;

                              then

                               A506: m1 >= ( len g1) by A505, XREAL_1: 6;

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

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

                              

                               A507: (i1 + l) = j1;

                              

                               A508: l in ( dom g2) by A413, A504, FINSEQ_3: 25;

                              

                              then

                               A509: (g /. ma) = (g2 /. l) by A413, A446, A503, FINSEQ_4: 69

                              .= pj by A413, A508, A507;

                              then (pj `1 ) <= (p1 `1 ) by A502;

                              then

                               A510: (p1 `1 ) = (pj `1 ) by A498, XXREAL_0: 1;

                              

                               A511: m1 <= ( len g) by A503, A505, NAT_1: 11;

                              then

                               A512: (q `2 ) = (ppi `2 ) by A447, A506;

                              

                               A513: (q `1 ) <= (pj `1 ) by A447, A506, A511;

                              1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

                              then

                               A514: 1 <= m1 by A506, XXREAL_0: 2;

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

                              then ( LSeg (g,m1)) = lq by A443, A436, A512, A513, TOPREAL3: 10;

                              then

                               A515: p1 in ( LSeg (g,m1)) by A496, A510, A513;

                              ( LSeg (g,m1)) in lg by A503, A505, A514;

                              hence thesis by A495, A515, TARSKI:def 4;

                            end;

                              suppose ma <> ( len g);

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

                              then

                               A516: (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 ) };

                              

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

                              

                               A518: (qa `1 ) <= (p1 `1 ) by A502;

                              

                               A519: ( len g1) <= (ma + 1) by A502, NAT_1: 13;

                              then

                               A520: (qa1 `2 ) = (ppi `2 ) by A447, A516;

                               A521:

                              now

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

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

                                then (ma + 1) <= ma by A502, A516, A519;

                                hence contradiction by XREAL_1: 29;

                              end;

                              

                               A522: (qa `2 ) = (ppi `2 ) & qa = |[(qa `1 ), (qa `2 )]| by A447, A502, EUCLID: 53;

                              

                               A523: 1 <= ma by A13, A23, A39, A502, NAT_1: 13;

                              

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

                              .= lma by A518, A521, A520, A522, A517, TOPREAL3: 10, XXREAL_0: 2;

                              then

                               A524: x in ( LSeg (g,ma)) by A495, A496, A518, A521;

                              ( LSeg (g,ma)) in lg by A523, A516;

                              hence thesis by A524, TARSKI:def 4;

                            end;

                          end;

                          hence thesis;

                        end;

                      end;

                      hence thesis;

                    end;

                    1 <= ( len g1) by A13, A23, A39, XXREAL_0: 2;

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

                    

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

                    .= (f /. 1) by A17, A15, FINSEQ_4: 71;

                    

                     A525: ( len g) = (( len g1) + l) by A413, FINSEQ_1: 22;

                    (i1 + 1) <= j1 by A411, NAT_1: 13;

                    then

                     A526: 1 <= l by XREAL_1: 19;

                    then

                     A527: l in ( dom g2) by A413, A419, FINSEQ_1: 1;

                    

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

                    .= (G * ((i1 + l),i2)) by A413, A527

                    .= (f /. ( len f)) by A3, A46, A294;

                    thus ( len f) <= ( len g) by A3, A23, A39, A526, A525, XREAL_1: 7;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A528: P[ 0 ]

      proof

        let f such that

         A529: ( len f) = 0 and

         A530: for n be Nat st n in ( dom f) holds ex i,j be Nat st [i, j] in ( Indices G) & (f /. n) = (G * (i,j)) and f is special and for n be Nat st n in ( dom f) & (n + 1) in ( dom f) holds (f /. n) <> (f /. (n + 1));

        take g = f;

        f = {} by A529;

        then for n be Nat holds n in ( dom g) & (n + 1) in ( dom g) implies for m,k,i,j be Nat 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 A530;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A528, A1);

      hence thesis;

    end;

    definition

      let v1,v2 be FinSequence of REAL ;

      assume

       A1: v1 <> {} ;

      :: GOBOARD2:def1

      func GoB (v1,v2) -> Matrix of ( TOP-REAL 2) means

      : Def1: ( len it ) = ( len v1) & ( width it ) = ( len v2) & for n,m be Nat st [n, m] in ( Indices it ) holds (it * (n,m)) = |[(v1 . n), (v2 . m)]|;

      existence

      proof

        defpred P[ Nat, Nat, Point of ( TOP-REAL 2)] means [$1, $2] in [:( dom v1), ( dom v2):] & for r, s st (v1 . $1) = r & (v2 . $2) = s holds $3 = |[r, s]|;

        

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

        

         A3: for i,j be Nat st [i, j] in [:( Seg ( len v1)), ( Seg ( len v2)):] holds ex p st P[i, j, p]

        proof

          let i,j be Nat;

          assume

           A4: [i, j] in [:( Seg ( len v1)), ( Seg ( len v2)):];

          reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 12;

          reconsider s1 = (v1 . i9), s2 = (v2 . j9) as Real;

          take |[s1, s2]|;

          thus [i, j] in [:( dom v1), ( dom v2):] by A2, A4, FINSEQ_1:def 3;

          let r, s;

          assume r = (v1 . i) & s = (v2 . j);

          hence thesis;

        end;

        consider M be Matrix of ( len v1), ( len v2), the carrier of ( TOP-REAL 2) such that

         A5: for i,j be Nat st [i, j] in ( Indices M) holds P[i, j, (M * (i,j))] from MATRIX_0:sch 2( A3);

        reconsider M as Matrix of the carrier of ( TOP-REAL 2);

        take M;

        thus ( len M) = ( len v1) & ( width M) = ( len v2) by A1, MATRIX_0: 23;

        let n,m be Nat;

        assume [n, m] in ( Indices M);

        hence thesis by A5;

      end;

      uniqueness

      proof

        let G1,G2 be Matrix of ( TOP-REAL 2);

        assume that

         A6: ( len G1) = ( len v1) & ( width G1) = ( len v2) and

         A7: for n,m be Nat st [n, m] in ( Indices G1) holds (G1 * (n,m)) = |[(v1 . n), (v2 . m)]| and

         A8: ( len G2) = ( len v1) & ( width G2) = ( len v2) and

         A9: for n,m be Nat st [n, m] in ( Indices G2) holds (G2 * (n,m)) = |[(v1 . n), (v2 . m)]|;

        

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

        now

          let n,m be Nat;

          reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def 12;

          

           A11: ( dom G1) = ( Seg ( len G1)) & ( dom G2) = ( Seg ( len G2)) by FINSEQ_1:def 3;

          reconsider r = (v1 . n9), s = (v2 . m9) as Real;

          assume

           A12: [n, m] in ( Indices G1);

          then (G1 * (n,m)) = |[r, s]| by A7;

          hence (G1 * (n,m)) = (G2 * (n,m)) by A6, A8, A9, A10, A12, A11;

        end;

        hence thesis by A6, A8, MATRIX_0: 21;

      end;

    end

    registration

      let v1,v2 be non empty FinSequence of REAL ;

      cluster ( GoB (v1,v2)) -> non empty-yielding X_equal-in-line Y_equal-in-column;

      coherence

      proof

        set M = ( GoB (v1,v2));

        

         A1: ( len M) = ( len v1) by Def1;

        then

         A2: ( dom M) = ( dom v1) by FINSEQ_3: 29;

        

         A3: ( width M) = ( len v2) by Def1;

        hence M is non empty-yielding by A1, MATRIX_0:def 10;

        

         A4: ( Indices M) = [:( dom v1), ( Seg ( len v2)):] by A3, A2, MATRIX_0:def 4;

        thus M is X_equal-in-line

        proof

          let n be Nat;

          reconsider l = ( Line (M,n)) as FinSequence of ( TOP-REAL 2);

          set x = ( X_axis l);

          assume

           A5: n in ( dom M);

          

           A6: ( len l) = ( width M) & ( dom x) = ( Seg ( len x)) by FINSEQ_1:def 3, MATRIX_0:def 7;

          

           A7: ( len x) = ( len l) by GOBOARD1:def 1;

          then

           A8: ( dom x) = ( dom l) by FINSEQ_3: 29;

          now

            let i,j be Nat;

            assume that

             A9: i in ( dom x) and

             A10: j in ( dom x);

            reconsider r = (v1 . n), s1 = (v2 . i), s2 = (v2 . j) as Real;

             [n, i] in ( Indices M) by A3, A2, A4, A5, A7, A6, A9, ZFMISC_1: 87;

            then (M * (n,i)) = |[r, s1]| by Def1;

            then

             A11: ((M * (n,i)) `1 ) = r by EUCLID: 52;

            (l /. i) = (l . i) by A8, A9, PARTFUN1:def 6;

            then (l /. i) = (M * (n,i)) by A7, A6, A9, MATRIX_0:def 7;

            then

             A12: (x . i) = r by A9, A11, GOBOARD1:def 1;

             [n, j] in ( Indices M) by A3, A2, A4, A5, A7, A6, A10, ZFMISC_1: 87;

            then (M * (n,j)) = |[r, s2]| by Def1;

            then

             A13: ((M * (n,j)) `1 ) = r by EUCLID: 52;

            (l /. j) = (l . j) by A8, A10, PARTFUN1:def 6;

            then (l /. j) = (M * (n,j)) by A7, A6, A10, MATRIX_0:def 7;

            hence (x . i) = (x . j) by A10, A13, A12, GOBOARD1:def 1;

          end;

          hence thesis by SEQM_3:def 10;

        end;

        thus M is Y_equal-in-column

        proof

          let n be Nat;

          reconsider c = ( Col (M,n)) as FinSequence of ( TOP-REAL 2);

          set y = ( Y_axis c);

          ( len y) = ( len c) by GOBOARD1:def 2;

          then

           A14: ( dom y) = ( dom c) by FINSEQ_3: 29;

          ( len c) = ( len M) by MATRIX_0:def 8;

          then

           A15: ( dom c) = ( dom M) by FINSEQ_3: 29;

          assume

           A16: n in ( Seg ( width M));

          now

            let i,j be Nat;

            assume that

             A17: i in ( dom y) and

             A18: j in ( dom y);

            reconsider r = (v2 . n), s1 = (v1 . i), s2 = (v1 . j) as Real;

             [i, n] in ( Indices M) by A3, A2, A4, A16, A14, A15, A17, ZFMISC_1: 87;

            then (M * (i,n)) = |[s1, r]| by Def1;

            then

             A19: ((M * (i,n)) `2 ) = r by EUCLID: 52;

            (c /. i) = (c . i) by A14, A17, PARTFUN1:def 6;

            then (c /. i) = (M * (i,n)) by A14, A15, A17, MATRIX_0:def 8;

            then

             A20: (y . i) = r by A17, A19, GOBOARD1:def 2;

             [j, n] in ( Indices M) by A3, A2, A4, A16, A14, A15, A18, ZFMISC_1: 87;

            then (M * (j,n)) = |[s2, r]| by Def1;

            then

             A21: ((M * (j,n)) `2 ) = r by EUCLID: 52;

            (c /. j) = (c . j) by A14, A18, PARTFUN1:def 6;

            then (c /. j) = (M * (j,n)) by A14, A15, A18, MATRIX_0:def 8;

            hence (y . i) = (y . j) by A18, A21, A20, GOBOARD1:def 2;

          end;

          hence thesis by SEQM_3:def 10;

        end;

      end;

    end

    registration

      let v1,v2 be non empty increasing FinSequence of REAL ;

      cluster ( GoB (v1,v2)) -> Y_increasing-in-line X_increasing-in-column;

      coherence

      proof

        set M = ( GoB (v1,v2));

        

         A1: ( width M) = ( len v2) by Def1;

        

         A2: ( len M) = ( len v1) by Def1;

        then

         A3: ( dom M) = ( dom v1) by FINSEQ_3: 29;

        then

         A4: ( Indices M) = [:( dom v1), ( Seg ( len v2)):] by A1, MATRIX_0:def 4;

        

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

        thus M is Y_increasing-in-line

        proof

          let n be Nat;

          reconsider l = ( Line (M,n)) as FinSequence of ( TOP-REAL 2);

          set y = ( Y_axis l);

          assume

           A6: n in ( dom M);

          

           A7: ( len l) = ( width M) & ( dom y) = ( Seg ( len y)) by FINSEQ_1:def 3, MATRIX_0:def 7;

          

           A8: ( len y) = ( len l) by GOBOARD1:def 2;

          then

           A9: ( dom y) = ( dom l) by FINSEQ_3: 29;

          now

            let i,j be Nat;

            assume that

             A10: i in ( dom y) and

             A11: j in ( dom y) and

             A12: i < j;

            reconsider r = (v1 . n), s1 = (v2 . i), s2 = (v2 . j) as Real;

             [n, j] in ( Indices M) by A1, A3, A4, A6, A8, A7, A11, ZFMISC_1: 87;

            then (M * (n,j)) = |[r, s2]| by Def1;

            then

             A13: ((M * (n,j)) `2 ) = s2 by EUCLID: 52;

            (l /. j) = (l . j) by A9, A11, PARTFUN1:def 6;

            then (l /. j) = (M * (n,j)) by A8, A7, A11, MATRIX_0:def 7;

            then

             A14: (y . j) = s2 by A11, A13, GOBOARD1:def 2;

             [n, i] in ( Indices M) by A1, A3, A4, A6, A8, A7, A10, ZFMISC_1: 87;

            then (M * (n,i)) = |[r, s1]| by Def1;

            then

             A15: ((M * (n,i)) `2 ) = s1 by EUCLID: 52;

            (l /. i) = (l . i) by A9, A10, PARTFUN1:def 6;

            then (l /. i) = (M * (n,i)) by A8, A7, A10, MATRIX_0:def 7;

            then (y . i) = s1 by A10, A15, GOBOARD1:def 2;

            hence (y . i) < (y . j) by A5, A1, A8, A7, A10, A11, A12, A14, SEQM_3:def 1;

          end;

          hence thesis by SEQM_3:def 1;

        end;

        

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

        thus M is X_increasing-in-column

        proof

          let n be Nat;

          reconsider c = ( Col (M,n)) as FinSequence of ( TOP-REAL 2);

          set x = ( X_axis c);

          assume

           A17: n in ( Seg ( width M));

          

           A18: ( len x) = ( len c) by GOBOARD1:def 1;

          then

           A19: ( dom x) = ( dom c) by FINSEQ_3: 29;

          

           A20: ( len c) = ( len M) by MATRIX_0:def 8;

          then

           A21: ( dom c) = ( dom M) by FINSEQ_3: 29;

          

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

          now

            let i,j be Nat;

            assume that

             A23: i in ( dom x) and

             A24: j in ( dom x) and

             A25: i < j;

            reconsider r = (v2 . n), s1 = (v1 . i), s2 = (v1 . j) as Real;

             [j, n] in ( Indices M) by A1, A3, A4, A17, A19, A21, A24, ZFMISC_1: 87;

            then (M * (j,n)) = |[s2, r]| by Def1;

            then

             A26: ((M * (j,n)) `1 ) = s2 by EUCLID: 52;

            (c /. j) = (c . j) by A19, A24, PARTFUN1:def 6;

            then (c /. j) = (M * (j,n)) by A19, A21, A24, MATRIX_0:def 8;

            then

             A27: (x . j) = s2 by A24, A26, GOBOARD1:def 1;

             [i, n] in ( Indices M) by A1, A3, A4, A17, A19, A21, A23, ZFMISC_1: 87;

            then (M * (i,n)) = |[s1, r]| by Def1;

            then

             A28: ((M * (i,n)) `1 ) = s1 by EUCLID: 52;

            (c /. i) = (c . i) by A19, A23, PARTFUN1:def 6;

            then (c /. i) = (M * (i,n)) by A19, A21, A23, MATRIX_0:def 8;

            then (x . i) = s1 by A23, A28, GOBOARD1:def 1;

            hence (x . i) < (x . j) by A16, A2, A18, A20, A22, A23, A24, A25, A27, SEQM_3:def 1;

          end;

          hence thesis by SEQM_3:def 1;

        end;

      end;

    end

    definition

      let f be non empty FinSequence of ( TOP-REAL 2);

      :: GOBOARD2:def2

      func GoB (f) -> Matrix of ( TOP-REAL 2) equals ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f))));

      correctness ;

    end

    registration

      let f be non empty FinSequence of ( TOP-REAL 2);

      cluster ( GoB f) -> non empty-yielding X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column;

      coherence ;

    end

    reserve f for non empty FinSequence of ( TOP-REAL 2);

    theorem :: GOBOARD2:13

    

     Th13: ( len ( GoB f)) = ( card ( rng ( X_axis f))) & ( width ( GoB f)) = ( card ( rng ( Y_axis f)))

    proof

      set x = ( X_axis f), y = ( Y_axis f);

      ( len ( Incr x)) = ( card ( rng x)) & ( len ( Incr y)) = ( card ( rng y)) by SEQ_4:def 21;

      hence thesis by Def1;

    end;

    theorem :: GOBOARD2:14

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

    proof

      set x = ( X_axis f), y = ( Y_axis f);

      let n such that

       A1: n in ( dom f);

      

       A2: ( rng ( Incr y)) = ( rng y) by SEQ_4:def 21;

      reconsider p = (f /. n) as Point of ( TOP-REAL 2);

      

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

      ( dom y) = ( Seg ( len y)) & ( len y) = ( len f) by FINSEQ_1:def 3, GOBOARD1:def 2;

      then (y . n) = (p `2 ) & (y . n) in ( rng y) by A1, A3, FUNCT_1:def 3, GOBOARD1:def 2;

      then

      consider j be Nat such that

       A4: j in ( dom ( Incr y)) and

       A5: (( Incr y) . j) = (p `2 ) by A2, FINSEQ_2: 10;

      

       A6: ( rng ( Incr x)) = ( rng x) by SEQ_4:def 21;

      ( dom x) = ( Seg ( len x)) & ( len x) = ( len f) by FINSEQ_1:def 3, GOBOARD1:def 1;

      then (x . n) = (p `1 ) & (x . n) in ( rng x) by A1, A3, FUNCT_1:def 3, GOBOARD1:def 1;

      then

      consider i be Nat such that

       A7: i in ( dom ( Incr x)) and

       A8: (( Incr x) . i) = (p `1 ) by A6, FINSEQ_2: 10;

      ( width ( GoB f)) = ( card ( rng y)) & ( len ( Incr y)) = ( card ( rng y)) by Th13, SEQ_4:def 21;

      then

       A9: ( Seg ( width ( GoB f))) = ( dom ( Incr y)) by FINSEQ_1:def 3;

      reconsider i, j as Element of NAT by ORDINAL1:def 12;

      take i, j;

      ( len ( GoB f)) = ( card ( rng x)) & ( len ( Incr x)) = ( card ( rng x)) by Th13, SEQ_4:def 21;

      then ( Indices ( GoB f)) = [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] & ( dom ( GoB f)) = ( dom ( Incr x)) by FINSEQ_3: 29, MATRIX_0:def 4;

      hence [i, j] in ( Indices ( GoB f)) by A7, A4, A9, ZFMISC_1: 87;

      then (( GoB f) * (i,j)) = |[(p `1 ), (p `2 )]| by A8, A5, Def1;

      hence thesis by EUCLID: 53;

    end;

    theorem :: GOBOARD2:15

    n in ( dom f) & (for m st m in ( dom f) holds (( X_axis f) . n) <= (( X_axis f) . m)) implies (f /. n) in ( rng ( Line (( GoB f),1)))

    proof

      set x = ( X_axis f), y = ( Y_axis f), r = (x . n);

      assume that

       A1: n in ( dom f) and

       A2: for m st m in ( dom f) holds r <= (x . m);

      reconsider p = (f /. n) as Point of ( TOP-REAL 2);

      

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

      

       A4: ( dom x) = ( Seg ( len x)) & ( len x) = ( len f) by FINSEQ_1:def 3, GOBOARD1:def 1;

      then

       A5: (x . n) = (p `1 ) by A1, A3, GOBOARD1:def 1;

      

       A6: ( rng ( Incr x)) = ( rng x) by SEQ_4:def 21;

      (x . n) in ( rng x) by A1, A3, A4, FUNCT_1:def 3;

      then

      consider i be Nat such that

       A7: i in ( dom ( Incr x)) and

       A8: (( Incr x) . i) = (p `1 ) by A5, A6, FINSEQ_2: 10;

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

      

       A9: 1 <= i by A7, FINSEQ_3: 25;

      then

      reconsider i1 = (i - 1) as Element of NAT by INT_1: 5;

      

       A10: i <= ( len ( Incr x)) by A7, FINSEQ_3: 25;

       A11:

      now

        reconsider s = (( Incr x) . i1) as Real;

        assume i <> 1;

        then 1 < i by A9, XXREAL_0: 1;

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

        then

         A12: 1 <= i1 by XREAL_1: 19;

        i1 <= i by XREAL_1: 44;

        then i1 <= ( len ( Incr x)) by A10, XXREAL_0: 2;

        then

         A13: i1 in ( dom ( Incr x)) by A12, FINSEQ_3: 25;

        then (( Incr x) . i1) in ( rng ( Incr x)) by FUNCT_1:def 3;

        then

         A14: ex m be Nat st m in ( dom x) & (x . m) = s by A6, FINSEQ_2: 10;

        i1 < i by XREAL_1: 44;

        then s < r by A5, A7, A8, A13, SEQM_3:def 1;

        hence contradiction by A2, A3, A4, A14;

      end;

      

       A15: ( rng ( Incr y)) = ( rng y) by SEQ_4:def 21;

      ( dom y) = ( Seg ( len y)) & ( len y) = ( len f) by FINSEQ_1:def 3, GOBOARD1:def 2;

      then (y . n) = (p `2 ) & (y . n) in ( rng y) by A1, A3, FUNCT_1:def 3, GOBOARD1:def 2;

      then

      consider j be Nat such that

       A16: j in ( dom ( Incr y)) and

       A17: (( Incr y) . j) = (p `2 ) by A15, FINSEQ_2: 10;

      

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

      ( len ( Line (( GoB f),1))) = ( width ( GoB f)) by MATRIX_0:def 7;

      then

       A19: ( dom ( Line (( GoB f),1))) = ( Seg ( width ( GoB f))) by FINSEQ_1:def 3;

      ( width ( GoB f)) = ( card ( rng y)) & ( len ( Incr y)) = ( card ( rng y)) by Th13, SEQ_4:def 21;

      then

       A20: ( dom ( Incr y)) = ( Seg ( width ( GoB f))) by FINSEQ_1:def 3;

      ( len ( GoB f)) = ( card ( rng x)) & ( len ( Incr x)) = ( card ( rng x)) by Th13, SEQ_4:def 21;

      then ( Indices ( GoB f)) = [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] & ( dom ( Incr x)) = ( dom ( GoB f)) by FINSEQ_3: 29, MATRIX_0:def 4;

      then [1, j] in ( Indices ( GoB f)) by A7, A16, A20, A11, ZFMISC_1: 87;

      then (( GoB f) * (1,j)) = |[(p `1 ), (p `2 )]| by A8, A17, A11, Def1;

      then (( Line (( GoB f),1)) . j) = (f /. n) by A16, A20, A18, MATRIX_0:def 7;

      hence thesis by A16, A20, A19, FUNCT_1:def 3;

    end;

    theorem :: GOBOARD2:16

    n in ( dom f) & (for m st m in ( dom f) holds (( X_axis f) . m) <= (( X_axis f) . n)) implies (f /. n) in ( rng ( Line (( GoB f),( len ( GoB f)))))

    proof

      set x = ( X_axis f), y = ( Y_axis f), r = (x . n);

      assume that

       A1: n in ( dom f) and

       A2: for m st m in ( dom f) holds (x . m) <= r;

      reconsider p = (f /. n) as Point of ( TOP-REAL 2);

      

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

      

       A4: ( dom x) = ( Seg ( len x)) & ( len x) = ( len f) by FINSEQ_1:def 3, GOBOARD1:def 1;

      then

       A5: (x . n) = (p `1 ) by A1, A3, GOBOARD1:def 1;

      

       A6: ( rng ( Incr x)) = ( rng x) by SEQ_4:def 21;

      (x . n) in ( rng x) by A1, A3, A4, FUNCT_1:def 3;

      then

      consider i be Nat such that

       A7: i in ( dom ( Incr x)) and

       A8: (( Incr x) . i) = (p `1 ) by A5, A6, FINSEQ_2: 10;

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

      

       A9: i <= ( len ( Incr x)) by A7, FINSEQ_3: 25;

      

       A10: 1 <= i by A7, FINSEQ_3: 25;

       A11:

      now

        reconsider s = (( Incr x) . (i + 1)) as Real;

        assume i <> ( len ( Incr x));

        then i < ( len ( Incr x)) by A9, XXREAL_0: 1;

        then

         A12: (i + 1) <= ( len ( Incr x)) by NAT_1: 13;

        1 <= (i + 1) by A10, NAT_1: 13;

        then

         A13: (i + 1) in ( dom ( Incr x)) by A12, FINSEQ_3: 25;

        then (( Incr x) . (i + 1)) in ( rng ( Incr x)) by FUNCT_1:def 3;

        then

         A14: ex m be Nat st m in ( dom x) & (x . m) = s by A6, FINSEQ_2: 10;

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

        then r < s by A5, A7, A8, A13, SEQM_3:def 1;

        hence contradiction by A2, A3, A4, A14;

      end;

      

       A15: ( rng ( Incr y)) = ( rng y) by SEQ_4:def 21;

      ( dom y) = ( Seg ( len y)) & ( len y) = ( len f) by FINSEQ_1:def 3, GOBOARD1:def 2;

      then (y . n) = (p `2 ) & (y . n) in ( rng y) by A1, A3, FUNCT_1:def 3, GOBOARD1:def 2;

      then

      consider j be Nat such that

       A16: j in ( dom ( Incr y)) and

       A17: (( Incr y) . j) = (p `2 ) by A15, FINSEQ_2: 10;

      

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

      ( len ( Line (( GoB f),( len ( GoB f))))) = ( width ( GoB f)) by MATRIX_0:def 7;

      then

       A19: ( dom ( Line (( GoB f),( len ( GoB f))))) = ( Seg ( width ( GoB f))) by FINSEQ_1:def 3;

      ( width ( GoB f)) = ( card ( rng y)) & ( len ( Incr y)) = ( card ( rng y)) by Th13, SEQ_4:def 21;

      then

       A20: ( dom ( Incr y)) = ( Seg ( width ( GoB f))) by FINSEQ_1:def 3;

      

       A21: ( len ( GoB f)) = ( card ( rng x)) & ( len ( Incr x)) = ( card ( rng x)) by Th13, SEQ_4:def 21;

      then ( Indices ( GoB f)) = [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] & ( dom ( Incr x)) = ( dom ( GoB f)) by FINSEQ_3: 29, MATRIX_0:def 4;

      then [( len ( GoB f)), j] in ( Indices ( GoB f)) by A21, A7, A16, A20, A11, ZFMISC_1: 87;

      then (( GoB f) * (( len ( GoB f)),j)) = |[(p `1 ), (p `2 )]| by A21, A8, A17, A11, Def1;

      then (( Line (( GoB f),( len ( GoB f)))) . j) = (f /. n) by A16, A20, A18, MATRIX_0:def 7;

      hence thesis by A16, A20, A19, FUNCT_1:def 3;

    end;

    theorem :: GOBOARD2:17

    n in ( dom f) & (for m st m in ( dom f) holds (( Y_axis f) . n) <= (( Y_axis f) . m)) implies (f /. n) in ( rng ( Col (( GoB f),1)))

    proof

      set x = ( X_axis f), y = ( Y_axis f), r = (y . n);

      assume that

       A1: n in ( dom f) and

       A2: for m st m in ( dom f) holds r <= (y . m);

      reconsider p = (f /. n) as Point of ( TOP-REAL 2);

      

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

      

       A4: ( dom y) = ( Seg ( len y)) & ( len y) = ( len f) by FINSEQ_1:def 3, GOBOARD1:def 2;

      then

       A5: (y . n) = (p `2 ) by A1, A3, GOBOARD1:def 2;

      

       A6: ( rng ( Incr y)) = ( rng y) by SEQ_4:def 21;

      (y . n) in ( rng y) by A1, A3, A4, FUNCT_1:def 3;

      then

      consider j be Nat such that

       A7: j in ( dom ( Incr y)) and

       A8: (( Incr y) . j) = (p `2 ) by A5, A6, FINSEQ_2: 10;

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

      

       A9: 1 <= j by A7, FINSEQ_3: 25;

      then

      reconsider j1 = (j - 1) as Element of NAT by INT_1: 5;

      

       A10: j <= ( len ( Incr y)) by A7, FINSEQ_3: 25;

       A11:

      now

        reconsider s = (( Incr y) . j1) as Real;

        assume j <> 1;

        then 1 < j by A9, XXREAL_0: 1;

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

        then

         A12: 1 <= j1 by XREAL_1: 19;

        j1 <= j by XREAL_1: 44;

        then j1 <= ( len ( Incr y)) by A10, XXREAL_0: 2;

        then

         A13: j1 in ( dom ( Incr y)) by A12, FINSEQ_3: 25;

        then (( Incr y) . j1) in ( rng ( Incr y)) by FUNCT_1:def 3;

        then

         A14: ex m be Nat st m in ( dom y) & (y . m) = s by A6, FINSEQ_2: 10;

        j1 < j by XREAL_1: 44;

        then s < r by A5, A7, A8, A13, SEQM_3:def 1;

        hence contradiction by A2, A3, A4, A14;

      end;

      

       A15: ( rng ( Incr x)) = ( rng x) by SEQ_4:def 21;

      ( dom x) = ( Seg ( len x)) & ( len x) = ( len f) by FINSEQ_1:def 3, GOBOARD1:def 1;

      then (x . n) = (p `1 ) & (x . n) in ( rng x) by A1, A3, FUNCT_1:def 3, GOBOARD1:def 1;

      then

      consider i be Nat such that

       A16: i in ( dom ( Incr x)) and

       A17: (( Incr x) . i) = (p `1 ) by A15, FINSEQ_2: 10;

      

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

      ( len ( Col (( GoB f),1))) = ( len ( GoB f)) by MATRIX_0:def 8;

      then

       A19: ( dom ( Col (( GoB f),1))) = ( dom ( GoB f)) by FINSEQ_3: 29;

      ( len ( GoB f)) = ( card ( rng x)) & ( len ( Incr x)) = ( card ( rng x)) by Th13, SEQ_4:def 21;

      then

       A20: ( dom ( Incr x)) = ( dom ( GoB f)) by FINSEQ_3: 29;

      ( width ( GoB f)) = ( card ( rng y)) & ( len ( Incr y)) = ( card ( rng y)) by Th13, SEQ_4:def 21;

      then ( Indices ( GoB f)) = [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] & ( dom ( Incr y)) = ( Seg ( width ( GoB f))) by FINSEQ_1:def 3, MATRIX_0:def 4;

      then [i, 1] in ( Indices ( GoB f)) by A16, A7, A20, A11, ZFMISC_1: 87;

      then (( GoB f) * (i,1)) = |[(p `1 ), (p `2 )]| by A17, A8, A11, Def1;

      then (( Col (( GoB f),1)) . i) = (f /. n) by A16, A20, A18, MATRIX_0:def 8;

      hence thesis by A16, A20, A19, FUNCT_1:def 3;

    end;

    theorem :: GOBOARD2:18

    n in ( dom f) & (for m st m in ( dom f) holds (( Y_axis f) . m) <= (( Y_axis f) . n)) implies (f /. n) in ( rng ( Col (( GoB f),( width ( GoB f)))))

    proof

      set x = ( X_axis f), y = ( Y_axis f), r = (y . n);

      assume that

       A1: n in ( dom f) and

       A2: for m st m in ( dom f) holds (y . m) <= r;

      reconsider p = (f /. n) as Point of ( TOP-REAL 2);

      

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

      

       A4: ( dom y) = ( Seg ( len y)) & ( len y) = ( len f) by FINSEQ_1:def 3, GOBOARD1:def 2;

      then

       A5: (y . n) = (p `2 ) by A1, A3, GOBOARD1:def 2;

      

       A6: ( rng ( Incr y)) = ( rng y) by SEQ_4:def 21;

      (y . n) in ( rng y) by A1, A3, A4, FUNCT_1:def 3;

      then

      consider j be Nat such that

       A7: j in ( dom ( Incr y)) and

       A8: (( Incr y) . j) = (p `2 ) by A5, A6, FINSEQ_2: 10;

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

      

       A9: j <= ( len ( Incr y)) by A7, FINSEQ_3: 25;

      

       A10: 1 <= j by A7, FINSEQ_3: 25;

       A11:

      now

        reconsider s = (( Incr y) . (j + 1)) as Real;

        assume j <> ( len ( Incr y));

        then j < ( len ( Incr y)) by A9, XXREAL_0: 1;

        then

         A12: (j + 1) <= ( len ( Incr y)) by NAT_1: 13;

        1 <= (j + 1) by A10, NAT_1: 13;

        then

         A13: (j + 1) in ( dom ( Incr y)) by A12, FINSEQ_3: 25;

        then (( Incr y) . (j + 1)) in ( rng ( Incr y)) by FUNCT_1:def 3;

        then

         A14: ex m be Nat st m in ( dom y) & (y . m) = s by A6, FINSEQ_2: 10;

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

        then r < s by A5, A7, A8, A13, SEQM_3:def 1;

        hence contradiction by A2, A3, A4, A14;

      end;

      

       A15: ( rng ( Incr x)) = ( rng x) by SEQ_4:def 21;

      ( dom x) = ( Seg ( len x)) & ( len x) = ( len f) by FINSEQ_1:def 3, GOBOARD1:def 1;

      then (x . n) = (p `1 ) & (x . n) in ( rng x) by A1, A3, FUNCT_1:def 3, GOBOARD1:def 1;

      then

      consider i be Nat such that

       A16: i in ( dom ( Incr x)) and

       A17: (( Incr x) . i) = (p `1 ) by A15, FINSEQ_2: 10;

      

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

      ( len ( Col (( GoB f),( width ( GoB f))))) = ( len ( GoB f)) by MATRIX_0:def 8;

      then

       A19: ( dom ( Col (( GoB f),( width ( GoB f))))) = ( dom ( GoB f)) by FINSEQ_3: 29;

      ( len ( GoB f)) = ( card ( rng x)) & ( len ( Incr x)) = ( card ( rng x)) by Th13, SEQ_4:def 21;

      then

       A20: ( dom ( Incr x)) = ( dom ( GoB f)) by FINSEQ_3: 29;

      

       A21: ( width ( GoB f)) = ( card ( rng y)) & ( len ( Incr y)) = ( card ( rng y)) by Th13, SEQ_4:def 21;

      then ( Indices ( GoB f)) = [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] & ( dom ( Incr y)) = ( Seg ( width ( GoB f))) by FINSEQ_1:def 3, MATRIX_0:def 4;

      then [i, ( width ( GoB f))] in ( Indices ( GoB f)) by A21, A16, A7, A20, A11, ZFMISC_1: 87;

      then (( GoB f) * (i,( width ( GoB f)))) = |[(p `1 ), (p `2 )]| by A21, A17, A8, A11, Def1;

      then (( Col (( GoB f),( width ( GoB f)))) . i) = (f /. n) by A16, A20, A18, MATRIX_0:def 8;

      hence thesis by A16, A20, A19, FUNCT_1:def 3;

    end;