jgraph_1.miz



    begin

    reserve x,y for set;

    reserve G for Graph;

    reserve vs,vs9 for FinSequence of the carrier of G;

    reserve IT for oriented Chain of G;

    reserve N for Nat;

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

    reserve r,r1,r2 for Real;

    theorem :: JGRAPH_1:1

    

     Th1: for vs st IT is Simple & vs is_oriented_vertex_seq_of IT holds for n, m st 1 <= n & n < m & m <= ( len vs) & (vs . n) = (vs . m) holds n = 1 & m = ( len vs)

    proof

      let vs;

      assume that

       A1: IT is Simple and

       A2: vs is_oriented_vertex_seq_of IT;

      

       A3: ( len vs) = (( len IT) + 1) by A2, GRAPH_4:def 5;

      consider vs9 such that

       A4: vs9 is_oriented_vertex_seq_of IT and

       A5: for n,m be Nat st 1 <= n & n < m & m <= ( len vs9) & (vs9 . n) = (vs9 . m) holds n = 1 & m = ( len vs9) by A1, GRAPH_4:def 7;

      

       A6: for n,m be Nat st 1 <= n & n < m & m <= ( len vs9) & (vs9 . n) = (vs9 . m) holds n = 1 & m = ( len vs9) by A5;

      per cases ;

        suppose IT <> {} ;

        then vs = vs9 by A2, A4, GRAPH_4: 10;

        hence thesis by A6;

      end;

        suppose IT = {} ;

        then ( len IT) = 0 ;

        hence thesis by A3, XXREAL_0: 2;

      end;

    end;

    definition

      let X be set;

      :: JGRAPH_1:def1

      func PGraph (X) -> MultiGraphStruct equals MultiGraphStruct (# X, [:X, X:], ( pr1 (X,X)), ( pr2 (X,X)) #);

      coherence ;

    end

    theorem :: JGRAPH_1:2

    for X be set holds the carrier of ( PGraph X) = X;

    definition

      let f be FinSequence;

      :: JGRAPH_1:def2

      func PairF (f) -> FinSequence means

      : Def2: ( len it ) = (( len f) -' 1) & for i be Nat st 1 <= i & i < ( len f) holds (it . i) = [(f . i), (f . (i + 1))];

      existence

      proof

        deffunc F( Nat) = [(f . $1), (f . ($1 + 1))];

        ex p be FinSequence st ( len p) = (( len f) -' 1) & for k be Nat st k in ( dom p) holds (p . k) = F(k) from FINSEQ_1:sch 2;

        then

        consider p be FinSequence such that

         A1: ( len p) = (( len f) -' 1) and

         A2: for k be Nat st k in ( dom p) holds (p . k) = [(f . k), (f . (k + 1))];

        for i be Nat st 1 <= i & i < ( len f) holds (p . i) = [(f . i), (f . (i + 1))]

        proof

          let i be Nat;

          assume that

           A3: 1 <= i and

           A4: i < ( len f);

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

          then

           A5: ((i + 1) - 1) <= (( len f) - 1) by XREAL_1: 9;

          (( len f) - 1) = (( len f) -' 1) by A3, A4, XREAL_1: 233, XXREAL_0: 2;

          then i in ( dom p) by A1, A3, A5, FINSEQ_3: 25;

          hence thesis by A2;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let g1,g2 be FinSequence;

        assume that

         A6: ( len g1) = (( len f) -' 1) and

         A7: for i be Nat st 1 <= i & i < ( len f) holds (g1 . i) = [(f . i), (f . (i + 1))] and

         A8: ( len g2) = (( len f) -' 1) and

         A9: for i be Nat st 1 <= i & i < ( len f) holds (g2 . i) = [(f . i), (f . (i + 1))];

        per cases ;

          suppose

           A10: ( len f) >= 1;

          for j be Nat st 1 <= j & j <= ( len g1) holds (g1 . j) = (g2 . j)

          proof

            let j be Nat;

            assume that

             A11: 1 <= j and

             A12: j <= ( len g1);

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

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

            then ( len g1) < ( len f) by A6, A10, XREAL_1: 233;

            then

             A13: j in NAT & j < ( len f) by A12, ORDINAL1:def 12, XXREAL_0: 2;

            then (g1 . j) = [(f . j), (f . (j + 1))] by A7, A11;

            hence thesis by A9, A11, A13;

          end;

          hence thesis by A6, A8, FINSEQ_1: 14;

        end;

          suppose ( len f) < 1;

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

          then ((( len f) + 1) - 1) <= (1 - 1) by XREAL_1: 9;

          then

           A14: ( len f) = 0 ;

          ( 0 qua Nat - 1) < 0 ;

          then g1 = {} by A6, A14, XREAL_0:def 2;

          hence thesis by A6, A8;

        end;

      end;

    end

    reserve X for non empty set;

    registration

      let X be non empty set;

      cluster ( PGraph X) -> non empty;

      coherence ;

    end

    theorem :: JGRAPH_1:3

    for f be FinSequence of X holds f is FinSequence of the carrier of ( PGraph X);

    theorem :: JGRAPH_1:4

    

     Th4: for f be FinSequence of X holds ( PairF f) is FinSequence of the carrier' of ( PGraph X)

    proof

      let f be FinSequence of X;

      ( rng ( PairF f)) c= [:X, X:]

      proof

        let y be object;

        

         A1: (( len f) -' 1) < ((( len f) -' 1) + 1) by NAT_1: 13;

        assume y in ( rng ( PairF f));

        then

        consider x be object such that

         A2: x in ( dom ( PairF f)) and

         A3: y = (( PairF f) . x) by FUNCT_1:def 3;

        reconsider n = x as Element of NAT by A2;

        

         A4: x in ( Seg ( len ( PairF f))) by A2, FINSEQ_1:def 3;

        then

         A5: 1 <= n by FINSEQ_1: 1;

        

         A6: ( len ( PairF f)) = (( len f) -' 1) by Def2;

        

         A7: n <= ( len ( PairF f)) by A4, FINSEQ_1: 1;

        then 1 <= (( len f) -' 1) by A5, A6, XXREAL_0: 2;

        then (( len f) -' 1) = (( len f) - 1) by NAT_D: 39;

        then

         A8: n < ( len f) by A7, A6, A1, XXREAL_0: 2;

        then

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

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

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

        then

         A10: (f . (n + 1)) in ( rng f) by FUNCT_1:def 3;

        n in ( dom f) by A5, A8, FINSEQ_3: 25;

        then

         A11: (f . n) in ( rng f) by FUNCT_1:def 3;

        (( PairF f) . n) = [(f . n), (f . (n + 1))] by A5, A8, Def2;

        hence thesis by A3, A11, A10, ZFMISC_1:def 2;

      end;

      hence thesis by FINSEQ_1:def 4;

    end;

    definition

      let X be non empty set, f be FinSequence of X;

      :: original: PairF

      redefine

      func PairF (f) -> FinSequence of the carrier' of ( PGraph X) ;

      coherence by Th4;

    end

    theorem :: JGRAPH_1:5

    

     Th5: for n be Nat, f be FinSequence of X st 1 <= n & n <= ( len ( PairF f)) holds (( PairF f) . n) in the carrier' of ( PGraph X)

    proof

      let n be Nat, f be FinSequence of X;

      assume that

       A1: 1 <= n and

       A2: n <= ( len ( PairF f));

      

       A3: (( len f) -' 1) < ((( len f) -' 1) + 1) by NAT_1: 13;

      

       A4: ( len ( PairF f)) = (( len f) -' 1) by Def2;

      then 1 <= (( len f) -' 1) by A1, A2, XXREAL_0: 2;

      then (( len f) -' 1) = (( len f) - 1) by NAT_D: 39;

      then

       A5: n < ( len f) by A2, A4, A3, XXREAL_0: 2;

      then

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

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

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

      then

       A7: (f . (n + 1)) in ( rng f) by FUNCT_1:def 3;

      n in ( dom f) by A1, A5, FINSEQ_3: 25;

      then

       A8: (f . n) in ( rng f) by FUNCT_1:def 3;

      (( PairF f) . n) = [(f . n), (f . (n + 1))] by A1, A5, Def2;

      hence thesis by A8, A7, ZFMISC_1:def 2;

    end;

    theorem :: JGRAPH_1:6

    

     Th6: for f be FinSequence of X holds ( PairF f) is oriented Chain of ( PGraph X)

    proof

      let f be FinSequence of X;

       A1:

      now

        per cases ;

          case ( len f) >= 1;

          then ((( len f) - 1) + 1) = ((( len f) -' 1) + 1) by XREAL_1: 233;

          then

           A2: ( len f) = (( len ( PairF f)) + 1) by Def2;

          

           A3: for n be Nat st 1 <= n & n <= ( len f) holds (f . n) in the carrier of ( PGraph X)

          proof

            let n be Nat;

            assume 1 <= n & n <= ( len f);

            then n in ( dom f) by FINSEQ_3: 25;

            then (f . n) in ( rng f) by FUNCT_1:def 3;

            hence thesis;

          end;

          

           A4: for n be Nat st 1 <= n & n <= ( len ( PairF f)) holds ex x9,y9 be Element of ( PGraph X) st x9 = (f . n) & y9 = (f . (n + 1)) & (( PairF f) . n) joins (x9,y9)

          proof

            

             A5: (( len f) -' 1) < ((( len f) -' 1) + 1) by NAT_1: 13;

            let n be Nat;

            assume that

             A6: 1 <= n and

             A7: n <= ( len ( PairF f));

            

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

            

             A9: ( len ( PairF f)) = (( len f) -' 1) by Def2;

            then 1 <= (( len f) -' 1) by A6, A7, XXREAL_0: 2;

            then (( len f) -' 1) = (( len f) - 1) by NAT_D: 39;

            then

             A10: n < ( len f) by A7, A9, A5, XXREAL_0: 2;

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

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

            then

             A11: (f . (n + 1)) in ( rng f) by FUNCT_1:def 3;

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

            then

             A12: (f . n) in ( rng f) by FUNCT_1:def 3;

            then

            reconsider a = (f . n), b = (f . (n + 1)) as Element of ( PGraph X) by A11;

            (( pr2 (X,X)) . ((f . n),(f . (n + 1)))) = (f . (n + 1)) by A12, A11, FUNCT_3:def 5;

            then

             A13: (the Target of ( PGraph X) . (( PairF f) . n)) = b by A6, A10, Def2;

            (( pr1 (X,X)) . ((f . n),(f . (n + 1)))) = (f . n) by A12, A11, FUNCT_3:def 4;

            then (the Source of ( PGraph X) . (( PairF f) . n)) = a by A6, A10, Def2;

            then (( PairF f) . n) joins (a,b) by A13, GRAPH_1:def 12;

            hence thesis;

          end;

          for n be Nat st 1 <= n & n <= ( len ( PairF f)) holds (( PairF f) . n) in the carrier' of ( PGraph X) by Th5;

          hence ( PairF f) is Chain of ( PGraph X) by A2, A3, A4, GRAPH_1:def 14;

        end;

          case ( len f) < 1;

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

          then ((( len f) + 1) - 1) <= (1 - 1) by XREAL_1: 9;

          then

           A14: ( len f) = 0 ;

          ( 0 qua Nat - 1) < 0 ;

          then (( len f) -' 1) = 0 by A14, XREAL_0:def 2;

          then ( len ( PairF f)) = 0 by Def2;

          then ( PairF f) = {} ;

          hence thesis by GRAPH_1: 14;

        end;

      end;

      for n be Nat st 1 <= n & n < ( len ( PairF f)) holds (the Source of ( PGraph X) . (( PairF f) . (n + 1))) = (the Target of ( PGraph X) . (( PairF f) . n))

      proof

        

         A15: (( len f) -' 1) < ((( len f) -' 1) + 1) by NAT_1: 13;

        let n be Nat;

        assume that

         A16: 1 <= n and

         A17: n < ( len ( PairF f));

        

         A18: ( len ( PairF f)) = (( len f) -' 1) by Def2;

        then 1 <= (( len f) -' 1) by A16, A17, XXREAL_0: 2;

        then

         A19: (( len f) -' 1) = (( len f) - 1) by NAT_D: 39;

        then

         A20: n < ( len f) by A17, A18, A15, XXREAL_0: 2;

        then n in ( dom f) by A16, FINSEQ_3: 25;

        then

         A21: (f . n) in ( rng f) by FUNCT_1:def 3;

        (n + 1) <= ( len ( PairF f)) by A17, NAT_1: 13;

        then

         A22: (n + 1) < ( len f) by A18, A19, A15, XXREAL_0: 2;

        then

         A23: ((n + 1) + 1) <= ( len f) by NAT_1: 13;

        

         A24: 1 < (n + 1) by A16, NAT_1: 13;

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

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

        then

         A25: (f . ((n + 1) + 1)) in ( rng f) by FUNCT_1:def 3;

        (n + 1) <= ( len f) by A20, NAT_1: 13;

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

        then

         A26: (f . (n + 1)) in ( rng f) by FUNCT_1:def 3;

        then

        reconsider b = (f . (n + 1)) as Element of ( PGraph X);

        (( pr2 (X,X)) . ((f . n),(f . (n + 1)))) = (f . (n + 1)) by A21, A26, FUNCT_3:def 5;

        then

         A27: (the Target of ( PGraph X) . (( PairF f) . n)) = b by A16, A20, Def2;

        (n + 1) in ( dom f) by A22, A24, FINSEQ_3: 25;

        then (f . (n + 1)) in ( rng f) by FUNCT_1:def 3;

        then (( pr1 (X,X)) . ((f . (n + 1)),(f . ((n + 1) + 1)))) = (f . (n + 1)) by A25, FUNCT_3:def 4;

        hence thesis by A22, A24, A27, Def2;

      end;

      hence thesis by A1, GRAPH_1:def 15;

    end;

    definition

      let X be non empty set, f be FinSequence of X;

      :: original: PairF

      redefine

      func PairF (f) -> oriented Chain of ( PGraph X) ;

      coherence by Th6;

    end

    theorem :: JGRAPH_1:7

    

     Th7: for f be FinSequence of X, f1 be FinSequence of the carrier of ( PGraph X) st ( len f) >= 1 & f = f1 holds f1 is_oriented_vertex_seq_of ( PairF f)

    proof

      let f be FinSequence of X, f1 be FinSequence of the carrier of ( PGraph X);

      assume that

       A1: ( len f) >= 1 and

       A2: f = f1;

      

       A3: for n st 1 <= n & n <= ( len ( PairF f)) holds (( PairF f) . n) orientedly_joins ((f1 /. n),(f1 /. (n + 1)))

      proof

        

         A4: (( len f) -' 1) < ((( len f) -' 1) + 1) by NAT_1: 13;

        let n;

        assume that

         A5: 1 <= n and

         A6: n <= ( len ( PairF f));

        

         A7: 1 < (n + 1) by A5, NAT_1: 13;

        

         A8: ( len ( PairF f)) = (( len f) -' 1) by Def2;

        then 1 <= (( len f) -' 1) by A5, A6, XXREAL_0: 2;

        then (( len f) -' 1) = (( len f) - 1) by NAT_D: 39;

        then

         A9: n < ( len f) by A6, A8, A4, XXREAL_0: 2;

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

        then

         A10: (n + 1) in ( dom f) by A7, FINSEQ_3: 25;

        then

         A11: (f . (n + 1)) in ( rng f) by FUNCT_1:def 3;

        

         A12: n in ( dom f) by A5, A9, FINSEQ_3: 25;

        then

         A13: (f . n) in ( rng f) by FUNCT_1:def 3;

        then

         A14: (( pr1 (X,X)) . ((f . n),(f . (n + 1)))) = (f . n) by A11, FUNCT_3:def 4;

        

         A15: (( pr2 (X,X)) . ((f . n),(f . (n + 1)))) = (f . (n + 1)) by A13, A11, FUNCT_3:def 5;

        (f1 /. (n + 1)) = (f1 . (n + 1)) by A2, A10, PARTFUN1:def 6;

        then

         A16: (the Target of ( PGraph X) . (( PairF f) . n)) = (f1 /. (n + 1)) by A2, A5, A9, A15, Def2;

        (f1 /. n) = (f1 . n) by A2, A12, PARTFUN1:def 6;

        then (the Source of ( PGraph X) . (( PairF f) . n)) = (f1 /. n) by A2, A5, A9, A14, Def2;

        hence thesis by A16, GRAPH_4:def 1;

      end;

      

       A17: for n be Nat st 1 <= n & n <= ( len ( PairF f)) holds (( PairF f) . n) orientedly_joins ((f1 /. n),(f1 /. (n + 1))) by A3;

      (( len f) -' 1) = (( len f) - 1) by A1, XREAL_1: 233;

      then ((( len f) - 1) + 1) = (( len ( PairF f)) + 1) by Def2;

      hence thesis by A2, A17, GRAPH_4:def 5;

    end;

    begin

    definition

      let X be non empty set, f,g be FinSequence of X;

      :: JGRAPH_1:def3

      pred g is_Shortcut_of f means (f . 1) = (g . 1) & (f . ( len f)) = (g . ( len g)) & ex fc be Subset of ( PairF f), fvs be Subset of f, sc be oriented simple Chain of ( PGraph X), g1 be FinSequence of the carrier of ( PGraph X) st ( Seq fc) = sc & ( Seq fvs) = g & g1 = g & g1 is_oriented_vertex_seq_of sc;

    end

    theorem :: JGRAPH_1:8

    

     Th8: for f,g be FinSequence of X st g is_Shortcut_of f holds 1 <= ( len g) & ( len g) <= ( len f)

    proof

      let f,g be FinSequence of X;

      reconsider df = ( dom f) as finite set;

      

       A1: ( card df) = ( card ( Seg ( len f))) by FINSEQ_1:def 3

      .= ( len f) by FINSEQ_1: 57;

      assume g is_Shortcut_of f;

      then

      consider fc be Subset of ( PairF f), fvs be Subset of f, sc be oriented simple Chain of ( PGraph X), g1 be FinSequence of the carrier of ( PGraph X) such that ( Seq fc) = sc and

       A2: ( Seq fvs) = g and

       A3: g1 = g and

       A4: g1 is_oriented_vertex_seq_of sc;

      

       A5: ( len g1) = (( len sc) + 1) by A4, GRAPH_4:def 5;

      reconsider dfvs = ( dom fvs) as finite set;

      

       A6: ( rng ( Sgm ( dom fvs))) c= ( dom fvs) by FINSEQ_1: 50;

      

       A7: ( dom fvs) c= ( dom f) by RELAT_1: 11;

      then

       A8: ( dom fvs) c= ( Seg ( len f)) by FINSEQ_1:def 3;

      g = (fvs * ( Sgm ( dom fvs))) by A2, FINSEQ_1:def 14;

      then ( dom g) = ( dom ( Sgm ( dom fvs))) by A6, RELAT_1: 27;

      

      then ( len g) = ( len ( Sgm ( dom fvs))) by FINSEQ_3: 29

      .= ( card dfvs) by A8, FINSEQ_3: 39;

      hence thesis by A3, A5, A7, A1, NAT_1: 12, NAT_1: 43;

    end;

    theorem :: JGRAPH_1:9

    

     Th9: for f be FinSequence of X st ( len f) >= 1 holds ex g be FinSequence of X st g is_Shortcut_of f

    proof

      let f be FinSequence of X;

      reconsider f1 = f as FinSequence of the carrier of ( PGraph X);

      assume ( len f) >= 1;

      then

      consider fc be Subset of ( PairF f), fvs be Subset of f1, sc be oriented simple Chain of ( PGraph X), vs1 be FinSequence of the carrier of ( PGraph X) such that

       A1: ( Seq fc) = sc & ( Seq fvs) = vs1 & vs1 is_oriented_vertex_seq_of sc & (f1 . 1) = (vs1 . 1) & (f1 . ( len f1)) = (vs1 . ( len vs1)) by Th7, GRAPH_4: 21;

      reconsider g1 = vs1 as FinSequence of X;

      g1 is_Shortcut_of f by A1;

      hence thesis;

    end;

    theorem :: JGRAPH_1:10

    

     Th10: for f,g be FinSequence of X st g is_Shortcut_of f holds ( rng ( PairF g)) c= ( rng ( PairF f))

    proof

      let f,g be FinSequence of X;

      

       A1: ( len ( PairF g)) = (( len g) -' 1) by Def2;

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

      then

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

      assume g is_Shortcut_of f;

      then

      consider fc be Subset of ( PairF f), fvs be Subset of f, sc be oriented simple Chain of ( PGraph X), g1 be FinSequence of the carrier of ( PGraph X) such that

       A3: ( Seq fc) = sc and ( Seq fvs) = g and

       A4: g1 = g and

       A5: g1 is_oriented_vertex_seq_of sc;

      

       A6: ( rng ( Sgm ( dom fc))) = ( dom fc) by FINSEQ_1: 50;

      (fc * ( Sgm ( dom fc))) = sc by A3, FINSEQ_1:def 14;

      then ( rng fc) = ( rng sc) by A6, RELAT_1: 28;

      then

       A7: ( rng sc) c= ( rng ( PairF f)) by RELAT_1: 11;

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

      then

       A8: (( len f) - 1) < ( len f) by XREAL_1: 19;

      let y be object;

      assume y in ( rng ( PairF g));

      then

      consider x be object such that

       A9: x in ( dom ( PairF g)) and

       A10: y = (( PairF g) . x) by FUNCT_1:def 3;

      reconsider n = x as Element of NAT by A9;

      

       A11: x in ( Seg ( len ( PairF g))) by A9, FINSEQ_1:def 3;

      then

       A12: 1 <= n by FINSEQ_1: 1;

      then

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

      

       A14: n <= ( len ( PairF g)) by A11, FINSEQ_1: 1;

      then 1 <= ( len ( PairF g)) by A12, XXREAL_0: 2;

      then (( len g) -' 1) = (( len g) - 1) by A1, NAT_D: 39;

      then

       A15: n < ( len g) by A14, A1, A2, XXREAL_0: 2;

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

      then (n + 1) <= (( len sc) + 1) by A4, A5, GRAPH_4:def 5;

      then

       A16: n <= ( len sc) by XREAL_1: 6;

      then

       A17: (sc . n) orientedly_joins ((g1 /. n),(g1 /. (n + 1))) by A5, A12, GRAPH_4:def 5;

      n in ( dom sc) by A12, A16, FINSEQ_3: 25;

      then (sc . n) in ( rng sc) by FUNCT_1:def 3;

      then

      consider z be object such that

       A18: z in ( dom ( PairF f)) and

       A19: (( PairF f) . z) = (sc . n) by A7, FUNCT_1:def 3;

      reconsider m = z as Element of NAT by A18;

      

       A20: z in ( Seg ( len ( PairF f))) by A18, FINSEQ_1:def 3;

      then

       A21: 1 <= m by FINSEQ_1: 1;

      m <= ( len ( PairF f)) by A20, FINSEQ_1: 1;

      then

       A22: m <= (( len f) -' 1) by Def2;

      then 1 <= (( len f) -' 1) by A21, XXREAL_0: 2;

      then (( len f) -' 1) = (( len f) - 1) by NAT_D: 39;

      then

       A23: m < ( len f) by A22, A8, XXREAL_0: 2;

      then

       A24: (m + 1) <= ( len f) by NAT_1: 13;

      

       A25: 1 <= m by A20, FINSEQ_1: 1;

      then

       A26: [(f . m), (f . (m + 1))] = (sc . n) by A19, A23, Def2;

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

      then (m + 1) in ( dom f) by A24, FINSEQ_3: 25;

      then

       A27: (f . (m + 1)) in ( rng f) by FUNCT_1:def 3;

      m in ( dom f) by A25, A23, FINSEQ_3: 25;

      then

       A28: (f . m) in ( rng f) by FUNCT_1:def 3;

      then (the Source of ( PGraph X) . ((f . m),(f . (m + 1)))) = (f . m) by A27, FUNCT_3:def 4;

      then (g1 /. n) = (f . m) by A17, A26, GRAPH_4:def 1;

      then

       A29: (g . n) = (f . m) by A4, A12, A15, FINSEQ_4: 15;

      

       A30: (( PairF g) . x) = [(g . n), (g . (n + 1))] by A12, A15, Def2;

      (the Target of ( PGraph X) . ((f . m),(f . (m + 1)))) = (f . (m + 1)) by A28, A27, FUNCT_3:def 5;

      then

       A31: (g1 /. (n + 1)) = (f . (m + 1)) by A17, A26, GRAPH_4:def 1;

      (n + 1) <= ( len g1) by A4, A15, NAT_1: 13;

      then (g . (n + 1)) = (f . (m + 1)) by A4, A31, A13, FINSEQ_4: 15;

      hence thesis by A10, A30, A18, A19, A26, A29, FUNCT_1:def 3;

    end;

    theorem :: JGRAPH_1:11

    

     Th11: for f,g be FinSequence of X st (f . 1) <> (f . ( len f)) & g is_Shortcut_of f holds g is one-to-one

    proof

      let f,g be FinSequence of X;

      assume that

       A1: (f . 1) <> (f . ( len f)) and

       A2: g is_Shortcut_of f;

      

       A3: (f . 1) = (g . 1) & (f . ( len f)) = (g . ( len g)) by A2;

      consider fc be Subset of ( PairF f), fvs be Subset of f, sc be oriented simple Chain of ( PGraph X), g1 be FinSequence of the carrier of ( PGraph X) such that ( Seq fc) = sc and ( Seq fvs) = g and

       A4: g1 = g and

       A5: g1 is_oriented_vertex_seq_of sc by A2;

      sc is Simple by GRAPH_4: 18;

      then

      consider vs be FinSequence of the carrier of ( PGraph X) such that

       A6: vs is_oriented_vertex_seq_of sc and

       A7: for n,m be Nat st 1 <= n & n < m & m <= ( len vs) & (vs . n) = (vs . m) holds n = 1 & m = ( len vs) by GRAPH_4:def 7;

      

       A8: ( len g1) = (( len sc) + 1) by A5, GRAPH_4:def 5;

      then 1 <= ( len g1) by NAT_1: 11;

      then 1 < ( len g1) by A1, A3, A4, XXREAL_0: 1;

      then sc <> {} by A8;

      then

       A9: g1 = vs by A5, A6, GRAPH_4: 10;

      let x,y be object;

      assume that

       A10: x in ( dom g) and

       A11: y in ( dom g) and

       A12: (g . x) = (g . y);

      assume

       A13: x <> y;

      reconsider i1 = x as Element of NAT by A10;

      

       A14: x in ( Seg ( len g)) by A10, FINSEQ_1:def 3;

      then

       A15: 1 <= i1 by FINSEQ_1: 1;

      

       A16: i1 <= ( len g) by A14, FINSEQ_1: 1;

      reconsider i2 = y as Element of NAT by A11;

      

       A17: y in ( Seg ( len g)) by A11, FINSEQ_1:def 3;

      then

       A18: 1 <= i2 by FINSEQ_1: 1;

      

       A19: i2 <= ( len g) by A17, FINSEQ_1: 1;

      per cases ;

        suppose i1 <= i2;

        then

         A20: i1 < i2 by A13, XXREAL_0: 1;

        then i1 = 1 by A4, A7, A9, A12, A15, A19;

        hence contradiction by A1, A3, A4, A7, A9, A12, A19, A20;

      end;

        suppose

         A21: i1 > i2;

        then i2 = 1 by A4, A7, A9, A12, A16, A18;

        hence contradiction by A1, A3, A4, A7, A9, A12, A16, A21;

      end;

    end;

    definition

      let n;

      let IT be FinSequence of ( TOP-REAL n);

      :: JGRAPH_1:def4

      attr IT is nodic means for i, j st ( LSeg (IT,i)) meets ( LSeg (IT,j)) holds (( LSeg (IT,i)) /\ ( LSeg (IT,j))) = {(IT . i)} & ((IT . i) = (IT . j) or (IT . i) = (IT . (j + 1))) or (( LSeg (IT,i)) /\ ( LSeg (IT,j))) = {(IT . (i + 1))} & ((IT . (i + 1)) = (IT . j) or (IT . (i + 1)) = (IT . (j + 1))) or ( LSeg (IT,i)) = ( LSeg (IT,j));

    end

    theorem :: JGRAPH_1:12

    for f be FinSequence of ( TOP-REAL 2) st f is s.n.c. holds f is s.c.c.

    proof

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

      assume f is s.n.c.;

      then for i, j st (i + 1) < j & (i > 1 & j < ( len f) or (j + 1) < ( len f)) holds ( LSeg (f,i)) misses ( LSeg (f,j)) by TOPREAL1:def 7;

      hence thesis by GOBOARD5:def 4;

    end;

    theorem :: JGRAPH_1:13

    

     Th13: for f be FinSequence of ( TOP-REAL 2) st f is s.c.c. & ( LSeg (f,1)) misses ( LSeg (f,(( len f) -' 1))) holds f is s.n.c.

    proof

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

      assume that

       A1: f is s.c.c. and

       A2: ( LSeg (f,1)) misses ( LSeg (f,(( len f) -' 1)));

      for i,j be Nat st (i + 1) < j holds ( LSeg (f,i)) misses ( LSeg (f,j))

      proof

        let i,j be Nat;

        assume

         A3: (i + 1) < j;

        per cases ;

          suppose ( len f) <> 0 ;

          then

           A4: ( len f) >= ( 0 qua Nat + 1) by NAT_1: 13;

          now

            per cases ;

              case

               A5: 1 <= i & (j + 1) <= ( len f);

              then

               A6: j < ( len f) by NAT_1: 13;

              now

                per cases ;

                  case

                   A7: i = 1 & (j + 1) = ( len f);

                  then j = (( len f) - 1);

                  then ( LSeg (f,i)) misses ( LSeg (f,j)) by A2, A4, A7, XREAL_1: 233;

                  hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

                end;

                  case not (i = 1 & (j + 1) = ( len f));

                  then i > 1 or (j + 1) < ( len f) by A5, XXREAL_0: 1;

                  then ( LSeg (f,i)) misses ( LSeg (f,j)) by A1, A3, A6, GOBOARD5:def 4;

                  hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

                end;

              end;

              hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

            end;

              case

               A8: not (1 <= i & (j + 1) <= ( len f));

              now

                per cases by A8;

                  case 1 > i;

                  then ( LSeg (f,i)) = {} by TOPREAL1:def 3;

                  hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

                end;

                  case (j + 1) > ( len f);

                  then ( LSeg (f,j)) = {} by TOPREAL1:def 3;

                  hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

                end;

              end;

              hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

            end;

          end;

          hence thesis;

        end;

          suppose

           A9: ( len f) = 0 ;

          now

            per cases ;

              case i >= 1;

              (i + 1) > ( len f) by A9;

              then ( LSeg (f,i)) = {} by TOPREAL1:def 3;

              hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

            end;

              case i < 1;

              then ( LSeg (f,i)) = {} by TOPREAL1:def 3;

              hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis by TOPREAL1:def 7;

    end;

    theorem :: JGRAPH_1:14

    

     Th14: for f be FinSequence of ( TOP-REAL 2) st f is nodic & ( PairF f) is Simple holds f is s.c.c.

    proof

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

      assume that

       A1: f is nodic and

       A2: ( PairF f) is Simple;

      reconsider f1 = f as FinSequence of the carrier of ( PGraph the carrier of ( TOP-REAL 2));

      per cases ;

        suppose ( len f) >= 1;

        then

         A3: f1 is_oriented_vertex_seq_of ( PairF f) by Th7;

        for i, j st (i + 1) < j & (i > 1 & j < ( len f) or (j + 1) < ( len f)) holds ( LSeg (f,i)) misses ( LSeg (f,j))

        proof

          let i, j;

          assume that

           A4: (i + 1) < j and

           A5: i > 1 & j < ( len f) or (j + 1) < ( len f);

          per cases ;

            suppose

             A6: i >= 1;

            

             A7: i < j by A4, NAT_1: 13;

            then

             A8: 1 <= j by A6, XXREAL_0: 2;

            then

             A9: 1 < (j + 1) by NAT_1: 13;

            

             A10: (i + 1) < (j + 1) by A4, NAT_1: 13;

            

             A11: 1 < (i + 1) by A6, NAT_1: 13;

            

             A12: j < ( len f) by A5, NAT_1: 13;

            then

             A13: (i + 1) < ( len f) by A4, XXREAL_0: 2;

            

             A14: (j + 1) <= ( len f) by A5, NAT_1: 13;

            

             A15: i < (j + 1) by A7, NAT_1: 13;

            then

             A16: i < ( len f) by A14, XXREAL_0: 2;

            now

              assume

               A17: ( LSeg (f,i)) meets ( LSeg (f,j));

              now

                per cases by A1, A17;

                  case

                   A18: (( LSeg (f,i)) /\ ( LSeg (f,j))) = {(f . i)} & ((f . i) = (f . j) or (f . i) = (f . (j + 1))) & ( LSeg (f,i)) <> ( LSeg (f,j));

                  now

                    per cases by A18;

                      case (f . i) = (f . j);

                      hence contradiction by A2, A3, A6, A7, A12, Th1;

                    end;

                      case (f . i) = (f . (j + 1));

                      hence contradiction by A2, A3, A5, A6, A15, A14, Th1;

                    end;

                  end;

                  hence contradiction;

                end;

                  case

                   A19: (( LSeg (f,i)) /\ ( LSeg (f,j))) = {(f . (i + 1))} & ((f . (i + 1)) = (f . j) or (f . (i + 1)) = (f . (j + 1))) & ( LSeg (f,i)) <> ( LSeg (f,j));

                  now

                    per cases by A19;

                      case (f . (i + 1)) = (f . j);

                      hence contradiction by A2, A3, A4, A12, A11, Th1;

                    end;

                      case (f . (i + 1)) = (f . (j + 1));

                      hence contradiction by A2, A3, A10, A14, A11, Th1;

                    end;

                  end;

                  hence contradiction;

                end;

                  case ( LSeg (f,i)) = ( LSeg (f,j));

                  then ( LSeg ((f /. i),(f /. (i + 1)))) = ( LSeg (f,j)) by A6, A13, TOPREAL1:def 3;

                  then

                   A20: ( LSeg ((f /. i),(f /. (i + 1)))) = ( LSeg ((f /. j),(f /. (j + 1)))) by A8, A14, TOPREAL1:def 3;

                  

                   A21: (f /. j) = (f . j) & (f /. (j + 1)) = (f . (j + 1)) by A8, A12, A14, A9, FINSEQ_4: 15;

                  

                   A22: (f /. i) = (f . i) & (f /. (i + 1)) = (f . (i + 1)) by A6, A13, A16, A11, FINSEQ_4: 15;

                  now

                    per cases by A20, A22, A21, SPPOL_1: 8;

                      case (f . i) = (f . j) & (f . (i + 1)) = (f . (j + 1));

                      hence contradiction by A2, A3, A10, A14, A11, Th1;

                    end;

                      case (f . i) = (f . (j + 1)) & (f . (i + 1)) = (f . j);

                      hence contradiction by A2, A3, A4, A12, A11, Th1;

                    end;

                  end;

                  hence contradiction;

                end;

              end;

              hence contradiction;

            end;

            hence thesis;

          end;

            suppose i < 1;

            then ( LSeg (f,i)) = {} by TOPREAL1:def 3;

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

            hence thesis;

          end;

        end;

        hence thesis by GOBOARD5:def 4;

      end;

        suppose

         A23: ( len f) < 1;

        for i, j st (i + 1) < j & (i > 1 & j < ( len f) or (j + 1) < ( len f)) holds ( LSeg (f,i)) misses ( LSeg (f,j))

        proof

          let i, j;

          assume that (i + 1) < j and i > 1 & j < ( len f) or (j + 1) < ( len f);

          per cases ;

            suppose i >= 1;

            then i > ( len f) by A23, XXREAL_0: 2;

            then (i + 1) > ( len f) by NAT_1: 13;

            then ( LSeg (f,i)) = {} by TOPREAL1:def 3;

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

            hence thesis;

          end;

            suppose i < 1;

            then ( LSeg (f,i)) = {} by TOPREAL1:def 3;

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

            hence thesis;

          end;

        end;

        hence thesis by GOBOARD5:def 4;

      end;

    end;

    theorem :: JGRAPH_1:15

    

     Th15: for f be FinSequence of ( TOP-REAL 2) st f is nodic & ( PairF f) is Simple & (f . 1) <> (f . ( len f)) holds f is s.n.c.

    proof

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

      assume that

       A1: f is nodic and

       A2: ( PairF f) is Simple and

       A3: (f . 1) <> (f . ( len f));

      reconsider f1 = f as FinSequence of the carrier of ( PGraph the carrier of ( TOP-REAL 2));

      

       A4: (( len f) -' 1) <= ( len f) by NAT_D: 44;

      per cases ;

        suppose

         A5: (( len f) -' 1) > 2;

        then

         A6: (( len f) -' 1) > 1 by XXREAL_0: 2;

        then

         A7: 1 < ( len f) by NAT_D: 44;

        ( len f) >= 1 by A6, NAT_D: 44;

        then

         A8: f1 is_oriented_vertex_seq_of ( PairF f) by Th7;

        

         A9: (1 + 1) < ( len f) by A5, NAT_D: 44;

        

         A10: (( len f) -' 1) = (( len f) - 1) by A6, NAT_D: 39;

        then

         A11: ((( len f) -' 1) + 1) = ( len f);

        now

          assume

           A12: ( LSeg (f,1)) meets ( LSeg (f,(( len f) -' 1)));

          now

            per cases by A1, A12;

              case (( LSeg (f,1)) /\ ( LSeg (f,(( len f) -' 1)))) = {(f . 1)} & ((f . 1) = (f . (( len f) -' 1)) or (f . 1) = (f . ((( len f) -' 1) + 1)));

              hence contradiction by A2, A3, A4, A6, A8, A10, Th1;

            end;

              case

               A13: (( LSeg (f,1)) /\ ( LSeg (f,(( len f) -' 1)))) = {(f . (1 + 1))} & ((f . (1 + 1)) = (f . (( len f) -' 1)) or (f . (1 + 1)) = (f . ((( len f) -' 1) + 1)));

              now

                per cases by A13;

                  case (f . (1 + 1)) = (f . (( len f) -' 1));

                  hence contradiction by A2, A4, A5, A8, Th1;

                end;

                  case (f . (1 + 1)) = (f . ((( len f) -' 1) + 1));

                  hence contradiction by A2, A8, A9, A10, Th1;

                end;

              end;

              hence contradiction;

            end;

              case ( LSeg (f,1)) = ( LSeg (f,(( len f) -' 1)));

              then ( LSeg ((f /. 1),(f /. (1 + 1)))) = ( LSeg (f,(( len f) -' 1))) by A9, TOPREAL1:def 3;

              then

               A14: ( LSeg ((f /. 1),(f /. (1 + 1)))) = ( LSeg ((f /. (( len f) -' 1)),(f /. ((( len f) -' 1) + 1)))) by A6, A10, TOPREAL1:def 3;

              

               A15: (1 + 1) < ((( len f) -' 1) + 1) by A6, XREAL_1: 6;

              (( len f) -' 1) < ( len f) by A11, NAT_1: 13;

              then

               A16: (f /. (( len f) -' 1)) = (f . (( len f) -' 1)) by A6, FINSEQ_4: 15;

              1 < ( len f) by A6, NAT_D: 44;

              then

               A17: (f /. 1) = (f . 1) by FINSEQ_4: 15;

              

               A18: (f /. (1 + 1)) = (f . (1 + 1)) & (f /. ((( len f) -' 1) + 1)) = (f . ((( len f) -' 1) + 1)) by A7, A9, A10, FINSEQ_4: 15;

              now

                per cases by A14, A17, A16, A18, SPPOL_1: 8;

                  case (f . 1) = (f . (( len f) -' 1)) & (f . (1 + 1)) = (f . ((( len f) -' 1) + 1));

                  hence contradiction by A2, A8, A10, A15, Th1;

                end;

                  case (f . 1) = (f . ((( len f) -' 1) + 1)) & (f . (1 + 1)) = (f . (( len f) -' 1));

                  hence contradiction by A3, A10;

                end;

              end;

              hence contradiction;

            end;

          end;

          hence contradiction;

        end;

        hence thesis by A1, A2, Th13, Th14;

      end;

        suppose

         A19: (( len f) -' 1) <= 2;

        for i,j be Nat st (i + 1) < j holds ( LSeg (f,i)) misses ( LSeg (f,j))

        proof

          let i,j be Nat;

          assume

           A20: (i + 1) < j;

          per cases ;

            suppose

             A21: 1 <= i & (j + 1) <= ( len f);

            then 1 < (i + 1) by NAT_1: 13;

            then (1 + 1) < ((i + 1) + 1) by XREAL_1: 8;

            then

             A22: ((1 + 1) + 1) <= ((i + 1) + 1) by NAT_1: 13;

            ((i + 1) + 1) < (j + 1) by A20, XREAL_1: 6;

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

            then ((1 + 1) + 1) < ( len f) by A22, XXREAL_0: 2;

            then

             A23: (((1 + 1) + 1) - 1) < (( len f) - 1) by XREAL_1: 9;

            then 1 < (( len f) - 1) by XXREAL_0: 2;

            hence thesis by A19, A23, NAT_D: 39;

          end;

            suppose

             A24: 1 > i or (j + 1) > ( len f);

            now

              per cases by A24;

                case 1 > i;

                then ( LSeg (f,i)) = {} by TOPREAL1:def 3;

                hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

              end;

                case (j + 1) > ( len f);

                then ( LSeg (f,j)) = {} by TOPREAL1:def 3;

                hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis by TOPREAL1:def 7;

      end;

    end;

    theorem :: JGRAPH_1:16

    

     Th16: for p1,p2,p3 be Point of ( TOP-REAL n) st (ex x be set st x <> p2 & x in (( LSeg (p1,p2)) /\ ( LSeg (p2,p3)))) holds p1 in ( LSeg (p2,p3)) or p3 in ( LSeg (p1,p2))

    proof

      let p1,p2,p3 be Point of ( TOP-REAL n);

      given x be set such that

       A1: x <> p2 and

       A2: x in (( LSeg (p1,p2)) /\ ( LSeg (p2,p3)));

      reconsider p = x as Point of ( TOP-REAL n) by A2;

      

       A3: p in { (((1 - r1) * p1) + (r1 * p2)) : 0 <= r1 & r1 <= 1 } by A2, XBOOLE_0:def 4;

      

       A4: p in { (((1 - r2) * p2) + (r2 * p3)) : 0 <= r2 & r2 <= 1 } by A2, XBOOLE_0:def 4;

      consider r1 such that

       A5: p = (((1 - r1) * p1) + (r1 * p2)) and 0 <= r1 and

       A6: r1 <= 1 by A3;

      consider r2 such that

       A7: p = (((1 - r2) * p2) + (r2 * p3)) and

       A8: 0 <= r2 and r2 <= 1 by A4;

      per cases ;

        suppose

         A9: r1 >= (1 - r2);

        now

          per cases ;

            case

             A10: r2 <> 0 ;

            (r2 * p3) = ((((1 - r1) * p1) + (r1 * p2)) - ((1 - r2) * p2)) by A5, A7, RLVECT_4: 1;

            then (r2 * p3) = (((1 - r1) * p1) + ((r1 * p2) - ((1 - r2) * p2))) by RLVECT_1:def 3;

            then ((r2 " ) * (r2 * p3)) = ((r2 " ) * (((1 - r1) * p1) + ((r1 - (1 - r2)) * p2))) by RLVECT_1: 35;

            then (((r2 " ) * r2) * p3) = ((r2 " ) * (((1 - r1) * p1) + ((r1 - (1 - r2)) * p2))) by RLVECT_1:def 7;

            then (1 * p3) = ((r2 " ) * (((1 - r1) * p1) + ((r1 - (1 - r2)) * p2))) by A10, XCMPLX_0:def 7;

            

            then

             A11: p3 = ((r2 " ) * (((1 - r1) * p1) + ((r1 - (1 - r2)) * p2))) by RLVECT_1:def 8

            .= (((r2 " ) * ((1 - r1) * p1)) + ((r2 " ) * ((r1 - (1 - r2)) * p2))) by RLVECT_1:def 5

            .= ((((r2 " ) * (1 - r1)) * p1) + ((r2 " ) * ((r1 - (1 - r2)) * p2))) by RLVECT_1:def 7

            .= ((((r2 " ) * (1 - r1)) * p1) + (((r2 " ) * (r1 - (1 - r2))) * p2)) by RLVECT_1:def 7;

            r1 <= (1 + 0 qua Nat) by A6;

            then (r1 - 1) <= 0 by XREAL_1: 20;

            then ((r1 - 1) + r2) <= ( 0 qua Nat + r2) by XREAL_1: 6;

            then

             A12: ((r2 " ) * (r1 - (1 - r2))) <= ((r2 " ) * r2) by A8, XREAL_1: 64;

            (((r2 " ) * (1 - r1)) + ((r2 " ) * (r1 - (1 - r2)))) = ((r2 " ) * ((1 - 1) + r2))

            .= 1 by A10, XCMPLX_0:def 7;

            then

             A13: ((r2 " ) * (1 - r1)) = (1 - ((r2 " ) * (r1 - (1 - r2))));

            (r1 - (1 - r2)) >= 0 by A9, XREAL_1: 48;

            hence thesis by A8, A11, A13, A12;

          end;

            case r2 = 0 ;

            then p = ((1 * p2) + ( 0. ( TOP-REAL n))) by A7, RLVECT_1: 10;

            then p = (p2 + ( 0. ( TOP-REAL n))) by RLVECT_1:def 8;

            hence thesis by A1, RLVECT_1: 4;

          end;

        end;

        hence thesis;

      end;

        suppose

         A14: r1 < (1 - r2);

        set s2 = (1 - r1);

        set s1 = (1 - r2);

        ((1 - s2) + s2) <= (1 + s2) by A6, XREAL_1: 6;

        then

         A15: (1 - 1) <= s2 by XREAL_1: 20;

        

         A16: ( 0 qua Nat + s1) <= ((1 - s1) + s1) by A8, XREAL_1: 6;

        now

          per cases ;

            case

             A17: s2 <> 0 ;

            (s2 * p1) = ((((1 - s1) * p3) + (s1 * p2)) - ((1 - s2) * p2)) by A5, A7, RLVECT_4: 1

            .= (((1 - s1) * p3) + ((s1 * p2) - ((1 - s2) * p2))) by RLVECT_1:def 3

            .= (((1 - s1) * p3) + ((s1 - (1 - s2)) * p2)) by RLVECT_1: 35;

            then (((s2 " ) * s2) * p1) = ((s2 " ) * (((1 - s1) * p3) + ((s1 - (1 - s2)) * p2))) by RLVECT_1:def 7;

            then (1 * p1) = ((s2 " ) * (((1 - s1) * p3) + ((s1 - (1 - s2)) * p2))) by A17, XCMPLX_0:def 7;

            

            then p1 = ((s2 " ) * (((1 - s1) * p3) + ((s1 - (1 - s2)) * p2))) by RLVECT_1:def 8

            .= (((s2 " ) * ((1 - s1) * p3)) + ((s2 " ) * ((s1 - (1 - s2)) * p2))) by RLVECT_1:def 5

            .= ((((s2 " ) * (1 - s1)) * p3) + ((s2 " ) * ((s1 - (1 - s2)) * p2))) by RLVECT_1:def 7;

            then

             A18: p1 = ((((s2 " ) * (1 - s1)) * p3) + (((s2 " ) * (s1 - (1 - s2))) * p2)) by RLVECT_1:def 7;

            s1 <= (1 + 0 qua Nat) by A16;

            then (s1 - 1) <= 0 by XREAL_1: 20;

            then ((s1 - 1) + s2) <= ( 0 qua Nat + s2) by XREAL_1: 6;

            then

             A19: ((s2 " ) * (s1 - (1 - s2))) <= ((s2 " ) * s2) by A15, XREAL_1: 64;

            (((s2 " ) * (1 - s1)) + ((s2 " ) * (s1 - (1 - s2)))) = ((s2 " ) * ((1 - 1) + s2))

            .= 1 by A17, XCMPLX_0:def 7;

            then

             A20: ((s2 " ) * (1 - s1)) = (1 - ((s2 " ) * (s1 - (1 - s2))));

            (s1 - (1 - s2)) >= 0 by A14, XREAL_1: 48;

            then p1 in { (((1 - r) * p3) + (r * p2)) : 0 <= r & r <= 1 } by A15, A18, A20, A19;

            hence thesis by RLTOPSP1:def 2;

          end;

            case s2 = 0 ;

            then p = ((1 * p2) + ( 0. ( TOP-REAL n))) by A5, RLVECT_1: 10;

            then p = (p2 + ( 0. ( TOP-REAL n))) by RLVECT_1:def 8;

            hence thesis by A1, RLVECT_1: 4;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: JGRAPH_1:17

    

     Th17: for f be FinSequence of ( TOP-REAL 2) st f is s.n.c. & (( LSeg (f,1)) /\ ( LSeg (f,(1 + 1)))) c= {(f /. (1 + 1))} & (( LSeg (f,(( len f) -' 2))) /\ ( LSeg (f,(( len f) -' 1)))) c= {(f /. (( len f) -' 1))} holds f is unfolded

    proof

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

      assume that

       A1: f is s.n.c. and

       A2: (( LSeg (f,1)) /\ ( LSeg (f,(1 + 1)))) c= {(f /. (1 + 1))} and

       A3: (( LSeg (f,(( len f) -' 2))) /\ ( LSeg (f,(( len f) -' 1)))) c= {(f /. (( len f) -' 1))};

      for i be Nat st 1 <= i & (i + 2) <= ( len f) holds (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) = {(f /. (i + 1))}

      proof

        let i be Nat;

        assume that

         A4: 1 <= i and

         A5: (i + 2) <= ( len f);

        

         A6: 1 < (i + 1) by A4, NAT_1: 13;

        then

         A7: ( LSeg (f,(i + 1))) = ( LSeg ((f /. (i + 1)),(f /. ((i + 1) + 1)))) by A5, TOPREAL1:def 3;

        

         A8: 1 < ((i + 1) + 1) by A6, NAT_1: 13;

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

        then

         A9: (i + 1) < ( len f) by A5, NAT_1: 13;

        then

         A10: ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A4, TOPREAL1:def 3;

        (f /. (i + 1)) in ( LSeg ((f /. i),(f /. (i + 1)))) & (f /. (i + 1)) in ( LSeg ((f /. (i + 1)),(f /. ((i + 1) + 1)))) by RLTOPSP1: 68;

        then (f /. (i + 1)) in (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) by A10, A7, XBOOLE_0:def 4;

        then

         A11: {(f /. (i + 1))} c= (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) by ZFMISC_1: 31;

        

         A12: i < ( len f) by A9, NAT_1: 13;

        per cases ;

          suppose i = 1;

          hence thesis by A2, A11;

        end;

          suppose

           A13: i <> 1;

          now

            per cases ;

              case

               A14: (i + 2) = ( len f);

              then (( len f) - 2) = (( len f) -' 2) & (( len f) - 1) = (( len f) -' 1) by A4, A6, NAT_D: 39;

              hence thesis by A3, A11, A14;

            end;

              case

               A15: (i + 2) <> ( len f);

              1 < i by A4, A13, XXREAL_0: 1;

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

              then

               A16: ((1 + 1) - 1) <= (i - 1) by XREAL_1: 9;

              (i + 2) < ( len f) by A5, A15, XXREAL_0: 1;

              then

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

              now

                (f /. (i + 1)) in ( LSeg (f,(i + 1))) & (f /. (i + 1)) in ( LSeg (f,i)) by A10, A7, RLTOPSP1: 68;

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

                then

                 A18: {(f /. (i + 1))} c= (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) by ZFMISC_1: 31;

                assume (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) <> {(f /. (i + 1))};

                then not (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) c= {(f /. (i + 1))} by A18;

                then

                consider x be object such that

                 A19: x in (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) and

                 A20: not x in {(f /. (i + 1))};

                

                 A21: ( LSeg (f,((i + 1) + 1))) = ( LSeg ((f /. ((i + 1) + 1)),(f /. (((i + 1) + 1) + 1)))) by A8, A17, TOPREAL1:def 3;

                

                 A22: x <> (f /. (i + 1)) by A20, TARSKI:def 1;

                now

                  per cases by A10, A7, A19, A22, Th16;

                    case

                     A23: (f /. i) in ( LSeg ((f /. (i + 1)),(f /. ((i + 1) + 1))));

                    

                     A24: (i -' 1) = (i - 1) by A4, XREAL_1: 233;

                    then ((i -' 1) + 1) < (i + 1) by NAT_1: 13;

                    then ( LSeg (f,(i -' 1))) misses ( LSeg (f,(i + 1))) by A1, TOPREAL1:def 7;

                    then

                     A25: (( LSeg (f,(i -' 1))) /\ ( LSeg (f,(i + 1)))) = {} ;

                    ( LSeg (f,(i -' 1))) = ( LSeg ((f /. (i -' 1)),(f /. ((i -' 1) + 1)))) by A12, A16, A24, TOPREAL1:def 3;

                    then (f /. i) in ( LSeg (f,(i -' 1))) by A24, RLTOPSP1: 68;

                    hence contradiction by A7, A23, A25, XBOOLE_0:def 4;

                  end;

                    case

                     A26: (f /. ((i + 1) + 1)) in ( LSeg ((f /. i),(f /. (i + 1))));

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

                    then ( LSeg (f,i)) misses ( LSeg (f,((i + 1) + 1))) by A1, TOPREAL1:def 7;

                    then

                     A27: (( LSeg (f,i)) /\ ( LSeg (f,((i + 1) + 1)))) = {} ;

                    (f /. ((i + 1) + 1)) in ( LSeg (f,((i + 1) + 1))) by A21, RLTOPSP1: 68;

                    hence contradiction by A10, A26, A27, XBOOLE_0:def 4;

                  end;

                end;

                hence contradiction;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis by TOPREAL1:def 6;

    end;

    theorem :: JGRAPH_1:18

    

     Th18: for f be FinSequence of X holds ( PairF f) is Simple & (f . 1) <> (f . ( len f)) implies f is one-to-one & ( len f) <> 1

    proof

      let f be FinSequence of X;

      thus ( PairF f) is Simple & (f . 1) <> (f . ( len f)) implies f is one-to-one & ( len f) <> 1

      proof

        reconsider f1 = f as FinSequence of the carrier of ( PGraph X);

        assume that

         A1: ( PairF f) is Simple and

         A2: (f . 1) <> (f . ( len f));

        consider vs be FinSequence of the carrier of ( PGraph X) such that

         A3: vs is_oriented_vertex_seq_of ( PairF f) and

         A4: for n,m be Nat st 1 <= n & n < m & m <= ( len vs) & (vs . n) = (vs . m) holds n = 1 & m = ( len vs) by A1, GRAPH_4:def 7;

        now

          per cases ;

            case

             A5: ( len f) >= 1;

            now

              per cases by A5, XXREAL_0: 1;

                case

                 A6: ( len f) > 1;

                

                 A7: f1 is_oriented_vertex_seq_of ( PairF f) by A5, Th7;

                then ( len f1) = (( len ( PairF f)) + 1) by GRAPH_4:def 5;

                then (1 - 1) < ((( len ( PairF f)) + 1) - 1) by A6, XREAL_1: 9;

                then ( PairF f) <> {} ;

                then

                 A8: vs = f1 by A3, A7, GRAPH_4: 10;

                for x,y be object st x in ( dom f) & y in ( dom f) & (f . x) = (f . y) holds x = y

                proof

                  let x,y be object;

                  assume that

                   A9: x in ( dom f) and

                   A10: y in ( dom f) and

                   A11: (f . x) = (f . y);

                  reconsider i = x, j = y as Element of NAT by A9, A10;

                  

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

                  then

                   A13: i <= ( len f) by A9, FINSEQ_1: 1;

                  

                   A14: j <= ( len f) by A10, A12, FINSEQ_1: 1;

                  

                   A15: 1 <= j by A10, A12, FINSEQ_1: 1;

                  

                   A16: 1 <= i by A9, A12, FINSEQ_1: 1;

                  now

                    assume

                     A17: i <> j;

                    now

                      per cases by A17, XXREAL_0: 1;

                        case

                         A18: i < j;

                        then i = 1 by A4, A8, A11, A16, A14;

                        hence contradiction by A2, A4, A8, A11, A14, A18;

                      end;

                        case

                         A19: j < i;

                        then j = 1 by A4, A8, A11, A13, A15;

                        hence contradiction by A2, A4, A8, A11, A13, A19;

                      end;

                    end;

                    hence contradiction;

                  end;

                  hence thesis;

                end;

                hence f is one-to-one;

              end;

                case ( len f) = 1;

                hence f is one-to-one by A2;

              end;

            end;

            hence f is one-to-one;

          end;

            case ( len f) < 1;

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

            then ((( len f) + 1) - 1) <= (1 - 1) by XREAL_1: 9;

            then ( len f) = 0 ;

            then ( Seg ( len f)) = {} ;

            then for x,y be object st x in ( dom f) & y in ( dom f) & (f . x) = (f . y) holds x = y by FINSEQ_1:def 3;

            hence f is one-to-one;

          end;

        end;

        hence thesis by A2;

      end;

    end;

    theorem :: JGRAPH_1:19

    for f be FinSequence of X holds f is one-to-one & ( len f) > 1 implies ( PairF f) is Simple & (f . 1) <> (f . ( len f))

    proof

      let f be FinSequence of X;

      assume that

       A1: f is one-to-one and

       A2: ( len f) > 1;

      

       A3: 1 in ( dom f) & ( len f) in ( dom f) by A2, FINSEQ_3: 25;

      reconsider f1 = f as FinSequence of the carrier of ( PGraph X);

      

       A4: for i,j be Nat st 1 <= i & i < j & j <= ( len f1) & (f1 . i) = (f1 . j) holds i = 1 & j = ( len f1)

      proof

        let i,j be Nat;

        assume that

         A5: 1 <= i and

         A6: i < j and

         A7: j <= ( len f1) and

         A8: (f1 . i) = (f1 . j);

        1 < j by A5, A6, XXREAL_0: 2;

        then j in ( Seg ( len f)) by A7, FINSEQ_1: 1;

        then

         A9: j in ( dom f) by FINSEQ_1:def 3;

        i < ( len f) by A6, A7, XXREAL_0: 2;

        then i in ( Seg ( len f)) by A5, FINSEQ_1: 1;

        then i in ( dom f) by FINSEQ_1:def 3;

        hence thesis by A1, A6, A8, A9;

      end;

      f1 is_oriented_vertex_seq_of ( PairF f) by A2, Th7;

      hence thesis by A1, A2, A3, A4, GRAPH_4:def 7;

    end;

    theorem :: JGRAPH_1:20

    for f be FinSequence of ( TOP-REAL 2) st f is nodic & ( PairF f) is Simple & (f . 1) <> (f . ( len f)) holds f is unfolded

    proof

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

      assume that

       A1: f is nodic and

       A2: ( PairF f) is Simple & (f . 1) <> (f . ( len f));

      per cases ;

        suppose

         A3: 2 < ( len f);

        then

         A4: (2 + 1) <= ( len f) by NAT_1: 13;

        then

         A5: (2 + 1) in ( dom f) by FINSEQ_3: 25;

        

         A6: (f . 2) = (f /. 2) by A3, FINSEQ_4: 15;

        then

         A7: (f . 2) in ( LSeg (f,2)) by A4, TOPREAL1: 21;

        (1 + 1) <= ( len f) by A3;

        then (f . 2) in ( LSeg (f,1)) by A6, TOPREAL1: 21;

        then (( LSeg (f,1)) /\ ( LSeg (f,2))) <> {} by A7, XBOOLE_0:def 4;

        then

         A8: ( LSeg (f,1)) meets ( LSeg (f,2));

        

         A9: ( len f) < (( len f) + 1) by NAT_1: 13;

        then

         A10: (( len f) - 1) < ( len f) by XREAL_1: 19;

        

         A11: 2 in ( dom f) by A3, FINSEQ_3: 25;

        

         A12: ( LSeg (f,1)) = ( LSeg ((f /. 1),(f /. (1 + 1)))) by A3, TOPREAL1:def 3;

        

         A13: f is one-to-one by A2, Th18;

        

         A14: 1 < ( len f) by A3, XXREAL_0: 2;

        then

         A15: 1 in ( dom f) by FINSEQ_3: 25;

        

         A16: (f . 1) = (f /. 1) by A14, FINSEQ_4: 15;

        

         A17: (( len f) -' 2) = (( len f) - 2) by A3, XREAL_1: 233;

        

         A18: ( LSeg (f,2)) = ( LSeg ((f /. 2),(f /. (2 + 1)))) by A4, TOPREAL1:def 3;

        now

          assume

           A19: ( LSeg (f,1)) = ( LSeg (f,2));

          now

            per cases by A12, A18, A19, SPPOL_1: 8;

              case

               A20: (f /. 1) = (f /. 2) & (f /. (1 + 1)) = (f /. (2 + 1));

              (f . 1) = (f /. 1) & (f . 2) = (f /. 2) by A3, A14, FINSEQ_4: 15;

              hence contradiction by A13, A15, A11, A20;

            end;

              case

               A21: (f /. 1) = (f /. (2 + 1)) & (f /. (1 + 1)) = (f /. 2);

              (f . (2 + 1)) = (f /. (2 + 1)) by A4, FINSEQ_4: 15;

              hence contradiction by A13, A15, A16, A5, A21;

            end;

          end;

          hence contradiction;

        end;

        then (( LSeg (f,1)) /\ ( LSeg (f,2))) = {(f . 1)} & ((f . 1) = (f . 2) or (f . 1) = (f . (2 + 1))) or (( LSeg (f,1)) /\ ( LSeg (f,2))) = {(f . (1 + 1))} & ((f . (1 + 1)) = (f . 2) or (f . (1 + 1)) = (f . (2 + 1))) by A1, A8;

        then

         A22: (( LSeg (f,1)) /\ ( LSeg (f,(1 + 1)))) c= {(f /. (1 + 1))} by A3, A13, A15, A5, FINSEQ_4: 15;

        

         A23: (( len f) - 1) = (( len f) -' 1) by A3, XREAL_1: 233, XXREAL_0: 2;

        then

         A24: ((( len f) -' 1) + 1) in ( dom f) by A14, FINSEQ_3: 25;

        

         A25: ((1 + 1) - 1) <= (( len f) - 1) by A3, XREAL_1: 9;

        then

         A26: (f . (( len f) -' 1)) = (f /. (( len f) -' 1)) by A23, A10, FINSEQ_4: 15;

        

         A27: ((2 + 1) - 2) <= (( len f) - 2) by A4, XREAL_1: 9;

        then

         A28: ( LSeg (f,(( len f) -' 2))) = ( LSeg ((f /. (( len f) -' 2)),(f /. ((( len f) -' 2) + 1)))) by A17, A10, TOPREAL1:def 3;

        

         A29: ((( len f) - 1) - 1) < (( len f) - 1) by A10, XREAL_1: 9;

        then (( len f) - 2) < ( len f) by A10, XXREAL_0: 2;

        then

         A30: (f . (( len f) -' 2)) = (f /. (( len f) -' 2)) by A27, A17, FINSEQ_4: 15;

        

         A31: (( len f) -' 2) < ( len f) by A17, A10, A29, XXREAL_0: 2;

        then

         A32: (( len f) -' 2) in ( dom f) by A27, A17, FINSEQ_3: 25;

        

         A33: ( LSeg (f,(( len f) -' 1))) = ( LSeg ((f /. (( len f) -' 1)),(f /. ((( len f) -' 1) + 1)))) by A25, A23, TOPREAL1:def 3;

        

         A34: (f . (( len f) -' 2)) = (f /. (( len f) -' 2)) by A27, A17, A31, FINSEQ_4: 15;

         A35:

        now

          assume

           A36: ( LSeg (f,(( len f) -' 2))) = ( LSeg (f,(( len f) -' 1)));

          

           A37: (( len f) -' 2) in ( dom f) by A27, A17, A31, FINSEQ_3: 25;

          

           A38: (( len f) -' 1) in ( dom f) by A25, A23, A10, FINSEQ_3: 25;

          now

            per cases by A28, A33, A36, SPPOL_1: 8;

              case

               A39: (f /. (( len f) -' 2)) = (f /. (( len f) -' 1)) & (f /. ((( len f) -' 2) + 1)) = (f /. ((( len f) -' 1) + 1));

              (f . (( len f) -' 1)) = (f /. (( len f) -' 1)) by A25, A23, A10, FINSEQ_4: 15;

              hence contradiction by A13, A23, A17, A9, A34, A37, A38, A39;

            end;

              case

               A40: (f /. (( len f) -' 2)) = (f /. ((( len f) -' 1) + 1)) & (f /. ((( len f) -' 2) + 1)) = (f /. (( len f) -' 1));

              ((( len f) -' 1) + 1) in ( Seg ( len f)) by A14, A23, FINSEQ_1: 1;

              then

               A41: ((( len f) -' 1) + 1) in ( dom f) by FINSEQ_1:def 3;

              (f . ((( len f) -' 1) + 1)) = (f /. ((( len f) -' 1) + 1)) by A14, A23, FINSEQ_4: 15;

              hence contradiction by A13, A23, A17, A10, A29, A30, A37, A40, A41;

            end;

          end;

          hence contradiction;

        end;

        ((( len f) -' 1) + 1) = ( len f) by A23;

        then

         A42: (f . (( len f) -' 1)) in ( LSeg (f,(( len f) -' 1))) by A25, A26, TOPREAL1: 21;

        ((( len f) -' 2) + 1) = (( len f) - ((1 + 1) - 1)) by A17;

        then (f . (( len f) -' 1)) in ( LSeg (f,(( len f) -' 2))) by A27, A23, A10, A26, TOPREAL1: 21;

        then (( LSeg (f,(( len f) -' 2))) /\ ( LSeg (f,(( len f) -' 1)))) <> {} by A42, XBOOLE_0:def 4;

        then ( LSeg (f,(( len f) -' 2))) meets ( LSeg (f,(( len f) -' 1)));

        then (( LSeg (f,(( len f) -' 2))) /\ ( LSeg (f,(( len f) -' 1)))) = {(f . (( len f) -' 2))} & ((f . (( len f) -' 2)) = (f . (( len f) -' 1)) or (f . (( len f) -' 2)) = (f . ((( len f) -' 1) + 1))) or (( LSeg (f,(( len f) -' 2))) /\ ( LSeg (f,(( len f) -' 1)))) = {(f . ((( len f) -' 2) + 1))} & ((f . ((( len f) -' 2) + 1)) = (f . (( len f) -' 1)) or (f . ((( len f) -' 2) + 1)) = (f . ((( len f) -' 1) + 1))) by A1, A35;

        then (( LSeg (f,(( len f) -' 2))) /\ ( LSeg (f,(( len f) -' 1)))) c= {(f /. (( len f) -' 1))} by A13, A25, A23, A17, A10, A29, A32, A24, FINSEQ_4: 15;

        hence thesis by A1, A2, A22, Th15, Th17;

      end;

        suppose

         A43: ( len f) <= 2;

        for i be Nat st 1 <= i & (i + 2) <= ( len f) holds (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) = {(f /. (i + 1))}

        proof

          let i be Nat;

          assume that

           A44: 1 <= i and

           A45: (i + 2) <= ( len f);

          (i + 2) <= 2 by A43, A45, XXREAL_0: 2;

          then i <= (2 - 2) by XREAL_1: 19;

          hence thesis by A44, XXREAL_0: 2;

        end;

        hence thesis by TOPREAL1:def 6;

      end;

    end;

    theorem :: JGRAPH_1:21

    

     Th21: for f,g be FinSequence of ( TOP-REAL 2), i st g is_Shortcut_of f & 1 <= i & (i + 1) <= ( len g) holds ex k1 be Element of NAT st 1 <= k1 & (k1 + 1) <= ( len f) & (f /. k1) = (g /. i) & (f /. (k1 + 1)) = (g /. (i + 1)) & (f . k1) = (g . i) & (f . (k1 + 1)) = (g . (i + 1))

    proof

      let f,g be FinSequence of ( TOP-REAL 2), i;

      assume that

       A1: g is_Shortcut_of f and

       A2: 1 <= i and

       A3: (i + 1) <= ( len g);

      

       A4: ( len ( PairF g)) = (( len g) -' 1) by Def2;

      

       A5: i < ( len g) by A3, NAT_1: 13;

      then

       A6: (( PairF g) . i) = [(g . i), (g . (i + 1))] by A2, Def2;

      1 <= (i + 1) by A2, NAT_1: 13;

      then

       A7: (g /. (i + 1)) = (g . (i + 1)) by A3, FINSEQ_4: 15;

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

      then

       A8: (g /. i) = (g . i) by A2, FINSEQ_4: 15;

      

       A9: ( len g) <= ( len f) by A1, Th8;

      1 < ( len g) by A2, A5, XXREAL_0: 2;

      then

       A10: (( len f) -' 1) = (( len f) - 1) by A9, XREAL_1: 233, XXREAL_0: 2;

      

       A11: ( len ( PairF f)) = (( len f) -' 1) by Def2;

      

       A12: i <= (( len g) - 1) by A3, XREAL_1: 19;

      then 1 <= (( len g) - 1) by A2, XXREAL_0: 2;

      then (( len g) -' 1) = (( len g) - 1) by NAT_D: 39;

      then i in ( dom ( PairF g)) by A2, A4, A12, FINSEQ_3: 25;

      then

       A13: [(g . i), (g . (i + 1))] in ( rng ( PairF g)) by A6, FUNCT_1:def 3;

      ( rng ( PairF g)) c= ( rng ( PairF f)) by A1, Th10;

      then

      consider x be object such that

       A14: x in ( dom ( PairF f)) and

       A15: (( PairF f) . x) = [(g . i), (g . (i + 1))] by A13, FUNCT_1:def 3;

      reconsider k = x as Element of NAT by A14;

      

       A16: x in ( Seg ( len ( PairF f))) by A14, FINSEQ_1:def 3;

      then

       A17: 1 <= k by FINSEQ_1: 1;

      k <= ( len ( PairF f)) by A16, FINSEQ_1: 1;

      then

       A18: (k + 1) <= ((( len f) - 1) + 1) by A11, A10, XREAL_1: 6;

      then

       A19: k < ( len f) by NAT_1: 13;

      then [(g . i), (g . (i + 1))] = [(f . k), (f . (k + 1))] by A15, A17, Def2;

      then

       A20: (g . i) = (f . k) & (g . (i + 1)) = (f . (k + 1)) by XTUPLE_0: 1;

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

      then

       A21: (f /. (k + 1)) = (f . (k + 1)) by A18, FINSEQ_4: 15;

      (f /. k) = (f . k) by A17, A19, FINSEQ_4: 15;

      hence thesis by A17, A18, A20, A8, A7, A21;

    end;

    theorem :: JGRAPH_1:22

    

     Th22: for f,g be FinSequence of ( TOP-REAL 2) st g is_Shortcut_of f holds ( rng g) c= ( rng f)

    proof

      let f,g be FinSequence of ( TOP-REAL 2);

      assume

       A1: g is_Shortcut_of f;

      let x be object;

      assume x in ( rng g);

      then

      consider z be object such that

       A2: z in ( dom g) and

       A3: x = (g . z) by FUNCT_1:def 3;

      reconsider i = z as Element of NAT by A2;

      

       A4: z in ( Seg ( len g)) by A2, FINSEQ_1:def 3;

      then

       A5: 1 <= i by FINSEQ_1: 1;

      

       A6: i <= ( len g) by A4, FINSEQ_1: 1;

      per cases ;

        suppose i < ( len g);

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

        then

        consider k1 be Element of NAT such that

         A7: 1 <= k1 and

         A8: (k1 + 1) <= ( len f) and (f /. k1) = (g /. i) and (f /. (k1 + 1)) = (g /. (i + 1)) and

         A9: (f . k1) = (g . i) and (f . (k1 + 1)) = (g . (i + 1)) by A1, A5, Th21;

        k1 < ( len f) by A8, NAT_1: 13;

        then k1 in ( dom f) by A7, FINSEQ_3: 25;

        hence thesis by A3, A9, FUNCT_1:def 3;

      end;

        suppose i >= ( len g);

        then

         A10: i = ( len g) by A6, XXREAL_0: 1;

        now

          per cases ;

            case

             A11: 1 < i;

            then

             A12: (i -' 1) = (i - 1) by XREAL_1: 233;

            (1 - 1) < (i - 1) by A11, XREAL_1: 9;

            then 0 < (i -' 1) by A11, XREAL_1: 233;

            then ( 0 qua Nat + 1) <= (i -' 1) by NAT_1: 13;

            then

            consider k1 be Element of NAT such that

             A13: 1 <= k1 and

             A14: (k1 + 1) <= ( len f) and (f /. k1) = (g /. (i -' 1)) and (f /. (k1 + 1)) = (g /. ((i -' 1) + 1)) and (f . k1) = (g . (i -' 1)) and

             A15: (f . (k1 + 1)) = (g . ((i -' 1) + 1)) by A1, A6, A12, Th21;

            1 < (k1 + 1) by A13, NAT_1: 13;

            then (k1 + 1) in ( dom f) by A14, FINSEQ_3: 25;

            hence thesis by A3, A12, A15, FUNCT_1:def 3;

          end;

            case 1 >= i;

            then

             A16: i = 1 by A5, XXREAL_0: 1;

            

             A17: (f . 1) = (g . 1) by A1;

            ( len g) <= ( len f) by A1, Th8;

            then 1 in ( dom f) by A10, A16, FINSEQ_3: 25;

            hence thesis by A3, A16, A17, FUNCT_1:def 3;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: JGRAPH_1:23

    

     Th23: for f,g be FinSequence of ( TOP-REAL 2) st g is_Shortcut_of f holds ( L~ g) c= ( L~ f)

    proof

      let f,g be FinSequence of ( TOP-REAL 2);

      assume

       A1: g is_Shortcut_of f;

      let x be object;

      assume x in ( L~ g);

      then x in ( union { ( LSeg (g,i)) : 1 <= i & (i + 1) <= ( len g) }) by TOPREAL1:def 4;

      then

      consider y such that

       A2: x in y & y in { ( LSeg (g,i)) : 1 <= i & (i + 1) <= ( len g) } by TARSKI:def 4;

      consider i such that

       A3: y = ( LSeg (g,i)) and

       A4: 1 <= i & (i + 1) <= ( len g) by A2;

      consider k1 be Element of NAT such that

       A5: 1 <= k1 & (k1 + 1) <= ( len f) and

       A6: (f /. k1) = (g /. i) & (f /. (k1 + 1)) = (g /. (i + 1)) and (f . k1) = (g . i) and (f . (k1 + 1)) = (g . (i + 1)) by A1, A4, Th21;

      

       A7: ( LSeg (f,k1)) in { ( LSeg (f,k)) : 1 <= k & (k + 1) <= ( len f) } by A5;

      x in ( LSeg ((g /. i),(g /. (i + 1)))) by A2, A3, A4, TOPREAL1:def 3;

      then x in ( LSeg (f,k1)) by A5, A6, TOPREAL1:def 3;

      then x in ( union { ( LSeg (f,k)) : 1 <= k & (k + 1) <= ( len f) }) by A7, TARSKI:def 4;

      hence thesis by TOPREAL1:def 4;

    end;

    theorem :: JGRAPH_1:24

    

     Th24: for f,g be FinSequence of ( TOP-REAL 2) st f is special & g is_Shortcut_of f holds g is special

    proof

      let f,g be FinSequence of ( TOP-REAL 2);

      assume that

       A1: f is special and

       A2: g is_Shortcut_of f;

      for i be Nat st 1 <= i & (i + 1) <= ( len g) holds ((g /. i) `1 ) = ((g /. (i + 1)) `1 ) or ((g /. i) `2 ) = ((g /. (i + 1)) `2 )

      proof

        

         A3: ( len g) <= ( len f) by A2, Th8;

        

         A4: ( len ( PairF g)) = (( len g) -' 1) by Def2;

        let i be Nat;

        assume that

         A5: 1 <= i and

         A6: (i + 1) <= ( len g);

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

        then

         A7: (g /. i) = (g . i) by A5, FINSEQ_4: 15;

        

         A8: i < ( len g) by A6, NAT_1: 13;

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

        then

         A9: (( len f) -' 1) = (( len f) - 1) by A3, XREAL_1: 233, XXREAL_0: 2;

        

         A10: i <= (( len g) - 1) by A6, XREAL_1: 19;

        then 1 <= (( len g) - 1) by A5, XXREAL_0: 2;

        then (( len g) -' 1) = (( len g) - 1) by NAT_D: 39;

        then

         A11: i in ( dom ( PairF g)) by A5, A4, A10, FINSEQ_3: 25;

        (( PairF g) . i) = [(g . i), (g . (i + 1))] by A5, A8, Def2;

        then

         A12: [(g . i), (g . (i + 1))] in ( rng ( PairF g)) by A11, FUNCT_1:def 3;

        ( rng ( PairF g)) c= ( rng ( PairF f)) by A2, Th10;

        then

        consider x be object such that

         A13: x in ( dom ( PairF f)) and

         A14: (( PairF f) . x) = [(g . i), (g . (i + 1))] by A12, FUNCT_1:def 3;

        reconsider k = x as Element of NAT by A13;

        

         A15: x in ( Seg ( len ( PairF f))) by A13, FINSEQ_1:def 3;

        then

         A16: 1 <= k by FINSEQ_1: 1;

        1 <= (i + 1) by A5, NAT_1: 13;

        then

         A17: (g /. (i + 1)) = (g . (i + 1)) by A6, FINSEQ_4: 15;

        

         A18: ( len ( PairF f)) = (( len f) -' 1) by Def2;

        k <= ( len ( PairF f)) by A15, FINSEQ_1: 1;

        then

         A19: (k + 1) <= ((( len f) - 1) + 1) by A18, A9, XREAL_1: 6;

        then

         A20: k < ( len f) by NAT_1: 13;

        then (( PairF f) . k) = [(f . k), (f . (k + 1))] by A16, Def2;

        then

         A21: (g . i) = (f . k) & (g . (i + 1)) = (f . (k + 1)) by A14, XTUPLE_0: 1;

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

        then

         A22: (f /. (k + 1)) = (f . (k + 1)) by A19, FINSEQ_4: 15;

        (f /. k) = (f . k) by A16, A20, FINSEQ_4: 15;

        hence thesis by A1, A16, A19, A21, A7, A17, A22, TOPREAL1:def 5;

      end;

      hence thesis by TOPREAL1:def 5;

    end;

    theorem :: JGRAPH_1:25

    

     Th25: for f be FinSequence of ( TOP-REAL 2) st f is special & 2 <= ( len f) & (f . 1) <> (f . ( len f)) holds ex g be FinSequence of ( TOP-REAL 2) st 2 <= ( len g) & g is special & g is one-to-one & ( L~ g) c= ( L~ f) & (f . 1) = (g . 1) & (f . ( len f)) = (g . ( len g)) & ( rng g) c= ( rng f)

    proof

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

      assume that

       A1: f is special and

       A2: 2 <= ( len f) and

       A3: (f . 1) <> (f . ( len f));

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

       A4: g is_Shortcut_of f by A2, Th9, XXREAL_0: 2;

      

       A5: (g . 1) = (f . 1) & (g . ( len g)) = (f . ( len f)) by A4;

      1 <= ( len g) by A4, Th8;

      then 1 < ( len g) by A3, A5, XXREAL_0: 1;

      then

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

      

       A7: ( L~ g) c= ( L~ f) & ( rng g) c= ( rng f) by A4, Th22, Th23;

      g is one-to-one by A3, A4, Th11;

      hence thesis by A1, A4, A7, A6, Th24;

    end;

    theorem :: JGRAPH_1:26

    

     Th26: for f1,f2 be FinSequence of ( TOP-REAL 2) st f1 is special & f2 is special & 2 <= ( len f1) & 2 <= ( len f2) & (f1 . 1) <> (f1 . ( len f1)) & (f2 . 1) <> (f2 . ( len f2)) & ( X_axis f1) lies_between ((( X_axis f1) . 1),(( X_axis f1) . ( len f1))) & ( X_axis f2) lies_between ((( X_axis f1) . 1),(( X_axis f1) . ( len f1))) & ( Y_axis f1) lies_between ((( Y_axis f2) . 1),(( Y_axis f2) . ( len f2))) & ( Y_axis f2) lies_between ((( Y_axis f2) . 1),(( Y_axis f2) . ( len f2))) holds ( L~ f1) meets ( L~ f2)

    proof

      let f1,f2 be FinSequence of ( TOP-REAL 2);

      assume that

       A1: f1 is special and

       A2: f2 is special and

       A3: 2 <= ( len f1) and

       A4: 2 <= ( len f2) and

       A5: (f1 . 1) <> (f1 . ( len f1)) and

       A6: (f2 . 1) <> (f2 . ( len f2)) and

       A7: ( X_axis f1) lies_between ((( X_axis f1) . 1),(( X_axis f1) . ( len f1))) and

       A8: ( X_axis f2) lies_between ((( X_axis f1) . 1),(( X_axis f1) . ( len f1))) and

       A9: ( Y_axis f1) lies_between ((( Y_axis f2) . 1),(( Y_axis f2) . ( len f2))) and

       A10: ( Y_axis f2) lies_between ((( Y_axis f2) . 1),(( Y_axis f2) . ( len f2)));

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

       A11: 2 <= ( len g1) and

       A12: g1 is special and

       A13: g1 is one-to-one and

       A14: ( L~ g1) c= ( L~ f1) and

       A15: (f1 . 1) = (g1 . 1) and

       A16: (f1 . ( len f1)) = (g1 . ( len g1)) and

       A17: ( rng g1) c= ( rng f1) by A1, A3, A5, Th25;

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

       A18: 2 <= ( len g2) and

       A19: g2 is special and

       A20: g2 is one-to-one and

       A21: ( L~ g2) c= ( L~ f2) and

       A22: (f2 . 1) = (g2 . 1) and

       A23: (f2 . ( len f2)) = (g2 . ( len g2)) and

       A24: ( rng g2) c= ( rng f2) by A2, A4, A6, Th25;

      

       A25: for k be Nat st k in ( dom g2) & (k + 1) in ( dom g2) holds (g2 /. k) <> (g2 /. (k + 1))

      proof

        let k be Nat;

        assume that

         A26: k in ( dom g2) and

         A27: (k + 1) in ( dom g2);

        

         A28: (g2 . k) = (g2 /. k) by A26, PARTFUN1:def 6;

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

        then (g2 . k) <> (g2 . (k + 1)) by A20, A26, A27;

        hence thesis by A27, A28, PARTFUN1:def 6;

      end;

      for i st i in ( dom ( Y_axis g1)) holds (( Y_axis g2) . 1) <= (( Y_axis g1) . i) & (( Y_axis g1) . i) <= (( Y_axis g2) . ( len g2))

      proof

        let i;

        

         A29: ( len ( Y_axis f2)) = ( len f2) by GOBOARD1:def 2;

        

         A30: 1 <= ( len f2) by A4, XXREAL_0: 2;

        then 1 in ( Seg ( len f2)) by FINSEQ_1: 1;

        then

         A31: 1 in ( dom ( Y_axis f2)) by A29, FINSEQ_1:def 3;

        ( len f2) in ( Seg ( len f2)) by A30, FINSEQ_1: 1;

        then

         A32: ( len f2) in ( dom ( Y_axis f2)) by A29, FINSEQ_1:def 3;

        

         A33: ( len ( Y_axis g2)) = ( len g2) by GOBOARD1:def 2;

        

         A34: 1 <= ( len g2) by A18, XXREAL_0: 2;

        then 1 in ( Seg ( len g2)) by FINSEQ_1: 1;

        then

         A35: 1 in ( dom ( Y_axis g2)) by A33, FINSEQ_1:def 3;

        (g2 /. 1) = (g2 . 1) by A34, FINSEQ_4: 15;

        then

         A36: (g2 /. 1) = (f2 /. 1) by A22, A30, FINSEQ_4: 15;

        ( len g2) in ( Seg ( len g2)) by A34, FINSEQ_1: 1;

        then

         A37: ( len g2) in ( dom ( Y_axis g2)) by A33, FINSEQ_1:def 3;

        (g2 /. ( len g2)) = (g2 . ( len g2)) by A34, FINSEQ_4: 15;

        then

         A38: (g2 /. ( len g2)) = (f2 /. ( len f2)) by A23, A30, FINSEQ_4: 15;

        assume

         A39: i in ( dom ( Y_axis g1));

        then

         A40: (( Y_axis g1) . i) = ((g1 /. i) `2 ) by GOBOARD1:def 2;

        ( len ( Y_axis g1)) = ( len g1) by GOBOARD1:def 2;

        then i in ( Seg ( len g1)) by A39, FINSEQ_1:def 3;

        then

         A41: i in ( dom g1) by FINSEQ_1:def 3;

        then (g1 . i) in ( rng g1) by FUNCT_1:def 3;

        then

        consider y be object such that

         A42: y in ( dom f1) and

         A43: (g1 . i) = (f1 . y) by A17, FUNCT_1:def 3;

        reconsider j = y as Element of NAT by A42;

        (f1 . j) = (f1 /. j) by A42, PARTFUN1:def 6;

        then

         A44: (g1 /. i) = (f1 /. j) by A41, A43, PARTFUN1:def 6;

        ( len ( Y_axis f1)) = ( len f1) & j in ( Seg ( len f1)) by A42, FINSEQ_1:def 3, GOBOARD1:def 2;

        then

         A45: j in ( dom ( Y_axis f1)) by FINSEQ_1:def 3;

        then

         A46: (( Y_axis f1) . j) = ((f1 /. j) `2 ) by GOBOARD1:def 2;

        (( Y_axis f1) . j) <= (( Y_axis f2) . ( len f2)) by A9, A45, GOBOARD4:def 2;

        then

         A47: ((g1 /. i) `2 ) <= ((g2 /. ( len g2)) `2 ) by A38, A44, A46, A32, GOBOARD1:def 2;

        (( Y_axis f2) . 1) <= (( Y_axis f1) . j) by A9, A45, GOBOARD4:def 2;

        then ((g2 /. 1) `2 ) <= ((g1 /. i) `2 ) by A36, A31, A44, A46, GOBOARD1:def 2;

        hence thesis by A35, A47, A40, A37, GOBOARD1:def 2;

      end;

      then

       A48: ( Y_axis g1) lies_between ((( Y_axis g2) . 1),(( Y_axis g2) . ( len g2))) by GOBOARD4:def 2;

      for i st i in ( dom ( X_axis g2)) holds (( X_axis g1) . 1) <= (( X_axis g2) . i) & (( X_axis g2) . i) <= (( X_axis g1) . ( len g1))

      proof

        let i;

        

         A49: ( len ( X_axis f1)) = ( len f1) by GOBOARD1:def 1;

        

         A50: 1 <= ( len f1) by A3, XXREAL_0: 2;

        then 1 in ( Seg ( len f1)) by FINSEQ_1: 1;

        then

         A51: 1 in ( dom ( X_axis f1)) by A49, FINSEQ_1:def 3;

        ( len f1) in ( Seg ( len f1)) by A50, FINSEQ_1: 1;

        then

         A52: ( len f1) in ( dom ( X_axis f1)) by A49, FINSEQ_1:def 3;

        

         A53: ( len ( X_axis g1)) = ( len g1) by GOBOARD1:def 1;

        

         A54: 1 <= ( len g1) by A11, XXREAL_0: 2;

        then 1 in ( Seg ( len g1)) by FINSEQ_1: 1;

        then

         A55: 1 in ( dom ( X_axis g1)) by A53, FINSEQ_1:def 3;

        (g1 /. 1) = (g1 . 1) by A54, FINSEQ_4: 15;

        then

         A56: (g1 /. 1) = (f1 /. 1) by A15, A50, FINSEQ_4: 15;

        ( len g1) in ( Seg ( len g1)) by A54, FINSEQ_1: 1;

        then

         A57: ( len g1) in ( dom ( X_axis g1)) by A53, FINSEQ_1:def 3;

        (g1 /. ( len g1)) = (g1 . ( len g1)) by A54, FINSEQ_4: 15;

        then

         A58: (g1 /. ( len g1)) = (f1 /. ( len f1)) by A16, A50, FINSEQ_4: 15;

        assume

         A59: i in ( dom ( X_axis g2));

        then

         A60: (( X_axis g2) . i) = ((g2 /. i) `1 ) by GOBOARD1:def 1;

        ( len ( X_axis g2)) = ( len g2) by GOBOARD1:def 1;

        then i in ( Seg ( len g2)) by A59, FINSEQ_1:def 3;

        then

         A61: i in ( dom g2) by FINSEQ_1:def 3;

        then (g2 . i) in ( rng g2) by FUNCT_1:def 3;

        then

        consider y be object such that

         A62: y in ( dom f2) and

         A63: (g2 . i) = (f2 . y) by A24, FUNCT_1:def 3;

        reconsider j = y as Element of NAT by A62;

        (f2 . j) = (f2 /. j) by A62, PARTFUN1:def 6;

        then

         A64: (g2 /. i) = (f2 /. j) by A61, A63, PARTFUN1:def 6;

        ( len ( X_axis f2)) = ( len f2) & j in ( Seg ( len f2)) by A62, FINSEQ_1:def 3, GOBOARD1:def 1;

        then

         A65: j in ( dom ( X_axis f2)) by FINSEQ_1:def 3;

        then

         A66: (( X_axis f2) . j) = ((f2 /. j) `1 ) by GOBOARD1:def 1;

        (( X_axis f2) . j) <= (( X_axis f1) . ( len f1)) by A8, A65, GOBOARD4:def 2;

        then

         A67: ((g2 /. i) `1 ) <= ((g1 /. ( len g1)) `1 ) by A58, A64, A66, A52, GOBOARD1:def 1;

        (( X_axis f1) . 1) <= (( X_axis f2) . j) by A8, A65, GOBOARD4:def 2;

        then ((g1 /. 1) `1 ) <= ((g2 /. i) `1 ) by A56, A51, A64, A66, GOBOARD1:def 1;

        hence thesis by A55, A67, A60, A57, GOBOARD1:def 1;

      end;

      then

       A68: ( X_axis g2) lies_between ((( X_axis g1) . 1),(( X_axis g1) . ( len g1))) by GOBOARD4:def 2;

      for i st i in ( dom ( Y_axis g2)) holds (( Y_axis g2) . 1) <= (( Y_axis g2) . i) & (( Y_axis g2) . i) <= (( Y_axis g2) . ( len g2))

      proof

        let i;

        

         A69: ( len ( Y_axis f2)) = ( len f2) by GOBOARD1:def 2;

        

         A70: 1 <= ( len f2) by A4, XXREAL_0: 2;

        then 1 in ( Seg ( len f2)) by FINSEQ_1: 1;

        then

         A71: 1 in ( dom ( Y_axis f2)) by A69, FINSEQ_1:def 3;

        

         A72: 1 <= ( len g2) by A18, XXREAL_0: 2;

        then (g2 /. 1) = (g2 . 1) by FINSEQ_4: 15;

        then

         A73: (g2 /. 1) = (f2 /. 1) by A22, A70, FINSEQ_4: 15;

        

         A74: ( len ( Y_axis g2)) = ( len g2) by GOBOARD1:def 2;

        then ( len g2) in ( Seg ( len ( Y_axis g2))) by A72, FINSEQ_1: 1;

        then

         A75: ( len g2) in ( dom ( Y_axis g2)) by FINSEQ_1:def 3;

        (g2 /. ( len g2)) = (g2 . ( len g2)) by A72, FINSEQ_4: 15;

        then

         A76: (g2 /. ( len g2)) = (f2 /. ( len f2)) by A23, A70, FINSEQ_4: 15;

        1 in ( Seg ( len g2)) by A72, FINSEQ_1: 1;

        then

         A77: 1 in ( dom ( Y_axis g2)) by A74, FINSEQ_1:def 3;

        ( len f2) in ( Seg ( len f2)) by A70, FINSEQ_1: 1;

        then

         A78: ( len f2) in ( dom ( Y_axis f2)) by A69, FINSEQ_1:def 3;

        assume

         A79: i in ( dom ( Y_axis g2));

        then

         A80: (( Y_axis g2) . i) = ((g2 /. i) `2 ) by GOBOARD1:def 2;

        i in ( Seg ( len g2)) by A79, A74, FINSEQ_1:def 3;

        then

         A81: i in ( dom g2) by FINSEQ_1:def 3;

        then (g2 . i) in ( rng g2) by FUNCT_1:def 3;

        then

        consider y be object such that

         A82: y in ( dom f2) and

         A83: (g2 . i) = (f2 . y) by A24, FUNCT_1:def 3;

        reconsider j = y as Element of NAT by A82;

        (f2 . j) = (f2 /. j) by A82, PARTFUN1:def 6;

        then

         A84: (g2 /. i) = (f2 /. j) by A81, A83, PARTFUN1:def 6;

        j in ( Seg ( len f2)) by A82, FINSEQ_1:def 3;

        then

         A85: j in ( dom ( Y_axis f2)) by A69, FINSEQ_1:def 3;

        then

         A86: (( Y_axis f2) . j) = ((f2 /. j) `2 ) by GOBOARD1:def 2;

        (( Y_axis f2) . j) <= (( Y_axis f2) . ( len f2)) by A10, A85, GOBOARD4:def 2;

        then

         A87: ((g2 /. i) `2 ) <= ((g2 /. ( len g2)) `2 ) by A76, A84, A86, A78, GOBOARD1:def 2;

        (( Y_axis f2) . 1) <= (( Y_axis f2) . j) by A10, A85, GOBOARD4:def 2;

        then ((g2 /. 1) `2 ) <= ((g2 /. i) `2 ) by A73, A71, A84, A86, GOBOARD1:def 2;

        hence thesis by A77, A87, A80, A75, GOBOARD1:def 2;

      end;

      then

       A88: ( Y_axis g2) lies_between ((( Y_axis g2) . 1),(( Y_axis g2) . ( len g2))) by GOBOARD4:def 2;

      for i st i in ( dom ( X_axis g1)) holds (( X_axis g1) . 1) <= (( X_axis g1) . i) & (( X_axis g1) . i) <= (( X_axis g1) . ( len g1))

      proof

        let i;

        

         A89: ( len ( X_axis f1)) = ( len f1) by GOBOARD1:def 1;

        assume

         A90: i in ( dom ( X_axis g1));

        then

         A91: (( X_axis g1) . i) = ((g1 /. i) `1 ) by GOBOARD1:def 1;

        

         A92: 1 <= ( len f1) by A3, XXREAL_0: 2;

        then ( len f1) in ( Seg ( len f1)) by FINSEQ_1: 1;

        then

         A93: ( len f1) in ( dom ( X_axis f1)) by A89, FINSEQ_1:def 3;

        

         A94: 1 <= ( len g1) by A11, XXREAL_0: 2;

        then (g1 /. 1) = (g1 . 1) by FINSEQ_4: 15;

        then

         A95: (g1 /. 1) = (f1 /. 1) by A15, A92, FINSEQ_4: 15;

        (g1 /. ( len g1)) = (g1 . ( len g1)) by A94, FINSEQ_4: 15;

        then

         A96: (g1 /. ( len g1)) = (f1 /. ( len f1)) by A16, A92, FINSEQ_4: 15;

        

         A97: ( len ( X_axis g1)) = ( len g1) by GOBOARD1:def 1;

        then

         A98: 1 in ( dom ( X_axis g1)) by A94, FINSEQ_3: 25;

        i in ( Seg ( len g1)) by A90, A97, FINSEQ_1:def 3;

        then

         A99: i in ( dom g1) by FINSEQ_1:def 3;

        then (g1 . i) in ( rng g1) by FUNCT_1:def 3;

        then

        consider y be object such that

         A100: y in ( dom f1) and

         A101: (g1 . i) = (f1 . y) by A17, FUNCT_1:def 3;

        reconsider j = y as Element of NAT by A100;

        (f1 . j) = (f1 /. j) by A100, PARTFUN1:def 6;

        then

         A102: (g1 /. i) = (f1 /. j) by A99, A101, PARTFUN1:def 6;

        ( len g1) in ( Seg ( len g1)) by A94, FINSEQ_1: 1;

        then

         A103: ( len g1) in ( dom ( X_axis g1)) by A97, FINSEQ_1:def 3;

        j in ( Seg ( len f1)) by A100, FINSEQ_1:def 3;

        then

         A104: j in ( dom ( X_axis f1)) by A89, FINSEQ_1:def 3;

        then

         A105: (( X_axis f1) . j) = ((f1 /. j) `1 ) by GOBOARD1:def 1;

        (( X_axis f1) . j) <= (( X_axis f1) . ( len f1)) by A7, A104, GOBOARD4:def 2;

        then

         A106: ((g1 /. i) `1 ) <= ((g1 /. ( len g1)) `1 ) by A96, A102, A105, A93, GOBOARD1:def 1;

        

         A107: (( X_axis f1) . 1) <= (( X_axis f1) . j) by A7, A104, GOBOARD4:def 2;

        1 in ( dom ( X_axis f1)) by A89, A92, FINSEQ_3: 25;

        then ((g1 /. 1) `1 ) <= ((g1 /. i) `1 ) by A95, A102, A107, A105, GOBOARD1:def 1;

        hence thesis by A98, A106, A91, A103, GOBOARD1:def 1;

      end;

      then

       A108: ( X_axis g1) lies_between ((( X_axis g1) . 1),(( X_axis g1) . ( len g1))) by GOBOARD4:def 2;

      for k be Nat st k in ( dom g1) & (k + 1) in ( dom g1) holds (g1 /. k) <> (g1 /. (k + 1))

      proof

        let k be Nat;

        assume that

         A109: k in ( dom g1) and

         A110: (k + 1) in ( dom g1);

        

         A111: (g1 . k) = (g1 /. k) by A109, PARTFUN1:def 6;

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

        then (g1 . k) <> (g1 . (k + 1)) by A13, A109, A110;

        hence thesis by A110, A111, PARTFUN1:def 6;

      end;

      then ( L~ g1) meets ( L~ g2) by A11, A12, A18, A19, A108, A68, A48, A88, A25, GOBOARD4: 4;

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

      then (( L~ f1) /\ ( L~ f2)) <> {} by A14, A21, XBOOLE_1: 3, XBOOLE_1: 27;

      hence thesis;

    end;

    begin

    theorem :: JGRAPH_1:27

    

     Th27: for a,b,r1,r2 be Real st a <= r1 & r1 <= b & a <= r2 & r2 <= b holds |.(r1 - r2).| <= (b - a)

    proof

      let a,b,r1,r2 be Real;

      assume that

       A1: a <= r1 and

       A2: r1 <= b & a <= r2 and

       A3: r2 <= b;

      per cases ;

        suppose

         A4: (r1 - r2) >= 0 ;

        

         A5: (r1 - r2) <= (b - r2) & (b - r2) <= (b - a) by A2, XREAL_1: 9, XREAL_1: 10;

         |.(r1 - r2).| = (r1 - r2) by A4, ABSVALUE:def 1;

        hence thesis by A5, XXREAL_0: 2;

      end;

        suppose (r1 - r2) < 0 ;

        

        then

         A6: |.(r1 - r2).| = ( - (r1 - r2)) by ABSVALUE:def 1

        .= (r2 - r1);

        (r2 - r1) <= (b - r1) & (b - r1) <= (b - a) by A1, A3, XREAL_1: 9, XREAL_1: 10;

        hence thesis by A6, XXREAL_0: 2;

      end;

    end;

    reserve p,p1,p2 for Point of ( TOP-REAL N);

    theorem :: JGRAPH_1:28

    

     Th28: for x1,x2 be Point of ( Euclid N) st x1 = p1 & x2 = p2 holds |.(p1 - p2).| = ( dist (x1,x2))

    proof

      let x1,x2 be Point of ( Euclid N);

      assume

       A1: x1 = p1 & x2 = p2;

      reconsider x19 = x1, x29 = x2 as Element of ( REAL N);

      (( Pitag_dist N) . (x19,x29)) = |.(x19 - x29).| by EUCLID:def 6

      .= |.(p1 - p2).| by A1;

      hence thesis by METRIC_1:def 1;

    end;

    theorem :: JGRAPH_1:29

    

     Th29: for p be Point of ( TOP-REAL 2) holds ( |.p.| ^2 ) = (((p `1 ) ^2 ) + ((p `2 ) ^2 ))

    proof

      let p be Point of ( TOP-REAL 2);

      reconsider w = p as Element of ( REAL 2) by EUCLID: 22;

      

       A1: (( sqr w) . 2) = ((p `2 ) ^2 ) by VALUED_1: 11;

       0 <= ( Sum ( sqr w)) by RVSUM_1: 86;

      then

       A2: ( |.p.| ^2 ) = ( Sum ( sqr w)) by SQUARE_1:def 2;

      ( len ( sqr w)) = 2 & (( sqr w) . 1) = ((p `1 ) ^2 ) by CARD_1:def 7, VALUED_1: 11;

      then ( sqr w) = <*((p `1 ) ^2 ), ((p `2 ) ^2 )*> by A1, FINSEQ_1: 44;

      hence thesis by A2, RVSUM_1: 77;

    end;

    theorem :: JGRAPH_1:30

    

     Th30: for p be Point of ( TOP-REAL 2) holds |.p.| = ( sqrt (((p `1 ) ^2 ) + ((p `2 ) ^2 )))

    proof

      let p be Point of ( TOP-REAL 2);

      ( |.p.| ^2 ) = (((p `1 ) ^2 ) + ((p `2 ) ^2 )) by Th29;

      hence thesis by SQUARE_1: 22;

    end;

    theorem :: JGRAPH_1:31

    

     Th31: for p be Point of ( TOP-REAL 2) holds |.p.| <= ( |.(p `1 ).| + |.(p `2 ).|)

    proof

      let p be Point of ( TOP-REAL 2);

      ( |.p.| ^2 ) = (((p `1 ) ^2 ) + ((p `2 ) ^2 )) by Th29;

      then ( sqrt (((p `1 ) ^2 ) + ((p `2 ) ^2 ))) = |.p.| by SQUARE_1: 22;

      hence thesis by COMPLEX1: 78;

    end;

    theorem :: JGRAPH_1:32

    

     Th32: for p1,p2 be Point of ( TOP-REAL 2) holds |.(p1 - p2).| <= ( |.((p1 `1 ) - (p2 `1 )).| + |.((p1 `2 ) - (p2 `2 )).|)

    proof

      let p1,p2 be Point of ( TOP-REAL 2);

      ((p1 `1 ) - (p2 `1 )) = ((p1 - p2) `1 ) & ((p1 `2 ) - (p2 `2 )) = ((p1 - p2) `2 ) by TOPREAL3: 3;

      hence thesis by Th31;

    end;

    theorem :: JGRAPH_1:33

    

     Th33: for p be Point of ( TOP-REAL 2) holds |.(p `1 ).| <= |.p.| & |.(p `2 ).| <= |.p.|

    proof

      let p be Point of ( TOP-REAL 2);

       |.p.| = ( sqrt (((p `1 ) ^2 ) + ((p `2 ) ^2 ))) by Th30;

      hence thesis by COMPLEX1: 79;

    end;

    theorem :: JGRAPH_1:34

    

     Th34: for p1,p2 be Point of ( TOP-REAL 2) holds |.((p1 `1 ) - (p2 `1 )).| <= |.(p1 - p2).| & |.((p1 `2 ) - (p2 `2 )).| <= |.(p1 - p2).|

    proof

      let p1,p2 be Point of ( TOP-REAL 2);

      ((p1 `1 ) - (p2 `1 )) = ((p1 - p2) `1 ) & ((p1 `2 ) - (p2 `2 )) = ((p1 - p2) `2 ) by TOPREAL3: 3;

      hence thesis by Th33;

    end;

    ::$Canceled

    theorem :: JGRAPH_1:36

    

     Th35: p in ( LSeg (p1,p2)) implies |.(p - p1).| <= |.(p1 - p2).| & |.(p - p2).| <= |.(p1 - p2).|

    proof

      assume

       A1: p in ( LSeg (p1,p2));

      then

      consider r such that

       A2: 0 <= r and

       A3: r <= 1 and

       A4: p = (((1 - r) * p1) + (r * p2)) by RLTOPSP1: 76;

      

       A5: 0 <= (1 - r) by A3, XREAL_1: 48;

      (p - p1) = ((((1 - r) * p1) - p1) + (r * p2)) by A4, RLVECT_1:def 3

      .= ((((1 - r) * p1) - (1 * p1)) + (r * p2)) by RLVECT_1:def 8

      .= ((((1 + ( - r)) - 1) * p1) + (r * p2)) by RLVECT_1: 35

      .= ((r * p2) + ( - (r * p1))) by RLVECT_1: 79

      .= ((r * p2) + (r * ( - p1))) by RLVECT_1: 25

      .= (r * (p2 - p1)) by RLVECT_1:def 5;

      

      then |.(p - p1).| = ( |.r.| * |.(p2 - p1).|) by TOPRNS_1: 7

      .= ( |.r.| * |.(p1 - p2).|) by TOPRNS_1: 27

      .= (r * |.(p1 - p2).|) by A2, ABSVALUE:def 1;

      then

       A6: ( |.(p1 - p2).| - |.(p - p1).|) = ((1 - r) * |.(p1 - p2).|);

      consider r such that

       A7: 0 <= r and

       A8: r <= 1 and

       A9: p = (((1 - r) * p2) + (r * p1)) by A1, RLTOPSP1: 76;

      (p - p2) = ((((1 - r) * p2) + ( - p2)) + (r * p1)) by A9, RLVECT_1:def 3

      .= ((((1 - r) * p2) - (1 * p2)) + (r * p1)) by RLVECT_1:def 8

      .= ((((1 + ( - r)) - 1) * p2) + (r * p1)) by RLVECT_1: 35

      .= ((r * p1) + ( - (r * p2))) by RLVECT_1: 79

      .= ((r * p1) + (r * ( - p2))) by RLVECT_1: 25

      .= (r * (p1 - p2)) by RLVECT_1:def 5;

      

      then |.(p - p2).| = ( |.r.| * |.(p1 - p2).|) by TOPRNS_1: 7

      .= (r * |.(p1 - p2).|) by A7, ABSVALUE:def 1;

      then

       A10: ( |.(p1 - p2).| - |.(p - p2).|) = ((1 - r) * |.(p1 - p2).|);

       0 <= (1 - r) by A8, XREAL_1: 48;

      hence thesis by A6, A5, A10, XREAL_1: 49;

    end;

    begin

    reserve M for non empty MetrSpace;

    theorem :: JGRAPH_1:37

    

     Th36: for P,Q be Subset of ( TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ( min_dist_min (P,Q)) >= 0

    proof

      let P,Q be Subset of ( TopSpaceMetr M);

      assume P <> {} & P is compact & Q <> {} & Q is compact;

      then ex x1,x2 be Point of M st x1 in P & x2 in Q & ( dist (x1,x2)) = ( min_dist_min (P,Q)) by WEIERSTR: 30;

      hence thesis by METRIC_1: 5;

    end;

    theorem :: JGRAPH_1:38

    

     Th37: for P,Q be Subset of ( TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds P misses Q iff ( min_dist_min (P,Q)) > 0

    proof

      let P,Q be Subset of ( TopSpaceMetr M);

      assume that

       A1: P <> {} and

       A2: P is compact and

       A3: Q <> {} and

       A4: Q is compact;

       A5:

      now

        set p = the Element of (P /\ Q);

        assume

         A6: (P /\ Q) <> {} ;

        then

         A7: p in P by XBOOLE_0:def 4;

        then

        reconsider p9 = p as Element of ( TopSpaceMetr M);

        reconsider q = p9 as Point of M by TOPMETR: 12;

        the distance of M is Reflexive by METRIC_1:def 6;

        then (the distance of M . (q,q)) = 0 by METRIC_1:def 2;

        then

         A8: ( dist (q,q)) = 0 by METRIC_1:def 1;

        p in Q by A6, XBOOLE_0:def 4;

        hence not ( min_dist_min (P,Q)) > 0 by A2, A4, A7, A8, WEIERSTR: 34;

      end;

      consider x1,x2 be Point of M such that

       A9: x1 in P & x2 in Q and

       A10: ( dist (x1,x2)) = ( min_dist_min (P,Q)) by A1, A2, A3, A4, WEIERSTR: 30;

      

       A11: the distance of M is discerning by METRIC_1:def 7;

      now

        assume not ( min_dist_min (P,Q)) > 0 ;

        then ( dist (x1,x2)) = 0 by A1, A2, A3, A4, A10, Th36;

        then (the distance of M . (x1,x2)) = 0 by METRIC_1:def 1;

        then x1 = x2 by A11, METRIC_1:def 3;

        hence (P /\ Q) <> {} by A9, XBOOLE_0:def 4;

      end;

      hence thesis by A5;

    end;

    theorem :: JGRAPH_1:39

    

     Th38: for f be FinSequence of ( TOP-REAL 2), a,c,d be Real st 1 <= ( len f) & ( X_axis f) lies_between ((( X_axis f) . 1),(( X_axis f) . ( len f))) & ( Y_axis f) lies_between (c,d) & a > 0 & (for i st 1 <= i & (i + 1) <= ( len f) holds |.((f /. i) - (f /. (i + 1))).| < a) holds ex g be FinSequence of ( TOP-REAL 2) st g is special & (g . 1) = (f . 1) & (g . ( len g)) = (f . ( len f)) & ( len g) >= ( len f) & ( X_axis g) lies_between ((( X_axis f) . 1),(( X_axis f) . ( len f))) & ( Y_axis g) lies_between (c,d) & (for j st j in ( dom g) holds ex k st k in ( dom f) & |.((g /. j) - (f /. k)).| < a) & for j st 1 <= j & (j + 1) <= ( len g) holds |.((g /. j) - (g /. (j + 1))).| < a

    proof

      let f be FinSequence of ( TOP-REAL 2), a,c,d be Real;

      assume that

       A1: 1 <= ( len f) and

       A2: ( X_axis f) lies_between ((( X_axis f) . 1),(( X_axis f) . ( len f))) and

       A3: ( Y_axis f) lies_between (c,d) and

       A4: a > 0 and

       A5: for i st 1 <= i & (i + 1) <= ( len f) holds |.((f /. i) - (f /. (i + 1))).| < a;

      

       A6: (f . ( len f)) = (f /. ( len f)) by A1, FINSEQ_4: 15;

      defpred P[ set, object] means for j st $1 = (2 * j) or $1 = ((2 * j) -' 1) holds ($1 = (2 * j) implies $2 = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]|) & ($1 = ((2 * j) -' 1) implies $2 = (f /. j));

      

       A7: for k be Nat st k in ( Seg ((2 * ( len f)) -' 1)) holds ex x be object st P[k, x]

      proof

        let k be Nat;

        assume

         A8: k in ( Seg ((2 * ( len f)) -' 1));

        then

         A9: 1 <= k by FINSEQ_1: 1;

        per cases by NAT_D: 12;

          suppose

           A10: (k mod 2) = 0 ;

          consider i be Nat such that

           A11: k = ((2 * i) + (k mod 2)) and (k mod 2) < 2 by NAT_D:def 2;

          for j st k = (2 * j) or k = ((2 * j) -' 1) holds (k = (2 * j) implies |[((f /. i) `1 ), ((f /. (i + 1)) `2 )]| = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]|) & (k = ((2 * j) -' 1) implies |[((f /. i) `1 ), ((f /. (i + 1)) `2 )]| = (f /. j))

          proof

            let j;

            assume k = (2 * j) or k = ((2 * j) -' 1);

            now

              assume

               A12: k = ((2 * j) -' 1);

              now

                ( 0 qua Nat - 1) < 0 ;

                then

                 A13: ( 0 -' 1) = 0 by XREAL_0:def 2;

                assume j = 0 ;

                hence contradiction by A8, A12, A13, FINSEQ_1: 1;

              end;

              then

               A14: j >= ( 0 qua Nat + 1) by NAT_1: 13;

              k = (((2 * (j - 1)) + (1 + 1)) - 1) by A9, A12, NAT_D: 39

              .= ((2 * (j - 1)) + 1);

              then k = ((2 * (j -' 1)) + 1) by A14, XREAL_1: 233;

              hence contradiction by A10, NAT_D:def 2;

            end;

            hence thesis by A10, A11;

          end;

          hence thesis;

        end;

          suppose

           A15: (k mod 2) = 1;

          consider i be Nat such that

           A16: k = ((2 * i) + (k mod 2)) and

           A17: (k mod 2) < 2 by NAT_D:def 2;

          for j st k = (2 * j) or k = ((2 * j) -' 1) holds (k = (2 * j) implies (f /. (i + 1)) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]|) & (k = ((2 * j) -' 1) implies (f /. (i + 1)) = (f /. j))

          proof

            let j;

            assume

             A18: k = (2 * j) or k = ((2 * j) -' 1);

            per cases by A18;

              suppose

               A19: k = ((2 * j) -' 1);

               A20:

              now

                assume k = ((2 * j) -' 1);

                

                then k = (((2 * (j - 1)) + (1 + 1)) - 1) by A9, NAT_D: 39

                .= ((2 * (j - 1)) + 1);

                hence (f /. (i + 1)) = (f /. j) by A15, A16;

              end;

              k = ((2 * j) - 1) by A9, A19, NAT_D: 39;

              hence thesis by A20;

            end;

              suppose

               A21: k = (2 * j);

              then

               A22: (2 * (j - i)) = 1 by A15, A16;

              then (j - i) >= 0 ;

              then

               A23: (j - i) = (j -' i) by XREAL_0:def 2;

              (j - i) = 0 or (j - i) > 0 by A22;

              then (j - i) >= ( 0 qua Nat + 1) by A15, A16, A21, A23, NAT_1: 13;

              then (2 * (j - i)) >= (2 * 1) by XREAL_1: 64;

              hence thesis by A16, A17, A21;

            end;

          end;

          hence thesis;

        end;

      end;

      ex p be FinSequence st ( dom p) = ( Seg ((2 * ( len f)) -' 1)) & for k be Nat st k in ( Seg ((2 * ( len f)) -' 1)) holds P[k, (p . k)] from FINSEQ_1:sch 1( A7);

      then

      consider p be FinSequence such that

       A24: ( dom p) = ( Seg ((2 * ( len f)) -' 1)) and

       A25: for k be Nat st k in ( Seg ((2 * ( len f)) -' 1)) holds for j st k = (2 * j) or k = ((2 * j) -' 1) holds (k = (2 * j) implies (p . k) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]|) & (k = ((2 * j) -' 1) implies (p . k) = (f /. j));

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

      proof

        let y be object;

        assume y in ( rng p);

        then

        consider x be object such that

         A26: x in ( dom p) and

         A27: y = (p . x) by FUNCT_1:def 3;

        reconsider i = x as Element of NAT by A26;

        x in ( Seg ( len p)) by A26, FINSEQ_1:def 3;

        then

         A28: 1 <= i by FINSEQ_1: 1;

        per cases by NAT_D: 12;

          suppose

           A29: (i mod 2) = 0 ;

          consider j be Nat such that

           A30: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          (p . i) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]| by A24, A25, A26, A29, A30;

          hence thesis by A27;

        end;

          suppose

           A31: (i mod 2) = 1;

          consider j be Nat such that

           A32: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A28, A31, A32, NAT_D: 39;

          then (p . i) = (f /. (j + 1)) by A24, A25, A26, A31, A32;

          hence thesis by A27;

        end;

      end;

      then

      reconsider g1 = p as FinSequence of ( TOP-REAL 2) by FINSEQ_1:def 4;

      

       A33: ( len p) = ((2 * ( len f)) -' 1) by A24, FINSEQ_1:def 3;

      for i be Nat st 1 <= i & (i + 1) <= ( len g1) holds ((g1 /. i) `1 ) = ((g1 /. (i + 1)) `1 ) or ((g1 /. i) `2 ) = ((g1 /. (i + 1)) `2 )

      proof

        let i be Nat;

        assume that

         A34: 1 <= i and

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

        

         A36: i < ( len g1) by A35, NAT_1: 13;

        then

         A37: (g1 . i) = (g1 /. i) by A34, FINSEQ_4: 15;

        

         A38: 1 < (i + 1) by A34, NAT_1: 13;

        then

         A39: (i + 1) in ( Seg ( len g1)) by A35, FINSEQ_1: 1;

        

         A40: i in ( Seg ((2 * ( len f)) -' 1)) by A33, A34, A36, FINSEQ_1: 1;

        

         A41: (g1 . (i + 1)) = (g1 /. (i + 1)) by A35, A38, FINSEQ_4: 15;

        per cases by NAT_D: 12;

          suppose

           A42: (i mod 2) = 0 ;

          consider j be Nat such that

           A43: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

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

          then ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A42, A43, NAT_D: 39;

          then

           A44: (g1 . (i + 1)) = (f /. (j + 1)) by A25, A33, A39, A42, A43;

          (g1 . i) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]| by A25, A40, A42, A43;

          hence thesis by A37, A41, A44, EUCLID: 52;

        end;

          suppose

           A45: (i mod 2) = 1;

          consider j be Nat such that

           A46: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          (i + 1) = (2 * (j + 1)) by A45, A46;

          then

           A47: (g1 . (i + 1)) = |[((f /. (j + 1)) `1 ), ((f /. ((j + 1) + 1)) `2 )]| by A25, A33, A39;

          ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A34, A45, A46, NAT_D: 39;

          then (g1 . i) = (f /. (j + 1)) by A25, A40, A45, A46;

          hence thesis by A37, A41, A47, EUCLID: 52;

        end;

      end;

      then

       A48: g1 is special by TOPREAL1:def 5;

      

       A49: (2 * ( len f)) >= (2 * 1) by A1, XREAL_1: 64;

      then

       A50: ((2 * ( len f)) -' 1) = ((2 * ( len f)) - 1) by XREAL_1: 233, XXREAL_0: 2;

      for i st i in ( dom ( Y_axis g1)) holds c <= (( Y_axis g1) . i) & (( Y_axis g1) . i) <= d

      proof

        let i;

        

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

        assume

         A52: i in ( dom ( Y_axis g1));

        then

         A53: i in ( Seg ( len ( Y_axis g1))) by FINSEQ_1:def 3;

        then

         A54: i in ( Seg ( len g1)) by GOBOARD1:def 2;

        i in ( Seg ( len g1)) by A53, GOBOARD1:def 2;

        then

         A55: i <= ( len g1) by FINSEQ_1: 1;

        

         A56: 1 <= i by A53, FINSEQ_1: 1;

        then

         A57: (g1 /. i) = (g1 . i) by A55, FINSEQ_4: 15;

        

         A58: (( Y_axis g1) . i) = ((g1 /. i) `2 ) by A52, GOBOARD1:def 2;

        per cases by NAT_D: 12;

          suppose

           A59: (i mod 2) = 0 ;

          consider j be Nat such that

           A60: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          (g1 . i) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]| by A25, A33, A54, A59, A60;

          then

           A61: ((g1 /. i) `2 ) = ((f /. (j + 1)) `2 ) by A57, EUCLID: 52;

          ((2 * j) + 1) <= (((2 * ( len f)) - 1) + 1) by A33, A50, A55, A59, A60, XREAL_1: 6;

          then (2 * j) < (2 * ( len f)) by NAT_1: 13;

          then ((2 * j) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

          then 1 <= (j + 1) & (j + 1) <= ( len f) by NAT_1: 11, NAT_1: 13;

          then (j + 1) in ( Seg ( len f)) by FINSEQ_1: 1;

          then

           A62: (j + 1) in ( dom ( Y_axis f)) by A51, FINSEQ_1:def 3;

          then (( Y_axis f) . (j + 1)) = ((f /. (j + 1)) `2 ) by GOBOARD1:def 2;

          hence thesis by A3, A58, A61, A62, GOBOARD4:def 2;

        end;

          suppose

           A63: (i mod 2) = 1;

          consider j be Nat such that

           A64: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A56, A63, A64, NAT_D: 39;

          then

           A65: ((g1 /. i) `2 ) = ((f /. (j + 1)) `2 ) by A25, A33, A54, A57, A63, A64;

          ((2 * j) + 1) <= (((2 * ( len f)) - 1) + 1) by A33, A50, A55, A63, A64, NAT_1: 13;

          then (2 * j) < (2 * ( len f)) by NAT_1: 13;

          then ((2 * j) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

          then 1 <= (j + 1) & (j + 1) <= ( len f) by NAT_1: 11, NAT_1: 13;

          then (j + 1) in ( Seg ( len f)) by FINSEQ_1: 1;

          then

           A66: (j + 1) in ( dom ( Y_axis f)) by A51, FINSEQ_1:def 3;

          then (( Y_axis f) . (j + 1)) = ((f /. (j + 1)) `2 ) by GOBOARD1:def 2;

          hence thesis by A3, A58, A65, A66, GOBOARD4:def 2;

        end;

      end;

      then

       A67: ( Y_axis g1) lies_between (c,d) by GOBOARD4:def 2;

      for i st i in ( dom ( X_axis g1)) holds (( X_axis f) . 1) <= (( X_axis g1) . i) & (( X_axis g1) . i) <= (( X_axis f) . ( len f))

      proof

        let i;

        

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

        assume

         A69: i in ( dom ( X_axis g1));

        then

         A70: i in ( Seg ( len ( X_axis g1))) by FINSEQ_1:def 3;

        then

         A71: i in ( Seg ( len g1)) by GOBOARD1:def 1;

        i in ( Seg ( len g1)) by A70, GOBOARD1:def 1;

        then

         A72: i <= ( len g1) by FINSEQ_1: 1;

        

         A73: 1 <= i by A70, FINSEQ_1: 1;

        then

         A74: (g1 /. i) = (g1 . i) by A72, FINSEQ_4: 15;

        

         A75: (( X_axis g1) . i) = ((g1 /. i) `1 ) by A69, GOBOARD1:def 1;

        per cases by NAT_D: 12;

          suppose

           A76: (i mod 2) = 0 ;

          consider j be Nat such that

           A77: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          (g1 . i) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]| by A25, A33, A71, A76, A77;

          then

           A78: ((g1 /. i) `1 ) = ((f /. j) `1 ) by A74, EUCLID: 52;

          ((2 * j) + 1) <= (((2 * ( len f)) - 1) + 1) by A33, A50, A72, A76, A77, XREAL_1: 6;

          then (2 * j) < (2 * ( len f)) by NAT_1: 13;

          then

           A79: ((2 * j) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

          j > 0 by A70, A76, A77, FINSEQ_1: 1;

          then j >= ( 0 qua Nat + 1) by NAT_1: 13;

          then j in ( Seg ( len f)) by A79, FINSEQ_1: 1;

          then

           A80: j in ( dom ( X_axis f)) by A68, FINSEQ_1:def 3;

          then (( X_axis f) . j) = ((f /. j) `1 ) by GOBOARD1:def 1;

          hence thesis by A2, A75, A78, A80, GOBOARD4:def 2;

        end;

          suppose

           A81: (i mod 2) = 1;

          consider j be Nat such that

           A82: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A73, A81, A82, NAT_D: 39;

          then

           A83: ((g1 /. i) `1 ) = ((f /. (j + 1)) `1 ) by A25, A33, A71, A74, A81, A82;

          ((2 * j) + 1) <= (((2 * ( len f)) - 1) + 1) by A33, A50, A72, A81, A82, NAT_1: 13;

          then (2 * j) < (2 * ( len f)) by NAT_1: 13;

          then ((2 * j) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

          then 1 <= (j + 1) & (j + 1) <= ( len f) by NAT_1: 11, NAT_1: 13;

          then (j + 1) in ( Seg ( len f)) by FINSEQ_1: 1;

          then

           A84: (j + 1) in ( dom ( X_axis f)) by A68, FINSEQ_1:def 3;

          then (( X_axis f) . (j + 1)) = ((f /. (j + 1)) `1 ) by GOBOARD1:def 1;

          hence thesis by A2, A75, A83, A84, GOBOARD4:def 2;

        end;

      end;

      then

       A85: ( X_axis g1) lies_between ((( X_axis f) . 1),(( X_axis f) . ( len f))) by GOBOARD4:def 2;

      (( len f) + ( len f)) >= (( len f) + 1) by A1, XREAL_1: 6;

      then

       A86: ((2 * ( len f)) - 1) >= ((( len f) + 1) - 1) by XREAL_1: 9;

      

       A87: ((2 * 1) -' 1) = ((1 + 1) -' 1)

      .= 1 by NAT_D: 34;

      

       A88: ((2 * ( len f)) - 1) >= ((1 + 1) - 1) by A49, XREAL_1: 9;

      then 1 in ( Seg ((2 * ( len f)) -' 1)) by A50, FINSEQ_1: 1;

      then

       A89: (p . 1) = (f /. 1) by A25, A87;

      

       A90: for i st 1 <= i & (i + 1) <= ( len g1) holds |.((g1 /. i) - (g1 /. (i + 1))).| < a

      proof

        let i;

        assume that

         A91: 1 <= i and

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

        

         A93: (g1 . (i + 1)) = (g1 /. (i + 1)) by A92, FINSEQ_4: 15, NAT_1: 11;

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

        then

         A94: i in ( Seg ( len g1)) by A91, FINSEQ_1: 1;

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

        then

         A95: (g1 . i) = (g1 /. i) by A91, FINSEQ_4: 15;

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

        then

         A96: (i + 1) in ( Seg ((2 * ( len f)) -' 1)) by A33, A92, FINSEQ_1: 1;

        per cases by NAT_D: 12;

          suppose

           A97: (i mod 2) = 0 ;

          consider j be Nat such that

           A98: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          

           A99: (g1 . i) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]| by A25, A33, A94, A97, A98;

          then

           A100: ((g1 /. i) `2 ) = ((f /. (j + 1)) `2 ) by A95, EUCLID: 52;

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

          then ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A97, A98, NAT_D: 39;

          then (g1 . (i + 1)) = (f /. (j + 1)) by A25, A96, A97, A98;

          then

           A101: ((g1 /. (i + 1)) `1 ) = ((f /. (j + 1)) `1 ) & ((g1 /. (i + 1)) `2 ) = ((f /. (j + 1)) `2 ) by A92, FINSEQ_4: 15, NAT_1: 11;

          

           A102: ((g1 /. i) - (g1 /. (i + 1))) = |[(((g1 /. i) `1 ) - ((g1 /. (i + 1)) `1 )), (((g1 /. i) `2 ) - ((g1 /. (i + 1)) `2 ))]| by EUCLID: 61

          .= |[(((f /. j) `1 ) - ((f /. (j + 1)) `1 )), 0 ]| by A95, A99, A100, A101, EUCLID: 52;

          then

           A103: (((g1 /. i) - (g1 /. (i + 1))) `1 ) = (((f /. j) `1 ) - ((f /. (j + 1)) `1 )) by EUCLID: 52;

          ((2 * j) + 1) <= (((2 * ( len f)) - 1) + 1) by A33, A50, A92, A97, A98, NAT_1: 13;

          then (2 * j) < (2 * ( len f)) by NAT_1: 13;

          then ((2 * j) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

          then

           A104: (j + 1) <= ( len f) by NAT_1: 13;

           |.((g1 /. i) - (g1 /. (i + 1))).| = ( sqrt (((((g1 /. i) - (g1 /. (i + 1))) `1 ) ^2 ) + ((((g1 /. i) - (g1 /. (i + 1))) `2 ) ^2 ))) by Th30

          .= ( sqrt (((((f /. j) `1 ) - ((f /. (j + 1)) `1 )) ^2 ) + ( 0 ^2 ))) by A102, A103, EUCLID: 52

          .= ( sqrt ((((f /. j) `1 ) - ((f /. (j + 1)) `1 )) ^2 ));

          then |.((g1 /. i) - (g1 /. (i + 1))).| = |.(((f /. j) `1 ) - ((f /. (j + 1)) `1 )).| by COMPLEX1: 72;

          then

           A105: |.((g1 /. i) - (g1 /. (i + 1))).| <= |.((f /. j) - (f /. (j + 1))).| by Th34;

          j > 0 by A91, A97, A98;

          then j >= ( 0 qua Nat + 1) by NAT_1: 13;

          then |.((f /. j) - (f /. (j + 1))).| < a by A5, A104;

          hence thesis by A105, XXREAL_0: 2;

        end;

          suppose

           A106: (i mod 2) = 1;

          consider j be Nat such that

           A107: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A91, A106, A107, NAT_D: 39;

          then

           A108: ((g1 /. i) `1 ) = ((f /. (j + 1)) `1 ) & ((g1 /. i) `2 ) = ((f /. (j + 1)) `2 ) by A25, A33, A94, A95, A106, A107;

          (i + 1) = (2 * (j + 1)) by A106, A107;

          then

           A109: (g1 /. (i + 1)) = |[((f /. (j + 1)) `1 ), ((f /. ((j + 1) + 1)) `2 )]| by A25, A96, A93;

          then

           A110: ((g1 /. (i + 1)) `1 ) = ((f /. (j + 1)) `1 ) by EUCLID: 52;

          

           A111: ((g1 /. i) - (g1 /. (i + 1))) = |[(((g1 /. i) `1 ) - ((g1 /. (i + 1)) `1 )), (((g1 /. i) `2 ) - ((g1 /. (i + 1)) `2 ))]| by EUCLID: 61

          .= |[ 0 , (((f /. (j + 1)) `2 ) - ((f /. ((j + 1) + 1)) `2 ))]| by A109, A110, A108, EUCLID: 52;

          then

           A112: (((g1 /. i) - (g1 /. (i + 1))) `1 ) = 0 by EUCLID: 52;

          ((2 * (j + 1)) + 1) <= (((2 * ( len f)) - 1) + 1) by A33, A50, A92, A106, A107, XREAL_1: 6;

          then (2 * (j + 1)) < (2 * ( len f)) by NAT_1: 13;

          then ((2 * (j + 1)) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

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

          then

           A113: |.((f /. (j + 1)) - (f /. ((j + 1) + 1))).| < a by A5, NAT_1: 11;

           |.((g1 /. i) - (g1 /. (i + 1))).| = ( sqrt (((((g1 /. i) - (g1 /. (i + 1))) `1 ) ^2 ) + ((((g1 /. i) - (g1 /. (i + 1))) `2 ) ^2 ))) by Th30

          .= ( sqrt ((((f /. (j + 1)) `2 ) - ((f /. ((j + 1) + 1)) `2 )) ^2 )) by A111, A112, EUCLID: 52;

          then |.((g1 /. i) - (g1 /. (i + 1))).| = |.(((f /. (j + 1)) `2 ) - ((f /. ((j + 1) + 1)) `2 )).| by COMPLEX1: 72;

          then |.((g1 /. i) - (g1 /. (i + 1))).| <= |.((f /. (j + 1)) - (f /. ((j + 1) + 1))).| by Th34;

          hence thesis by A113, XXREAL_0: 2;

        end;

      end;

      

       A114: for i st i in ( dom g1) holds ex k st k in ( dom f) & |.((g1 /. i) - (f /. k)).| < a

      proof

        let i;

        assume

         A115: i in ( dom g1);

        then

         A116: i in ( Seg ( len g1)) by FINSEQ_1:def 3;

        then

         A117: i <= ( len g1) by FINSEQ_1: 1;

        

         A118: 1 <= i by A116, FINSEQ_1: 1;

        then

         A119: (g1 . i) = (g1 /. i) by A117, FINSEQ_4: 15;

        per cases by NAT_D: 12;

          suppose

           A120: (i mod 2) = 0 ;

          consider j be Nat such that

           A121: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          j > 0 by A116, A120, A121, FINSEQ_1: 1;

          then

           A122: j >= ( 0 qua Nat + 1) by NAT_1: 13;

          

           A123: (g1 . i) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]| by A24, A25, A115, A120, A121;

          then

           A124: ((g1 /. i) `1 ) = ((f /. j) `1 ) by A119, EUCLID: 52;

          

           A125: ((g1 /. i) `2 ) = ((f /. (j + 1)) `2 ) by A119, A123, EUCLID: 52;

          

           A126: ((g1 /. i) - (f /. j)) = |[(((g1 /. i) `1 ) - ((f /. j) `1 )), (((g1 /. i) `2 ) - ((f /. j) `2 ))]| by EUCLID: 61

          .= |[ 0 , (((g1 /. i) `2 ) - ((f /. j) `2 ))]| by A124;

          then (((g1 /. i) - (f /. j)) `2 ) = (((g1 /. i) `2 ) - ((f /. j) `2 )) by EUCLID: 52;

          

          then |.((g1 /. i) - (f /. j)).| = ( sqrt (((((g1 /. i) - (f /. j)) `1 ) ^2 ) + ((((g1 /. i) `2 ) - ((f /. j) `2 )) ^2 ))) by Th30

          .= ( sqrt (( 0 ^2 ) + ((((f /. (j + 1)) `2 ) - ((f /. j) `2 )) ^2 ))) by A125, A126, EUCLID: 52

          .= ( sqrt ((((f /. (j + 1)) `2 ) - ((f /. j) `2 )) ^2 ));

          

          then |.((g1 /. i) - (f /. j)).| = |.(((f /. (j + 1)) `2 ) - ((f /. j) `2 )).| by COMPLEX1: 72

          .= |.(((f /. j) `2 ) - ((f /. (j + 1)) `2 )).| by UNIFORM1: 11;

          then

           A127: |.((g1 /. i) - (f /. j)).| <= |.((f /. j) - (f /. (j + 1))).| by Th34;

          ((2 * j) + 1) <= (((2 * ( len f)) - 1) + 1) by A33, A50, A117, A120, A121, XREAL_1: 6;

          then (2 * j) < (2 * ( len f)) by NAT_1: 13;

          then

           A128: ((2 * j) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

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

          then |.((f /. j) - (f /. (j + 1))).| < a by A5, A122;

          then

           A129: |.((g1 /. i) - (f /. j)).| < a by A127, XXREAL_0: 2;

          j in ( dom f) by A122, A128, FINSEQ_3: 25;

          hence thesis by A129;

        end;

          suppose

           A130: (i mod 2) = 1;

          consider j be Nat such that

           A131: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A118, A130, A131, NAT_D: 39;

          then (g1 . i) = (f /. (j + 1)) by A24, A25, A115, A130, A131;

          

          then

           A132: |.((g1 /. i) - (f /. (j + 1))).| = |.( 0. ( TOP-REAL 2)).| by A119, RLVECT_1: 5

          .= 0 by TOPRNS_1: 23;

          (((2 * j) + 1) + 1) <= (((2 * ( len f)) - 1) + 1) by A33, A50, A117, A130, A131, XREAL_1: 6;

          then ((2 * j) + 1) < (2 * ( len f)) by NAT_1: 13;

          then (2 * j) < (2 * ( len f)) by NAT_1: 13;

          then ((2 * j) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

          then

           A133: (j + 1) <= ( len f) by NAT_1: 13;

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

          then (j + 1) in ( dom f) by A133, FINSEQ_3: 25;

          hence thesis by A4, A132;

        end;

      end;

      ((2 * ( len f)) -' 1) in ( Seg ((2 * ( len f)) -' 1)) by A50, A88, FINSEQ_1: 1;

      then (g1 . ( len g1)) = (f . ( len f)) by A25, A33, A6;

      hence thesis by A1, A33, A48, A50, A89, A86, A85, A67, A114, A90, FINSEQ_4: 15;

    end;

    theorem :: JGRAPH_1:40

    

     Th39: for f be FinSequence of ( TOP-REAL 2), a,c,d be Real st 1 <= ( len f) & ( Y_axis f) lies_between ((( Y_axis f) . 1),(( Y_axis f) . ( len f))) & ( X_axis f) lies_between (c,d) & a > 0 & (for i st 1 <= i & (i + 1) <= ( len f) holds |.((f /. i) - (f /. (i + 1))).| < a) holds ex g be FinSequence of ( TOP-REAL 2) st g is special & (g . 1) = (f . 1) & (g . ( len g)) = (f . ( len f)) & ( len g) >= ( len f) & ( Y_axis g) lies_between ((( Y_axis f) . 1),(( Y_axis f) . ( len f))) & ( X_axis g) lies_between (c,d) & (for j st j in ( dom g) holds ex k st k in ( dom f) & |.((g /. j) - (f /. k)).| < a) & for j st 1 <= j & (j + 1) <= ( len g) holds |.((g /. j) - (g /. (j + 1))).| < a

    proof

      

       A1: ((2 * 1) -' 1) = ((1 + 1) -' 1)

      .= 1 by NAT_D: 34;

      let f be FinSequence of ( TOP-REAL 2), a,c,d be Real;

      assume that

       A2: 1 <= ( len f) and

       A3: ( Y_axis f) lies_between ((( Y_axis f) . 1),(( Y_axis f) . ( len f))) and

       A4: ( X_axis f) lies_between (c,d) and

       A5: a > 0 and

       A6: for i st 1 <= i & (i + 1) <= ( len f) holds |.((f /. i) - (f /. (i + 1))).| < a;

      (( len f) + ( len f)) >= (( len f) + 1) by A2, XREAL_1: 6;

      then

       A7: ((2 * ( len f)) - 1) >= ((( len f) + 1) - 1) by XREAL_1: 9;

      defpred P[ set, object] means for j st $1 = (2 * j) or $1 = ((2 * j) -' 1) holds ($1 = (2 * j) implies $2 = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]|) & ($1 = ((2 * j) -' 1) implies $2 = (f /. j));

      

       A8: for k be Nat st k in ( Seg ((2 * ( len f)) -' 1)) holds ex x be object st P[k, x]

      proof

        let k be Nat;

        assume

         A9: k in ( Seg ((2 * ( len f)) -' 1));

        then

         A10: 1 <= k by FINSEQ_1: 1;

        per cases by NAT_D: 12;

          suppose

           A11: (k mod 2) = 0 ;

          consider i be Nat such that

           A12: k = ((2 * i) + (k mod 2)) and (k mod 2) < 2 by NAT_D:def 2;

          for j st k = (2 * j) or k = ((2 * j) -' 1) holds (k = (2 * j) implies |[((f /. i) `1 ), ((f /. (i + 1)) `2 )]| = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]|) & (k = ((2 * j) -' 1) implies |[((f /. i) `1 ), ((f /. (i + 1)) `2 )]| = (f /. j))

          proof

            let j;

            assume k = (2 * j) or k = ((2 * j) -' 1);

            now

              assume

               A13: k = ((2 * j) -' 1);

              now

                ( 0 qua Nat - 1) < 0 ;

                then

                 A14: ( 0 -' 1) = 0 by XREAL_0:def 2;

                assume j = 0 ;

                hence contradiction by A9, A13, A14, FINSEQ_1: 1;

              end;

              then

               A15: j >= ( 0 qua Nat + 1) by NAT_1: 13;

              k = (((2 * (j - 1)) + (1 + 1)) - 1) by A10, A13, NAT_D: 39

              .= ((2 * (j - 1)) + 1);

              then k = ((2 * (j -' 1)) + 1) by A15, XREAL_1: 233;

              hence contradiction by A11, NAT_D:def 2;

            end;

            hence thesis by A11, A12;

          end;

          hence thesis;

        end;

          suppose

           A16: (k mod 2) = 1;

          consider i be Nat such that

           A17: k = ((2 * i) + (k mod 2)) and

           A18: (k mod 2) < 2 by NAT_D:def 2;

          for j st k = (2 * j) or k = ((2 * j) -' 1) holds (k = (2 * j) implies (f /. (i + 1)) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]|) & (k = ((2 * j) -' 1) implies (f /. (i + 1)) = (f /. j))

          proof

            let j;

            assume

             A19: k = (2 * j) or k = ((2 * j) -' 1);

            per cases by A19;

              suppose

               A20: k = ((2 * j) -' 1);

               A21:

              now

                assume k = ((2 * j) -' 1);

                

                then k = (((2 * (j - 1)) + (1 + 1)) - 1) by A10, NAT_D: 39

                .= ((2 * (j - 1)) + 1);

                hence (f /. (i + 1)) = (f /. j) by A16, A17;

              end;

              k = ((2 * j) - 1) by A10, A20, NAT_D: 39;

              hence thesis by A21;

            end;

              suppose

               A22: k = (2 * j);

              then

               A23: (2 * (j - i)) = 1 by A16, A17;

              then (j - i) >= 0 ;

              then

               A24: (j - i) = (j -' i) by XREAL_0:def 2;

              (j - i) = 0 or (j - i) > 0 by A23;

              then (j - i) >= ( 0 qua Nat + 1) by A16, A17, A22, A24, NAT_1: 13;

              then (2 * (j - i)) >= (2 * 1) by XREAL_1: 64;

              hence thesis by A17, A18, A22;

            end;

          end;

          hence thesis;

        end;

      end;

      ex p be FinSequence st ( dom p) = ( Seg ((2 * ( len f)) -' 1)) & for k be Nat st k in ( Seg ((2 * ( len f)) -' 1)) holds P[k, (p . k)] from FINSEQ_1:sch 1( A8);

      then

      consider p be FinSequence such that

       A25: ( dom p) = ( Seg ((2 * ( len f)) -' 1)) and

       A26: for k be Nat st k in ( Seg ((2 * ( len f)) -' 1)) holds for j st k = (2 * j) or k = ((2 * j) -' 1) holds (k = (2 * j) implies (p . k) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]|) & (k = ((2 * j) -' 1) implies (p . k) = (f /. j));

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

      proof

        let y be object;

        assume y in ( rng p);

        then

        consider x be object such that

         A27: x in ( dom p) and

         A28: y = (p . x) by FUNCT_1:def 3;

        reconsider i = x as Element of NAT by A27;

        x in ( Seg ( len p)) by A27, FINSEQ_1:def 3;

        then

         A29: 1 <= i by FINSEQ_1: 1;

        per cases by NAT_D: 12;

          suppose

           A30: (i mod 2) = 0 ;

          consider j be Nat such that

           A31: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          (p . i) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]| by A25, A26, A27, A30, A31;

          hence thesis by A28;

        end;

          suppose

           A32: (i mod 2) = 1;

          consider j be Nat such that

           A33: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          ((2 * (j + 1)) - 1) = ((2 * (j + 1)) -' 1) by A29, A32, A33, NAT_D: 39;

          then (p . i) = (f /. (j + 1)) by A25, A26, A27, A32, A33;

          hence thesis by A28;

        end;

      end;

      then

      reconsider g1 = p as FinSequence of ( TOP-REAL 2) by FINSEQ_1:def 4;

      

       A34: ( len p) = ((2 * ( len f)) -' 1) by A25, FINSEQ_1:def 3;

      for i be Nat st 1 <= i & (i + 1) <= ( len g1) holds ((g1 /. i) `1 ) = ((g1 /. (i + 1)) `1 ) or ((g1 /. i) `2 ) = ((g1 /. (i + 1)) `2 )

      proof

        let i be Nat;

        assume that

         A35: 1 <= i and

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

        1 < (i + 1) by A35, NAT_1: 13;

        then

         A37: (i + 1) in ( Seg ( len g1)) & (g1 /. (i + 1)) = (g1 . (i + 1)) by A36, FINSEQ_1: 1, FINSEQ_4: 15;

        i < ( len g1) by A36, NAT_1: 13;

        then

         A38: i in ( Seg ((2 * ( len f)) -' 1)) & (g1 . i) = (g1 /. i) by A34, A35, FINSEQ_1: 1, FINSEQ_4: 15;

        per cases by NAT_D: 12;

          suppose

           A39: (i mod 2) = 0 ;

          consider j be Nat such that

           A40: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

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

          then ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A39, A40, NAT_D: 39;

          then

           A41: (g1 /. (i + 1)) = (f /. (j + 1)) by A26, A34, A37, A39, A40;

          (g1 /. i) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]| by A26, A38, A39, A40;

          hence thesis by A41, EUCLID: 52;

        end;

          suppose

           A42: (i mod 2) = 1;

          consider j be Nat such that

           A43: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          (i + 1) = (2 * (j + 1)) by A42, A43;

          then

           A44: (g1 /. (i + 1)) = |[((f /. (j + 1)) `1 ), ((f /. ((j + 1) + 1)) `2 )]| by A26, A34, A37;

          ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A35, A42, A43, NAT_D: 39;

          then (g1 /. i) = (f /. (j + 1)) by A26, A38, A42, A43;

          hence thesis by A44, EUCLID: 52;

        end;

      end;

      then

       A45: g1 is special by TOPREAL1:def 5;

      

       A46: (2 * ( len f)) >= (2 * 1) by A2, XREAL_1: 64;

      then

       A47: ((2 * ( len f)) -' 1) = ((2 * ( len f)) - 1) by XREAL_1: 233, XXREAL_0: 2;

      for i st i in ( dom ( Y_axis g1)) holds (( Y_axis f) . 1) <= (( Y_axis g1) . i) & (( Y_axis g1) . i) <= (( Y_axis f) . ( len f))

      proof

        let i;

        

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

        assume

         A49: i in ( dom ( Y_axis g1));

        then

         A50: i in ( Seg ( len ( Y_axis g1))) by FINSEQ_1:def 3;

        then

         A51: i in ( Seg ( len g1)) by GOBOARD1:def 2;

        i in ( Seg ( len g1)) by A50, GOBOARD1:def 2;

        then

         A52: i <= ( len g1) by FINSEQ_1: 1;

        

         A53: 1 <= i by A50, FINSEQ_1: 1;

        then

         A54: (g1 /. i) = (g1 . i) by A52, FINSEQ_4: 15;

        

         A55: (( Y_axis g1) . i) = ((g1 /. i) `2 ) by A49, GOBOARD1:def 2;

        per cases by NAT_D: 12;

          suppose

           A56: (i mod 2) = 0 ;

          consider j be Nat such that

           A57: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          (g1 /. i) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]| by A26, A34, A51, A54, A56, A57;

          then

           A58: ((g1 /. i) `2 ) = ((f /. (j + 1)) `2 ) by EUCLID: 52;

          ((2 * j) + 1) <= (((2 * ( len f)) - 1) + 1) by A34, A47, A52, A56, A57, XREAL_1: 6;

          then (2 * j) < (2 * ( len f)) by NAT_1: 13;

          then ((2 * j) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

          then 1 <= (j + 1) & (j + 1) <= ( len f) by NAT_1: 11, NAT_1: 13;

          then (j + 1) in ( Seg ( len f)) by FINSEQ_1: 1;

          then

           A59: (j + 1) in ( dom ( Y_axis f)) by A48, FINSEQ_1:def 3;

          then (( Y_axis f) . (j + 1)) = ((f /. (j + 1)) `2 ) by GOBOARD1:def 2;

          hence thesis by A3, A55, A58, A59, GOBOARD4:def 2;

        end;

          suppose

           A60: (i mod 2) = 1;

          consider j be Nat such that

           A61: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A53, A60, A61, NAT_D: 39;

          then

           A62: ((g1 /. i) `2 ) = ((f /. (j + 1)) `2 ) by A26, A34, A51, A54, A60, A61;

          ((2 * j) + 1) <= (((2 * ( len f)) - 1) + 1) by A34, A47, A52, A60, A61, NAT_1: 13;

          then (2 * j) < (2 * ( len f)) by NAT_1: 13;

          then ((2 * j) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

          then 1 <= (j + 1) & (j + 1) <= ( len f) by NAT_1: 11, NAT_1: 13;

          then (j + 1) in ( Seg ( len f)) by FINSEQ_1: 1;

          then

           A63: (j + 1) in ( dom ( Y_axis f)) by A48, FINSEQ_1:def 3;

          then (( Y_axis f) . (j + 1)) = ((f /. (j + 1)) `2 ) by GOBOARD1:def 2;

          hence thesis by A3, A55, A62, A63, GOBOARD4:def 2;

        end;

      end;

      then

       A64: ( Y_axis g1) lies_between ((( Y_axis f) . 1),(( Y_axis f) . ( len f))) by GOBOARD4:def 2;

      

       A65: ((2 * ( len f)) - 1) >= ((1 + 1) - 1) by A46, XREAL_1: 9;

      then 1 in ( Seg ((2 * ( len f)) -' 1)) by A47, FINSEQ_1: 1;

      then (p . 1) = (f /. 1) by A26, A1;

      then

       A66: (g1 . 1) = (f . 1) by A2, FINSEQ_4: 15;

      

       A67: for i st 1 <= i & (i + 1) <= ( len g1) holds |.((g1 /. i) - (g1 /. (i + 1))).| < a

      proof

        let i;

        assume that

         A68: 1 <= i and

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

        

         A70: (g1 . (i + 1)) = (g1 /. (i + 1)) by A69, FINSEQ_4: 15, NAT_1: 11;

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

        then

         A71: i in ( Seg ( len g1)) by A68, FINSEQ_1: 1;

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

        then

         A72: (i + 1) in ( Seg ((2 * ( len f)) -' 1)) by A34, A69, FINSEQ_1: 1;

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

        then

         A73: (g1 . i) = (g1 /. i) by A68, FINSEQ_4: 15;

        per cases by NAT_D: 12;

          suppose

           A74: (i mod 2) = 0 ;

          consider j be Nat such that

           A75: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          

           A76: (g1 /. i) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]| by A26, A34, A71, A73, A74, A75;

          then

           A77: ((g1 /. i) `2 ) = ((f /. (j + 1)) `2 ) by EUCLID: 52;

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

          then ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A74, A75, NAT_D: 39;

          then

           A78: (g1 /. (i + 1)) = (f /. (j + 1)) by A26, A72, A70, A74, A75;

          ((g1 /. i) - (g1 /. (i + 1))) = |[(((g1 /. i) `1 ) - ((g1 /. (i + 1)) `1 )), (((g1 /. i) `2 ) - ((g1 /. (i + 1)) `2 ))]| by EUCLID: 61

          .= |[(((f /. j) `1 ) - ((f /. (j + 1)) `1 )), 0 ]| by A76, A78, A77, EUCLID: 52;

          then (((g1 /. i) - (g1 /. (i + 1))) `1 ) = (((f /. j) `1 ) - ((f /. (j + 1)) `1 )) & (((g1 /. i) - (g1 /. (i + 1))) `2 ) = 0 by EUCLID: 52;

          

          then |.((g1 /. i) - (g1 /. (i + 1))).| = ( sqrt (((((f /. j) `1 ) - ((f /. (j + 1)) `1 )) ^2 ) + ( 0 ^2 ))) by Th30

          .= ( sqrt ((((f /. j) `1 ) - ((f /. (j + 1)) `1 )) ^2 ));

          then |.((g1 /. i) - (g1 /. (i + 1))).| = |.(((f /. j) `1 ) - ((f /. (j + 1)) `1 )).| by COMPLEX1: 72;

          then

           A79: |.((g1 /. i) - (g1 /. (i + 1))).| <= |.((f /. j) - (f /. (j + 1))).| by Th34;

          ((2 * j) + 1) <= (((2 * ( len f)) - 1) + 1) by A34, A47, A69, A74, A75, NAT_1: 13;

          then (2 * j) < (2 * ( len f)) by NAT_1: 13;

          then ((2 * j) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

          then

           A80: (j + 1) <= ( len f) by NAT_1: 13;

          j > 0 by A68, A74, A75;

          then j >= ( 0 qua Nat + 1) by NAT_1: 13;

          then |.((f /. j) - (f /. (j + 1))).| < a by A6, A80;

          hence thesis by A79, XXREAL_0: 2;

        end;

          suppose

           A81: (i mod 2) = 1;

          consider j be Nat such that

           A82: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A68, A81, A82, NAT_D: 39;

          then

           A83: (g1 /. i) = (f /. (j + 1)) by A26, A34, A71, A73, A81, A82;

          (i + 1) = (2 * (j + 1)) by A81, A82;

          then

           A84: (g1 /. (i + 1)) = |[((f /. (j + 1)) `1 ), ((f /. ((j + 1) + 1)) `2 )]| by A26, A72, A70;

          then

           A85: ((g1 /. (i + 1)) `1 ) = ((f /. (j + 1)) `1 ) by EUCLID: 52;

          ((g1 /. i) - (g1 /. (i + 1))) = |[(((g1 /. i) `1 ) - ((g1 /. (i + 1)) `1 )), (((g1 /. i) `2 ) - ((g1 /. (i + 1)) `2 ))]| by EUCLID: 61

          .= |[ 0 , (((f /. (j + 1)) `2 ) - ((f /. ((j + 1) + 1)) `2 ))]| by A83, A84, A85, EUCLID: 52;

          then (((g1 /. i) - (g1 /. (i + 1))) `1 ) = 0 & (((g1 /. i) - (g1 /. (i + 1))) `2 ) = (((f /. (j + 1)) `2 ) - ((f /. ((j + 1) + 1)) `2 )) by EUCLID: 52;

          

          then |.((g1 /. i) - (g1 /. (i + 1))).| = ( sqrt (( 0 ^2 ) + ((((f /. (j + 1)) `2 ) - ((f /. ((j + 1) + 1)) `2 )) ^2 ))) by Th30

          .= ( sqrt ((((f /. (j + 1)) `2 ) - ((f /. ((j + 1) + 1)) `2 )) ^2 ));

          then |.((g1 /. i) - (g1 /. (i + 1))).| = |.(((f /. (j + 1)) `2 ) - ((f /. ((j + 1) + 1)) `2 )).| by COMPLEX1: 72;

          then

           A86: |.((g1 /. i) - (g1 /. (i + 1))).| <= |.((f /. (j + 1)) - (f /. ((j + 1) + 1))).| by Th34;

          ((2 * (j + 1)) + 1) <= (((2 * ( len f)) - 1) + 1) by A34, A47, A69, A81, A82, XREAL_1: 6;

          then (2 * (j + 1)) < (2 * ( len f)) by NAT_1: 13;

          then ((2 * (j + 1)) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

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

          then |.((f /. (j + 1)) - (f /. ((j + 1) + 1))).| < a by A6, NAT_1: 11;

          hence thesis by A86, XXREAL_0: 2;

        end;

      end;

      

       A87: for i st i in ( dom g1) holds ex k st k in ( dom f) & |.((g1 /. i) - (f /. k)).| < a

      proof

        let i;

        assume

         A88: i in ( dom g1);

        then

         A89: i <= ( len g1) by FINSEQ_3: 25;

        

         A90: 1 <= i by A88, FINSEQ_3: 25;

        then

         A91: (g1 . i) = (g1 /. i) by A89, FINSEQ_4: 15;

        per cases by NAT_D: 12;

          suppose

           A92: (i mod 2) = 0 ;

          consider j be Nat such that

           A93: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          j > 0 by A88, A92, A93, FINSEQ_3: 25;

          then

           A94: j >= ( 0 qua Nat + 1) by NAT_1: 13;

          

           A95: (g1 /. i) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]| by A25, A26, A88, A91, A92, A93;

          then

           A96: ((g1 /. i) `1 ) = ((f /. j) `1 ) by EUCLID: 52;

          

           A97: ((g1 /. i) - (f /. j)) = |[(((g1 /. i) `1 ) - ((f /. j) `1 )), (((g1 /. i) `2 ) - ((f /. j) `2 ))]| by EUCLID: 61

          .= |[ 0 , (((g1 /. i) `2 ) - ((f /. j) `2 ))]| by A96;

          then

           A98: (((g1 /. i) - (f /. j)) `1 ) = 0 by EUCLID: 52;

          (((g1 /. i) - (f /. j)) `2 ) = (((g1 /. i) `2 ) - ((f /. j) `2 )) by A97, EUCLID: 52;

          

          then |.((g1 /. i) - (f /. j)).| = ( sqrt (((((g1 /. i) - (f /. j)) `1 ) ^2 ) + ((((g1 /. i) `2 ) - ((f /. j) `2 )) ^2 ))) by Th30

          .= ( sqrt ((((f /. (j + 1)) `2 ) - ((f /. j) `2 )) ^2 )) by A95, A98, EUCLID: 52;

          

          then |.((g1 /. i) - (f /. j)).| = |.(((f /. (j + 1)) `2 ) - ((f /. j) `2 )).| by COMPLEX1: 72

          .= |.(((f /. j) `2 ) - ((f /. (j + 1)) `2 )).| by UNIFORM1: 11;

          then

           A99: |.((g1 /. i) - (f /. j)).| <= |.((f /. j) - (f /. (j + 1))).| by Th34;

          ((2 * j) + 1) <= (((2 * ( len f)) - 1) + 1) by A34, A47, A89, A92, A93, XREAL_1: 6;

          then (2 * j) < (2 * ( len f)) by NAT_1: 13;

          then

           A100: ((2 * j) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

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

          then |.((f /. j) - (f /. (j + 1))).| < a by A6, A94;

          then

           A101: |.((g1 /. i) - (f /. j)).| < a by A99, XXREAL_0: 2;

          j in ( dom f) by A94, A100, FINSEQ_3: 25;

          hence thesis by A101;

        end;

          suppose

           A102: (i mod 2) = 1;

          consider j be Nat such that

           A103: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A90, A102, A103, NAT_D: 39;

          then (g1 /. i) = (f /. (j + 1)) by A25, A26, A88, A91, A102, A103;

          

          then

           A104: |.((g1 /. i) - (f /. (j + 1))).| = |.( 0. ( TOP-REAL 2)).| by RLVECT_1: 5

          .= 0 by TOPRNS_1: 23;

          (((2 * j) + 1) + 1) <= (((2 * ( len f)) - 1) + 1) by A34, A47, A89, A102, A103, XREAL_1: 6;

          then ((2 * j) + 1) < (2 * ( len f)) by NAT_1: 13;

          then (2 * j) < (2 * ( len f)) by NAT_1: 13;

          then ((2 * j) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

          then

           A105: (j + 1) <= ( len f) by NAT_1: 13;

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

          then (j + 1) in ( dom f) by A105, FINSEQ_3: 25;

          hence thesis by A5, A104;

        end;

      end;

      for i st i in ( dom ( X_axis g1)) holds c <= (( X_axis g1) . i) & (( X_axis g1) . i) <= d

      proof

        let i;

        

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

        assume

         A107: i in ( dom ( X_axis g1));

        then

         A108: i in ( Seg ( len ( X_axis g1))) by FINSEQ_1:def 3;

        then

         A109: i in ( Seg ( len g1)) by GOBOARD1:def 1;

        then

         A110: i <= ( len g1) by FINSEQ_1: 1;

        

         A111: 1 <= i by A108, FINSEQ_1: 1;

        then

         A112: (g1 /. i) = (g1 . i) by A110, FINSEQ_4: 15;

        

         A113: (( X_axis g1) . i) = ((g1 /. i) `1 ) by A107, GOBOARD1:def 1;

        per cases by NAT_D: 12;

          suppose

           A114: (i mod 2) = 0 ;

          consider j be Nat such that

           A115: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          (g1 /. i) = |[((f /. j) `1 ), ((f /. (j + 1)) `2 )]| by A26, A34, A109, A112, A114, A115;

          then

           A116: ((g1 /. i) `1 ) = ((f /. j) `1 ) by EUCLID: 52;

          ((2 * j) + 1) <= (((2 * ( len f)) - 1) + 1) by A34, A47, A110, A114, A115, XREAL_1: 6;

          then (2 * j) < (2 * ( len f)) by NAT_1: 13;

          then

           A117: ((2 * j) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

          j > 0 by A108, A114, A115, FINSEQ_1: 1;

          then j >= ( 0 qua Nat + 1) by NAT_1: 13;

          then j in ( Seg ( len f)) by A117, FINSEQ_1: 1;

          then

           A118: j in ( dom ( X_axis f)) by A106, FINSEQ_1:def 3;

          then (( X_axis f) . j) = ((f /. j) `1 ) by GOBOARD1:def 1;

          hence thesis by A4, A113, A116, A118, GOBOARD4:def 2;

        end;

          suppose

           A119: (i mod 2) = 1;

          consider j be Nat such that

           A120: i = ((2 * j) + (i mod 2)) and (i mod 2) < 2 by NAT_D:def 2;

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

          ((2 * (j + 1)) -' 1) = ((2 * (j + 1)) - 1) by A111, A119, A120, NAT_D: 39;

          then

           A121: ((g1 /. i) `1 ) = ((f /. (j + 1)) `1 ) by A26, A34, A109, A112, A119, A120;

          ((2 * j) + 1) <= (((2 * ( len f)) - 1) + 1) by A34, A47, A110, A119, A120, NAT_1: 13;

          then (2 * j) < (2 * ( len f)) by NAT_1: 13;

          then ((2 * j) / 2) < ((2 * ( len f)) / 2) by XREAL_1: 74;

          then 1 <= (j + 1) & (j + 1) <= ( len f) by NAT_1: 11, NAT_1: 13;

          then (j + 1) in ( Seg ( len f)) by FINSEQ_1: 1;

          then

           A122: (j + 1) in ( dom ( X_axis f)) by A106, FINSEQ_1:def 3;

          then (( X_axis f) . (j + 1)) = ((f /. (j + 1)) `1 ) by GOBOARD1:def 1;

          hence thesis by A4, A113, A121, A122, GOBOARD4:def 2;

        end;

      end;

      then

       A123: ( X_axis g1) lies_between (c,d) by GOBOARD4:def 2;

      ((2 * ( len f)) -' 1) in ( Seg ((2 * ( len f)) -' 1)) by A47, A65, FINSEQ_1: 1;

      then (p . ((2 * ( len f)) -' 1)) = (f /. ( len f)) by A26;

      hence thesis by A2, A34, A45, A47, A66, A7, A64, A123, A87, A67, FINSEQ_4: 15;

    end;

    theorem :: JGRAPH_1:41

    

     Th40: for f be FinSequence of ( TOP-REAL 2) st 1 <= ( len f) holds ( len ( X_axis f)) = ( len f) & (( X_axis f) . 1) = ((f /. 1) `1 ) & (( X_axis f) . ( len f)) = ((f /. ( len f)) `1 )

    proof

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

      

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

      assume

       A2: 1 <= ( len f);

      then ( len f) in ( Seg ( len f)) by FINSEQ_1: 1;

      then

       A3: ( len f) in ( dom ( X_axis f)) by A1, FINSEQ_1:def 3;

      1 in ( Seg ( len f)) by A2, FINSEQ_1: 1;

      then 1 in ( dom ( X_axis f)) by A1, FINSEQ_1:def 3;

      hence thesis by A3, GOBOARD1:def 1;

    end;

    theorem :: JGRAPH_1:42

    

     Th41: for f be FinSequence of ( TOP-REAL 2) st 1 <= ( len f) holds ( len ( Y_axis f)) = ( len f) & (( Y_axis f) . 1) = ((f /. 1) `2 ) & (( Y_axis f) . ( len f)) = ((f /. ( len f)) `2 )

    proof

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

      

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

      assume

       A2: 1 <= ( len f);

      then ( len f) in ( Seg ( len f)) by FINSEQ_1: 1;

      then

       A3: ( len f) in ( dom ( Y_axis f)) by A1, FINSEQ_1:def 3;

      1 in ( Seg ( len f)) by A2, FINSEQ_1: 1;

      then 1 in ( dom ( Y_axis f)) by A1, FINSEQ_1:def 3;

      hence thesis by A3, GOBOARD1:def 2;

    end;

    theorem :: JGRAPH_1:43

    

     Th42: for f be FinSequence of ( TOP-REAL 2) st i in ( dom f) holds (( X_axis f) . i) = ((f /. i) `1 ) & (( Y_axis f) . i) = ((f /. i) `2 )

    proof

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

      assume

       A1: i in ( dom f);

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

      then i in ( dom ( X_axis f)) by A1, FINSEQ_3: 29;

      hence (( X_axis f) . i) = ((f /. i) `1 ) by GOBOARD1:def 1;

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

      then i in ( dom ( Y_axis f)) by A1, FINSEQ_3: 29;

      hence thesis by GOBOARD1:def 2;

    end;

    theorem :: JGRAPH_1:44

    

     Th43: for P,Q be non empty Subset of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2) st P is_an_arc_of (p1,p2) & Q is_an_arc_of (q1,q2) & (for p be Point of ( TOP-REAL 2) st p in P holds (p1 `1 ) <= (p `1 ) & (p `1 ) <= (p2 `1 )) & (for p be Point of ( TOP-REAL 2) st p in Q holds (p1 `1 ) <= (p `1 ) & (p `1 ) <= (p2 `1 )) & (for p be Point of ( TOP-REAL 2) st p in P holds (q1 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 )) & (for p be Point of ( TOP-REAL 2) st p in Q holds (q1 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 )) holds P meets Q

    proof

      let P,Q be non empty Subset of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2);

      assume that

       A1: P is_an_arc_of (p1,p2) and

       A2: Q is_an_arc_of (q1,q2) and

       A3: for p be Point of ( TOP-REAL 2) st p in P holds (p1 `1 ) <= (p `1 ) & (p `1 ) <= (p2 `1 ) and

       A4: for p be Point of ( TOP-REAL 2) st p in Q holds (p1 `1 ) <= (p `1 ) & (p `1 ) <= (p2 `1 ) and

       A5: for p be Point of ( TOP-REAL 2) st p in P holds (q1 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 ) and

       A6: for p be Point of ( TOP-REAL 2) st p in Q holds (q1 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 );

      consider g be Function of I[01] , (( TOP-REAL 2) | Q) such that

       A7: g is being_homeomorphism and

       A8: (g . 0 ) = q1 and

       A9: (g . 1) = q2 by A2, TOPREAL1:def 1;

      

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

      then

      reconsider P9 = P, Q9 = Q as Subset of ( TopSpaceMetr ( Euclid 2));

      P is compact by A1, JORDAN5A: 1;

      then

       A11: P9 is compact by A10, COMPTS_1: 23;

      Q is compact by A2, JORDAN5A: 1;

      then

       A12: Q9 is compact by A10, COMPTS_1: 23;

      set e = (( min_dist_min (P9,Q9)) / 5);

      consider f be Function of I[01] , (( TOP-REAL 2) | P) such that

       A13: f is being_homeomorphism and

       A14: (f . 0 ) = p1 and

       A15: (f . 1) = p2 by A1, TOPREAL1:def 1;

      consider f1 be Function of I[01] , ( TOP-REAL 2) such that

       A16: f = f1 and

       A17: f1 is continuous and f1 is one-to-one by A13, JORDAN7: 15;

      consider g1 be Function of I[01] , ( TOP-REAL 2) such that

       A18: g = g1 and

       A19: g1 is continuous and g1 is one-to-one by A7, JORDAN7: 15;

      assume (P /\ Q) = {} ;

      then P misses Q;

      then

       A20: ( min_dist_min (P9,Q9)) > 0 by A11, A12, Th37;

      then

       A21: e > ( 0 / 5) by XREAL_1: 74;

      then

      consider hb be FinSequence of REAL such that

       A22: (hb . 1) = 0 and

       A23: (hb . ( len hb)) = 1 and

       A24: 5 <= ( len hb) and

       A25: ( rng hb) c= the carrier of I[01] and

       A26: hb is increasing and

       A27: for i be Nat, R be Subset of I[01] , W be Subset of ( Euclid 2) st 1 <= i & i < ( len hb) & R = [.(hb /. i), (hb /. (i + 1)).] & W = (g1 .: R) holds ( diameter W) < e by A19, UNIFORM1: 13;

      consider h be FinSequence of REAL such that

       A28: (h . 1) = 0 and

       A29: (h . ( len h)) = 1 and

       A30: 5 <= ( len h) and

       A31: ( rng h) c= the carrier of I[01] and

       A32: h is increasing and

       A33: for i be Nat, R be Subset of I[01] , W be Subset of ( Euclid 2) st 1 <= i & i < ( len h) & R = [.(h /. i), (h /. (i + 1)).] & W = (f1 .: R) holds ( diameter W) < e by A17, A21, UNIFORM1: 13;

      deffunc F( Nat) = (f1 . (h . $1));

      ex h19 be FinSequence st ( len h19) = ( len h) & for i be Nat st i in ( dom h19) holds (h19 . i) = F(i) from FINSEQ_1:sch 2;

      then

      consider h19 be FinSequence such that

       A34: ( len h19) = ( len h) and

       A35: for i be Nat st i in ( dom h19) holds (h19 . i) = (f1 . (h . i));

      

       A36: ( dom g1) = ( [#] I[01] ) by A7, A18, TOPS_2:def 5

      .= the carrier of I[01] ;

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

      proof

        let y be object;

        assume y in ( rng h19);

        then

        consider x be object such that

         A37: x in ( dom h19) and

         A38: y = (h19 . x) by FUNCT_1:def 3;

        reconsider i = x as Element of NAT by A37;

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

        then i in ( dom h) by A34, A37, FINSEQ_1:def 3;

        then

         A39: (h . i) in ( rng h) by FUNCT_1:def 3;

        

         A40: ( dom f1) = ( [#] I[01] ) by A13, A16, TOPS_2:def 5

        .= the carrier of I[01] ;

        

         A41: ( rng f) = ( [#] (( TOP-REAL 2) | P)) by A13, TOPS_2:def 5

        .= P by PRE_TOPC:def 5;

        (h19 . i) = (f1 . (h . i)) by A35, A37;

        then (h19 . i) in ( rng f) by A16, A31, A39, A40, FUNCT_1:def 3;

        hence thesis by A38, A41;

      end;

      then

      reconsider h1 = h19 as FinSequence of ( TOP-REAL 2) by FINSEQ_1:def 4;

      

       A42: ( len h1) >= 1 by A30, A34, XXREAL_0: 2;

      then

       A43: (h1 . 1) = (h1 /. 1) by FINSEQ_4: 15;

      

       A44: for i st 1 <= i & (i + 1) <= ( len h1) holds |.((h1 /. i) - (h1 /. (i + 1))).| < e

      proof

        reconsider Pa = P as Subset of ( TOP-REAL 2);

        reconsider W1 = P as Subset of ( Euclid 2) by TOPREAL3: 8;

        let i;

        assume that

         A45: 1 <= i and

         A46: (i + 1) <= ( len h1);

        

         A47: 1 < (i + 1) by A45, NAT_1: 13;

        then

         A48: (h . (i + 1)) = (h /. (i + 1)) by A34, A46, FINSEQ_4: 15;

        

         A49: (i + 1) in ( dom h19) by A46, A47, FINSEQ_3: 25;

        then

         A50: (h19 . (i + 1)) = (f1 . (h . (i + 1))) by A35;

        then

         A51: (h1 /. (i + 1)) = (f1 . (h . (i + 1))) by A46, A47, FINSEQ_4: 15;

        

         A52: i < ( len h1) by A46, NAT_1: 13;

        then

         A53: (h . i) = (h /. i) by A34, A45, FINSEQ_4: 15;

        

         A54: i in ( dom h) by A34, A45, A52, FINSEQ_3: 25;

        then

         A55: (h . i) in ( rng h) by FUNCT_1:def 3;

        

         A56: (i + 1) in ( dom h) by A34, A46, A47, FINSEQ_3: 25;

        then (h . (i + 1)) in ( rng h) by FUNCT_1:def 3;

        then

        reconsider R = [.(h /. i), (h /. (i + 1)).] as Subset of I[01] by A31, A55, A53, A48, BORSUK_1: 40, XXREAL_2:def 12;

        reconsider W = (f1 .: R) as Subset of ( Euclid 2) by TOPREAL3: 8;

        

         A57: Pa is compact by A1, JORDAN5A: 1;

        reconsider Pa as non empty Subset of ( TOP-REAL 2);

        

         A58: ( rng f) = ( [#] (( TOP-REAL 2) | P)) by A13, TOPS_2:def 5

        .= P by PRE_TOPC:def 5;

        set r1 = (((( E-bound Pa) - ( W-bound Pa)) + (( N-bound Pa) - ( S-bound Pa))) + 1);

        

         A59: for x,y be Point of ( Euclid 2) st x in W1 & y in W1 holds ( dist (x,y)) <= r1

        proof

          let x,y be Point of ( Euclid 2);

          assume that

           A60: x in W1 and

           A61: y in W1;

          reconsider pw1 = x, pw2 = y as Point of ( TOP-REAL 2) by A60, A61;

          

           A62: ( S-bound Pa) <= (pw2 `2 ) & (pw2 `2 ) <= ( N-bound Pa) by A57, A61, PSCOMP_1: 24;

          ( S-bound Pa) <= (pw1 `2 ) & (pw1 `2 ) <= ( N-bound Pa) by A57, A60, PSCOMP_1: 24;

          then

           A63: |.((pw1 `2 ) - (pw2 `2 )).| <= (( N-bound Pa) - ( S-bound Pa)) by A62, Th27;

          

           A64: ( W-bound Pa) <= (pw2 `1 ) & (pw2 `1 ) <= ( E-bound Pa) by A57, A61, PSCOMP_1: 24;

          ( W-bound Pa) <= (pw1 `1 ) & (pw1 `1 ) <= ( E-bound Pa) by A57, A60, PSCOMP_1: 24;

          then |.((pw1 `1 ) - (pw2 `1 )).| <= (( E-bound Pa) - ( W-bound Pa)) by A64, Th27;

          then

           A65: ( |.((pw1 `1 ) - (pw2 `1 )).| + |.((pw1 `2 ) - (pw2 `2 )).|) <= ((( E-bound Pa) - ( W-bound Pa)) + (( N-bound Pa) - ( S-bound Pa))) by A63, XREAL_1: 7;

          ((( E-bound Pa) - ( W-bound Pa)) + (( N-bound Pa) - ( S-bound Pa))) <= (((( E-bound Pa) - ( W-bound Pa)) + (( N-bound Pa) - ( S-bound Pa))) + 1) by XREAL_1: 29;

          then

           A66: ( |.((pw1 `1 ) - (pw2 `1 )).| + |.((pw1 `2 ) - (pw2 `2 )).|) <= r1 by A65, XXREAL_0: 2;

          ( dist (x,y)) = |.(pw1 - pw2).| & |.(pw1 - pw2).| <= ( |.((pw1 `1 ) - (pw2 `1 )).| + |.((pw1 `2 ) - (pw2 `2 )).|) by Th28, Th32;

          hence thesis by A66, XXREAL_0: 2;

        end;

        

         A67: p1 in Pa by A1, TOPREAL1: 1;

        then ( S-bound Pa) <= (p1 `2 ) & (p1 `2 ) <= ( N-bound Pa) by A57, PSCOMP_1: 24;

        then ( S-bound Pa) <= ( N-bound Pa) by XXREAL_0: 2;

        then

         A68: 0 <= (( N-bound Pa) - ( S-bound Pa)) by XREAL_1: 48;

        ( W-bound Pa) <= (p1 `1 ) & (p1 `1 ) <= ( E-bound Pa) by A57, A67, PSCOMP_1: 24;

        then ( W-bound Pa) <= ( E-bound Pa) by XXREAL_0: 2;

        then 0 <= (( E-bound Pa) - ( W-bound Pa)) by XREAL_1: 48;

        then

         A69: W1 is bounded by A68, A59, TBSP_1:def 7;

        

         A70: ( dom f1) = ( [#] I[01] ) by A13, A16, TOPS_2:def 5

        .= the carrier of I[01] ;

        (i + 1) in ( dom h) by A34, A46, A47, FINSEQ_3: 25;

        then (h . (i + 1)) in ( rng h) by FUNCT_1:def 3;

        then (h19 . (i + 1)) in ( rng f) by A16, A31, A50, A70, FUNCT_1:def 3;

        then

         A71: (f1 . (h . (i + 1))) is Element of ( TOP-REAL 2) by A35, A49, A58;

        

         A72: i in ( dom h19) by A45, A52, FINSEQ_3: 25;

        then

         A73: (h19 . i) = (f1 . (h . i)) by A35;

        then (h19 . i) in ( rng f) by A16, A31, A55, A70, FUNCT_1:def 3;

        then (f1 . (h . i)) is Element of ( TOP-REAL 2) by A35, A72, A58;

        then

        reconsider w1 = (f1 . (h . i)), w2 = (f1 . (h . (i + 1))) as Point of ( Euclid 2) by A71, TOPREAL3: 8;

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

        then

         A74: (h /. i) <= (h /. (i + 1)) by A32, A54, A53, A56, A48, SEQM_3:def 1;

        then (h . i) in R by A53, XXREAL_1: 1;

        then

         A75: w1 in (f1 .: R) by A70, FUNCT_1:def 6;

        (h . (i + 1)) in R by A48, A74, XXREAL_1: 1;

        then

         A76: w2 in (f1 .: R) by A70, FUNCT_1:def 6;

        ( dom f1) = ( [#] I[01] ) by A13, A16, TOPS_2:def 5;

        then P = (f1 .: [. 0 , 1.]) by A16, A58, BORSUK_1: 40, RELAT_1: 113;

        then W is bounded by A69, BORSUK_1: 40, RELAT_1: 123, TBSP_1: 14;

        then

         A77: ( dist (w1,w2)) <= ( diameter W) by A75, A76, TBSP_1:def 8;

        ( diameter W) < e by A33, A34, A45, A52;

        then

         A78: ( dist (w1,w2)) < e by A77, XXREAL_0: 2;

        (h1 /. i) = (f1 . (h . i)) by A45, A52, A73, FINSEQ_4: 15;

        hence thesis by A51, A78, Th28;

      end;

      

       A79: for i st i in ( dom h1) holds ((h1 /. 1) `1 ) <= ((h1 /. i) `1 ) & ((h1 /. i) `1 ) <= ((h1 /. ( len h1)) `1 )

      proof

        ( len h) in ( dom h19) by A34, A42, FINSEQ_3: 25;

        then (h1 . ( len h1)) = (f1 . (h . ( len h))) by A34, A35;

        then

         A80: (h1 /. ( len h1)) = (f1 . (h . ( len h))) by A42, FINSEQ_4: 15;

        let i;

        assume

         A81: i in ( dom h1);

        then (h1 . i) = (f1 . (h . i)) by A35;

        then

         A82: (h1 /. i) = (f1 . (h . i)) by A81, PARTFUN1:def 6;

        i in ( Seg ( len h)) by A34, A81, FINSEQ_1:def 3;

        then i in ( dom h) by FINSEQ_1:def 3;

        then

         A83: (h . i) in ( rng h) by FUNCT_1:def 3;

        ( dom f1) = ( [#] I[01] ) by A13, A16, TOPS_2:def 5

        .= the carrier of I[01] ;

        then

         A84: (h1 /. i) in ( rng f) by A16, A31, A82, A83, FUNCT_1:def 3;

        1 in ( dom h19) by A42, FINSEQ_3: 25;

        then (h1 . 1) = (f1 . (h . 1)) by A35;

        then

         A85: (h1 /. 1) = (f1 . (h . 1)) by A42, FINSEQ_4: 15;

        ( rng f) = ( [#] (( TOP-REAL 2) | P)) by A13, TOPS_2:def 5

        .= P by PRE_TOPC:def 5;

        hence thesis by A3, A14, A15, A16, A28, A29, A85, A80, A84;

      end;

      for i st i in ( dom ( X_axis h1)) holds (( X_axis h1) . 1) <= (( X_axis h1) . i) & (( X_axis h1) . i) <= (( X_axis h1) . ( len h1))

      proof

        let i;

        

         A86: (( X_axis h1) . 1) = ((h1 /. 1) `1 ) & (( X_axis h1) . ( len h1)) = ((h1 /. ( len h1)) `1 ) by A42, Th40;

        assume i in ( dom ( X_axis h1));

        then i in ( Seg ( len ( X_axis h1))) by FINSEQ_1:def 3;

        then i in ( Seg ( len h1)) by A42, Th40;

        then

         A87: i in ( dom h1) by FINSEQ_1:def 3;

        then (( X_axis h1) . i) = ((h1 /. i) `1 ) by Th42;

        hence thesis by A79, A87, A86;

      end;

      then

       A88: ( X_axis h1) lies_between ((( X_axis h1) . 1),(( X_axis h1) . ( len h1))) by GOBOARD4:def 2;

      

       A89: for i st i in ( dom h1) holds (q1 `2 ) <= ((h1 /. i) `2 ) & ((h1 /. i) `2 ) <= (q2 `2 )

      proof

        let i;

        

         A90: ( rng f) = ( [#] (( TOP-REAL 2) | P)) by A13, TOPS_2:def 5

        .= P by PRE_TOPC:def 5;

        assume

         A91: i in ( dom h1);

        then (h1 . i) = (f1 . (h . i)) by A35;

        then

         A92: (h1 /. i) = (f1 . (h . i)) by A91, PARTFUN1:def 6;

        i in ( Seg ( len h1)) by A91, FINSEQ_1:def 3;

        then i in ( dom h) by A34, FINSEQ_1:def 3;

        then

         A93: (h . i) in ( rng h) by FUNCT_1:def 3;

        ( dom f1) = ( [#] I[01] ) by A13, A16, TOPS_2:def 5

        .= the carrier of I[01] ;

        then (h1 /. i) in ( rng f) by A16, A31, A92, A93, FUNCT_1:def 3;

        hence thesis by A5, A90;

      end;

      for i st i in ( dom ( Y_axis h1)) holds (q1 `2 ) <= (( Y_axis h1) . i) & (( Y_axis h1) . i) <= (q2 `2 )

      proof

        let i;

        assume i in ( dom ( Y_axis h1));

        then i in ( Seg ( len ( Y_axis h1))) by FINSEQ_1:def 3;

        then i in ( Seg ( len h1)) by A42, Th41;

        then

         A94: i in ( dom h1) by FINSEQ_1:def 3;

        then (( Y_axis h1) . i) = ((h1 /. i) `2 ) by Th42;

        hence thesis by A89, A94;

      end;

      then ( Y_axis h1) lies_between ((q1 `2 ),(q2 `2 )) by GOBOARD4:def 2;

      then

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

       A95: f2 is special and

       A96: (f2 . 1) = (h1 . 1) and

       A97: (f2 . ( len f2)) = (h1 . ( len h1)) and

       A98: ( len f2) >= ( len h1) and

       A99: ( X_axis f2) lies_between ((( X_axis h1) . 1),(( X_axis h1) . ( len h1))) & ( Y_axis f2) lies_between ((q1 `2 ),(q2 `2 )) and

       A100: for j st j in ( dom f2) holds ex k st k in ( dom h1) & |.((f2 /. j) - (h1 /. k)).| < e and

       A101: for j st 1 <= j & (j + 1) <= ( len f2) holds |.((f2 /. j) - (f2 /. (j + 1))).| < e by A21, A44, A42, A88, Th38;

      

       A102: ( len f2) >= 1 by A42, A98, XXREAL_0: 2;

      then

       A103: (f2 . ( len f2)) = (f2 /. ( len f2)) by FINSEQ_4: 15;

      deffunc F( Nat) = (g1 . (hb . $1));

      ex h29 be FinSequence st ( len h29) = ( len hb) & for i be Nat st i in ( dom h29) holds (h29 . i) = F(i) from FINSEQ_1:sch 2;

      then

      consider h29 be FinSequence such that

       A104: ( len h29) = ( len hb) and

       A105: for i be Nat st i in ( dom h29) holds (h29 . i) = (g1 . (hb . i));

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

      proof

        let y be object;

        assume y in ( rng h29);

        then

        consider x be object such that

         A106: x in ( dom h29) and

         A107: y = (h29 . x) by FUNCT_1:def 3;

        reconsider i = x as Element of NAT by A106;

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

        then i in ( dom hb) by A104, A106, FINSEQ_1:def 3;

        then

         A108: (hb . i) in ( rng hb) by FUNCT_1:def 3;

        

         A109: ( dom g1) = ( [#] I[01] ) by A7, A18, TOPS_2:def 5

        .= the carrier of I[01] ;

        

         A110: ( rng g) = ( [#] (( TOP-REAL 2) | Q)) by A7, TOPS_2:def 5

        .= Q by PRE_TOPC:def 5;

        (h29 . i) = (g1 . (hb . i)) by A105, A106;

        then (h29 . i) in ( rng g) by A18, A25, A108, A109, FUNCT_1:def 3;

        hence thesis by A107, A110;

      end;

      then

      reconsider h2 = h29 as FinSequence of ( TOP-REAL 2) by FINSEQ_1:def 4;

      

       A111: ( rng f) = ( [#] (( TOP-REAL 2) | P)) by A13, TOPS_2:def 5

      .= P by PRE_TOPC:def 5;

      

       A112: for i st 1 <= i & (i + 1) <= ( len h2) holds |.((h2 /. i) - (h2 /. (i + 1))).| < e

      proof

        reconsider Qa = Q as Subset of ( TOP-REAL 2);

        reconsider W1 = Q as Subset of ( Euclid 2) by TOPREAL3: 8;

        let i;

        assume that

         A113: 1 <= i and

         A114: (i + 1) <= ( len h2);

        

         A115: Qa is compact by A2, JORDAN5A: 1;

        reconsider Qa as non empty Subset of ( TOP-REAL 2);

        

         A116: ( rng g) = ( [#] (( TOP-REAL 2) | Q)) by A7, TOPS_2:def 5

        .= Q by PRE_TOPC:def 5;

        set r1 = (((( E-bound Qa) - ( W-bound Qa)) + (( N-bound Qa) - ( S-bound Qa))) + 1);

        

         A117: for x,y be Point of ( Euclid 2) st x in W1 & y in W1 holds ( dist (x,y)) <= r1

        proof

          let x,y be Point of ( Euclid 2);

          assume that

           A118: x in W1 and

           A119: y in W1;

          reconsider pw1 = x, pw2 = y as Point of ( TOP-REAL 2) by A118, A119;

          

           A120: ( S-bound Qa) <= (pw2 `2 ) & (pw2 `2 ) <= ( N-bound Qa) by A115, A119, PSCOMP_1: 24;

          ( S-bound Qa) <= (pw1 `2 ) & (pw1 `2 ) <= ( N-bound Qa) by A115, A118, PSCOMP_1: 24;

          then

           A121: |.((pw1 `2 ) - (pw2 `2 )).| <= (( N-bound Qa) - ( S-bound Qa)) by A120, Th27;

          

           A122: ( W-bound Qa) <= (pw2 `1 ) & (pw2 `1 ) <= ( E-bound Qa) by A115, A119, PSCOMP_1: 24;

          ( W-bound Qa) <= (pw1 `1 ) & (pw1 `1 ) <= ( E-bound Qa) by A115, A118, PSCOMP_1: 24;

          then |.((pw1 `1 ) - (pw2 `1 )).| <= (( E-bound Qa) - ( W-bound Qa)) by A122, Th27;

          then

           A123: ( |.((pw1 `1 ) - (pw2 `1 )).| + |.((pw1 `2 ) - (pw2 `2 )).|) <= ((( E-bound Qa) - ( W-bound Qa)) + (( N-bound Qa) - ( S-bound Qa))) by A121, XREAL_1: 7;

          ((( E-bound Qa) - ( W-bound Qa)) + (( N-bound Qa) - ( S-bound Qa))) <= (((( E-bound Qa) - ( W-bound Qa)) + (( N-bound Qa) - ( S-bound Qa))) + 1) by XREAL_1: 29;

          then

           A124: ( |.((pw1 `1 ) - (pw2 `1 )).| + |.((pw1 `2 ) - (pw2 `2 )).|) <= r1 by A123, XXREAL_0: 2;

          ( dist (x,y)) = |.(pw1 - pw2).| & |.(pw1 - pw2).| <= ( |.((pw1 `1 ) - (pw2 `1 )).| + |.((pw1 `2 ) - (pw2 `2 )).|) by Th28, Th32;

          hence thesis by A124, XXREAL_0: 2;

        end;

        

         A125: q1 in Qa by A2, TOPREAL1: 1;

        then ( S-bound Qa) <= (q1 `2 ) & (q1 `2 ) <= ( N-bound Qa) by A115, PSCOMP_1: 24;

        then ( S-bound Qa) <= ( N-bound Qa) by XXREAL_0: 2;

        then

         A126: 0 <= (( N-bound Qa) - ( S-bound Qa)) by XREAL_1: 48;

        ( W-bound Qa) <= (q1 `1 ) & (q1 `1 ) <= ( E-bound Qa) by A115, A125, PSCOMP_1: 24;

        then ( W-bound Qa) <= ( E-bound Qa) by XXREAL_0: 2;

        then 0 <= (( E-bound Qa) - ( W-bound Qa)) by XREAL_1: 48;

        then

         A127: W1 is bounded by A126, A117, TBSP_1:def 7;

        

         A128: ( dom g1) = ( [#] I[01] ) by A7, A18, TOPS_2:def 5

        .= the carrier of I[01] ;

        

         A129: 1 < (i + 1) by A113, NAT_1: 13;

        then (i + 1) in ( Seg ( len hb)) by A104, A114, FINSEQ_1: 1;

        then (i + 1) in ( dom hb) by FINSEQ_1:def 3;

        then

         A130: (hb . (i + 1)) in ( rng hb) by FUNCT_1:def 3;

        

         A131: i < ( len h2) by A114, NAT_1: 13;

        then

         A132: (hb . i) = (hb /. i) by A104, A113, FINSEQ_4: 15;

        

         A133: (i + 1) in ( dom h29) by A114, A129, FINSEQ_3: 25;

        then (h29 . (i + 1)) = (g1 . (hb . (i + 1))) by A105;

        then (h29 . (i + 1)) in ( rng g) by A18, A25, A128, A130, FUNCT_1:def 3;

        then

         A134: (g1 . (hb . (i + 1))) is Element of ( TOP-REAL 2) by A105, A133, A116;

        

         A135: (hb . (i + 1)) = (hb /. (i + 1)) by A104, A114, A129, FINSEQ_4: 15;

        i in ( dom h29) by A113, A131, FINSEQ_3: 25;

        then

         A136: (h29 . i) = (g1 . (hb . i)) by A105;

        i in ( Seg ( len hb)) by A104, A113, A131, FINSEQ_1: 1;

        then

         A137: i in ( dom hb) by FINSEQ_1:def 3;

        then

         A138: (hb . i) in ( rng hb) by FUNCT_1:def 3;

        then (h29 . i) in ( rng g) by A18, A25, A136, A128, FUNCT_1:def 3;

        then

        reconsider w1 = (g1 . (hb . i)), w2 = (g1 . (hb . (i + 1))) as Point of ( Euclid 2) by A136, A116, A134, TOPREAL3: 8;

        (i + 1) in ( Seg ( len hb)) by A104, A114, A129, FINSEQ_1: 1;

        then

         A139: (i + 1) in ( dom hb) by FINSEQ_1:def 3;

        then (hb . (i + 1)) in ( rng hb) by FUNCT_1:def 3;

        then

        reconsider R = [.(hb /. i), (hb /. (i + 1)).] as Subset of I[01] by A25, A138, A132, A135, BORSUK_1: 40, XXREAL_2:def 12;

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

        then

         A140: (hb /. i) <= (hb /. (i + 1)) by A26, A137, A132, A139, A135, SEQM_3:def 1;

        then (hb . i) in R by A132, XXREAL_1: 1;

        then

         A141: w1 in (g1 .: R) by A128, FUNCT_1:def 6;

        (hb . (i + 1)) in R by A135, A140, XXREAL_1: 1;

        then

         A142: w2 in (g1 .: R) by A128, FUNCT_1:def 6;

        reconsider W = (g1 .: R) as Subset of ( Euclid 2) by TOPREAL3: 8;

        ( dom g1) = ( [#] I[01] ) by A7, A18, TOPS_2:def 5;

        then Q = (g1 .: [. 0 , 1.]) by A18, A116, BORSUK_1: 40, RELAT_1: 113;

        then W is bounded by A127, BORSUK_1: 40, RELAT_1: 123, TBSP_1: 14;

        then

         A143: ( dist (w1,w2)) <= ( diameter W) by A141, A142, TBSP_1:def 8;

        ( diameter W) < e by A27, A104, A113, A131;

        then

         A144: ( dist (w1,w2)) < e by A143, XXREAL_0: 2;

        (h2 . (i + 1)) = (h2 /. (i + 1)) by A114, A129, FINSEQ_4: 15;

        then

         A145: (h2 /. (i + 1)) = (g1 . (hb . (i + 1))) by A105, A133;

        (h2 /. i) = (g1 . (hb . i)) by A113, A131, A136, FINSEQ_4: 15;

        hence thesis by A145, A144, Th28;

      end;

      

       A146: 1 <= ( len hb) by A24, XXREAL_0: 2;

      then

       A147: ( len hb) in ( dom hb) by FINSEQ_3: 25;

      

       A148: 1 <= ( len hb) by A24, XXREAL_0: 2;

      then

       A149: (h2 . ( len h2)) = (h2 /. ( len h2)) by A104, FINSEQ_4: 15;

      

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

      

       A151: for i st i in ( dom hb) holds (h2 /. i) = (g1 . (hb . i))

      proof

        let i;

        assume

         A152: i in ( dom hb);

        then i in ( dom h29) by A104, FINSEQ_3: 29;

        then

         A153: (h2 . i) = (g1 . (hb . i)) by A105;

        1 <= i & i <= ( len hb) by A150, A152, FINSEQ_1: 1;

        hence thesis by A104, A153, FINSEQ_4: 15;

      end;

      

       A154: (f2 . 1) = (f2 /. 1) by A102, FINSEQ_4: 15;

      

       A155: 1 <= ( len h) by A30, XXREAL_0: 2;

      then 1 in ( dom h19) by A34, FINSEQ_3: 25;

      then

       A156: (h1 /. 1) = (f1 . (h . 1)) by A35, A43;

      ( len h) in ( dom h19) by A34, A155, FINSEQ_3: 25;

      then

       A157: (f2 /. 1) <> (f2 /. ( len f2)) by A1, A14, A15, A16, A28, A29, A34, A35, A96, A97, A43, A154, A103, A156, JORDAN6: 37;

      5 <= ( len f2) by A30, A34, A98, XXREAL_0: 2;

      then

       A158: 2 <= ( len f2) by XXREAL_0: 2;

      

       A159: (h1 . ( len h1)) = (h1 /. ( len h1)) by A42, FINSEQ_4: 15;

      

      then

       A160: (( X_axis f2) . ( len f2)) = ((h1 /. ( len h1)) `1 ) by A97, A102, A103, Th40

      .= (( X_axis h1) . ( len h1)) by A42, Th40;

      

       A161: (h2 . 1) = (h2 /. 1) by A148, A104, FINSEQ_4: 15;

      

       A162: ( len h2) >= 1 by A24, A104, XXREAL_0: 2;

      

       A163: for i st i in ( dom h2) holds ((h2 /. 1) `2 ) <= ((h2 /. i) `2 ) & ((h2 /. i) `2 ) <= ((h2 /. ( len h2)) `2 )

      proof

        let i;

        assume i in ( dom h2);

        then i in ( Seg ( len h2)) by FINSEQ_1:def 3;

        then i in ( dom hb) by A104, FINSEQ_1:def 3;

        then

         A164: (h2 /. i) = (g1 . (hb . i)) & (hb . i) in ( rng hb) by A151, FUNCT_1:def 3;

        ( dom g1) = ( [#] I[01] ) by A7, A18, TOPS_2:def 5

        .= the carrier of I[01] ;

        then

         A165: (h2 /. i) in ( rng g) by A18, A25, A164, FUNCT_1:def 3;

        1 in ( Seg ( len hb)) by A104, A162, FINSEQ_1: 1;

        then 1 in ( dom hb) by FINSEQ_1:def 3;

        then

         A166: (h2 /. 1) = (g1 . (hb . 1)) by A151;

        ( len hb) in ( Seg ( len hb)) by A104, A162, FINSEQ_1: 1;

        then ( len hb) in ( dom hb) by FINSEQ_1:def 3;

        then

         A167: (h2 /. ( len h2)) = (g1 . (hb . ( len hb))) by A104, A151;

        ( rng g) = ( [#] (( TOP-REAL 2) | Q)) by A7, TOPS_2:def 5

        .= Q by PRE_TOPC:def 5;

        hence thesis by A6, A8, A9, A18, A22, A23, A166, A167, A165;

      end;

      for i st i in ( dom ( Y_axis h2)) holds (( Y_axis h2) . 1) <= (( Y_axis h2) . i) & (( Y_axis h2) . i) <= (( Y_axis h2) . ( len h2))

      proof

        let i;

        

         A168: (( Y_axis h2) . 1) = ((h2 /. 1) `2 ) & (( Y_axis h2) . ( len h2)) = ((h2 /. ( len h2)) `2 ) by A162, Th41;

        assume i in ( dom ( Y_axis h2));

        then i in ( Seg ( len ( Y_axis h2))) by FINSEQ_1:def 3;

        then i in ( Seg ( len h2)) by A162, Th41;

        then

         A169: i in ( dom h2) by FINSEQ_1:def 3;

        then (( Y_axis h2) . i) = ((h2 /. i) `2 ) by Th42;

        hence thesis by A163, A169, A168;

      end;

      then

       A170: ( Y_axis h2) lies_between ((( Y_axis h2) . 1),(( Y_axis h2) . ( len h2))) by GOBOARD4:def 2;

      

       A171: for i st i in ( dom h2) holds (p1 `1 ) <= ((h2 /. i) `1 ) & ((h2 /. i) `1 ) <= (p2 `1 )

      proof

        let i;

        

         A172: ( rng g) = ( [#] (( TOP-REAL 2) | Q)) by A7, TOPS_2:def 5

        .= Q by PRE_TOPC:def 5;

        assume i in ( dom h2);

        then i in ( Seg ( len h2)) by FINSEQ_1:def 3;

        then i in ( dom hb) by A104, FINSEQ_1:def 3;

        then

         A173: (h2 /. i) = (g1 . (hb . i)) & (hb . i) in ( rng hb) by A151, FUNCT_1:def 3;

        ( dom g1) = ( [#] I[01] ) by A7, A18, TOPS_2:def 5

        .= the carrier of I[01] ;

        then (h2 /. i) in ( rng g) by A18, A25, A173, FUNCT_1:def 3;

        hence thesis by A4, A172;

      end;

      for i st i in ( dom ( X_axis h2)) holds (p1 `1 ) <= (( X_axis h2) . i) & (( X_axis h2) . i) <= (p2 `1 )

      proof

        let i;

        assume i in ( dom ( X_axis h2));

        then i in ( Seg ( len ( X_axis h2))) by FINSEQ_1:def 3;

        then i in ( Seg ( len h2)) by A162, Th40;

        then

         A174: i in ( dom h2) by FINSEQ_1:def 3;

        then (( X_axis h2) . i) = ((h2 /. i) `1 ) by Th42;

        hence thesis by A171, A174;

      end;

      then ( X_axis h2) lies_between ((p1 `1 ),(p2 `1 )) by GOBOARD4:def 2;

      then

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

       A175: g2 is special and

       A176: (g2 . 1) = (h2 . 1) and

       A177: (g2 . ( len g2)) = (h2 . ( len h2)) and

       A178: ( len g2) >= ( len h2) and

       A179: ( Y_axis g2) lies_between ((( Y_axis h2) . 1),(( Y_axis h2) . ( len h2))) & ( X_axis g2) lies_between ((p1 `1 ),(p2 `1 )) and

       A180: for j st j in ( dom g2) holds ex k st k in ( dom h2) & |.((g2 /. j) - (h2 /. k)).| < e and

       A181: for j st 1 <= j & (j + 1) <= ( len g2) holds |.((g2 /. j) - (g2 /. (j + 1))).| < e by A21, A162, A170, A112, Th39;

      5 <= ( len g2) by A24, A104, A178, XXREAL_0: 2;

      then

       A182: 2 <= ( len g2) by XXREAL_0: 2;

      

       A183: ( len g2) >= 1 by A162, A178, XXREAL_0: 2;

      then (g2 . 1) = (g2 /. 1) by FINSEQ_4: 15;

      

      then

       A184: (( Y_axis g2) . 1) = ((h2 /. 1) `2 ) by A176, A183, A161, Th41

      .= (( Y_axis h2) . 1) by A162, Th41;

      1 in ( dom hb) by A146, FINSEQ_3: 25;

      then (h2 /. 1) = (g1 . (hb . 1)) by A151;

      then

       A185: (g2 . 1) <> (g2 . ( len g2)) by A2, A8, A9, A18, A22, A23, A104, A151, A176, A177, A161, A149, A147, JORDAN6: 37;

      ( len hb) in ( dom hb) by A148, FINSEQ_3: 25;

      then

       A186: (g2 . ( len g2)) = q2 by A9, A18, A23, A104, A151, A177, A149;

      (g2 /. ( len g2)) = (g2 . ( len g2)) by A183, FINSEQ_4: 15;

      then

       A187: (( Y_axis g2) . ( len g2)) = (q2 `2 ) by A183, A186, Th41;

      1 in ( dom hb) by A148, FINSEQ_3: 25;

      then

       A188: (h2 /. 1) = q1 by A8, A18, A22, A151;

      

       A189: ( rng g) = ( [#] (( TOP-REAL 2) | Q)) by A7, TOPS_2:def 5

      .= Q by PRE_TOPC:def 5;

      ( len h) in ( dom h19) by A34, A42, FINSEQ_3: 25;

      then (h1 /. ( len h1)) = p2 by A15, A16, A29, A34, A35, A159;

      then

       A190: (( X_axis f2) . ( len f2)) = (p2 `1 ) by A97, A102, A159, A103, Th40;

      1 in ( dom h19) by A42, FINSEQ_3: 25;

      then (h1 . 1) = (f1 . (h . 1)) by A35;

      then

       A191: (( X_axis f2) . 1) = (p1 `1 ) by A14, A16, A28, A96, A102, A154, Th40;

      (g2 . ( len g2)) = (g2 /. ( len g2)) by A183, FINSEQ_4: 15;

      

      then

       A192: (( Y_axis g2) . ( len g2)) = ((h2 /. ( len h2)) `2 ) by A177, A183, A149, Th41

      .= (( Y_axis h2) . ( len h2)) by A162, Th41;

      (g2 /. 1) = (g2 . 1) by A183, FINSEQ_4: 15;

      then

       A193: (( Y_axis g2) . 1) = (q1 `2 ) by A176, A183, A188, A161, Th41;

      (( X_axis f2) . 1) = ((h1 /. 1) `1 ) by A96, A102, A43, A154, Th40

      .= (( X_axis h1) . 1) by A42, Th40;

      then ( L~ f2) meets ( L~ g2) by A95, A99, A175, A179, A154, A103, A191, A190, A193, A187, A160, A184, A192, A158, A182, A157, A185, Th26;

      then

      consider s be object such that

       A194: s in ( L~ f2) and

       A195: s in ( L~ g2) by XBOOLE_0: 3;

      reconsider ps = s as Point of ( TOP-REAL 2) by A194;

      ps in ( union { ( LSeg (g2,j)) : 1 <= j & (j + 1) <= ( len g2) }) by A195, TOPREAL1:def 4;

      then

      consider y such that

       A196: ps in y & y in { ( LSeg (g2,j)) : 1 <= j & (j + 1) <= ( len g2) } by TARSKI:def 4;

      ps in ( union { ( LSeg (f2,i)) : 1 <= i & (i + 1) <= ( len f2) }) by A194, TOPREAL1:def 4;

      then

      consider x such that

       A197: ps in x & x in { ( LSeg (f2,i)) : 1 <= i & (i + 1) <= ( len f2) } by TARSKI:def 4;

      consider i such that

       A198: x = ( LSeg (f2,i)) and

       A199: 1 <= i and

       A200: (i + 1) <= ( len f2) by A197;

      ( LSeg (f2,i)) = ( LSeg ((f2 /. i),(f2 /. (i + 1)))) by A199, A200, TOPREAL1:def 3;

      then

       A201: |.(ps - (f2 /. i)).| <= |.((f2 /. i) - (f2 /. (i + 1))).| by A197, A198, Th35;

      i < ( len f2) by A200, NAT_1: 13;

      then i in ( dom f2) by A199, FINSEQ_3: 25;

      then

      consider k such that

       A202: k in ( dom h1) and

       A203: |.((f2 /. i) - (h1 /. k)).| < e by A100;

      k in ( dom h) by A34, A202, FINSEQ_3: 29;

      then

       A204: (h . k) in ( rng h) by FUNCT_1:def 3;

      reconsider p11 = (h1 /. k) as Point of ( TOP-REAL 2);

       |.((f2 /. i) - (f2 /. (i + 1))).| < e by A101, A199, A200;

      then |.(ps - (f2 /. i)).| < e by A201, XXREAL_0: 2;

      then |.(ps - (h1 /. k)).| <= ( |.(ps - (f2 /. i)).| + |.((f2 /. i) - (h1 /. k)).|) & ( |.(ps - (f2 /. i)).| + |.((f2 /. i) - (h1 /. k)).|) < (e + e) by A203, TOPRNS_1: 34, XREAL_1: 8;

      then |.(ps - (h1 /. k)).| < (e + e) by XXREAL_0: 2;

      then

       A205: |.(p11 - ps).| < (e + e) by TOPRNS_1: 27;

      k in ( Seg ( len h1)) by A202, FINSEQ_1:def 3;

      then 1 <= k & k <= ( len h1) by FINSEQ_1: 1;

      then (h1 . k) = (h1 /. k) by FINSEQ_4: 15;

      then

       A206: (h1 /. k) = (f1 . (h . k)) by A35, A202;

      consider j such that

       A207: y = ( LSeg (g2,j)) and

       A208: 1 <= j and

       A209: (j + 1) <= ( len g2) by A196;

      ( LSeg (g2,j)) = ( LSeg ((g2 /. j),(g2 /. (j + 1)))) by A208, A209, TOPREAL1:def 3;

      then

       A210: |.(ps - (g2 /. j)).| <= |.((g2 /. j) - (g2 /. (j + 1))).| by A196, A207, Th35;

      j < ( len g2) by A209, NAT_1: 13;

      then j in ( Seg ( len g2)) by A208, FINSEQ_1: 1;

      then j in ( dom g2) by FINSEQ_1:def 3;

      then

      consider k9 be Nat such that

       A211: k9 in ( dom h2) and

       A212: |.((g2 /. j) - (h2 /. k9)).| < e by A180;

      k9 in ( Seg ( len h2)) by A211, FINSEQ_1:def 3;

      then

       A213: k9 in ( dom hb) by A104, FINSEQ_1:def 3;

      then

       A214: (hb . k9) in ( rng hb) by FUNCT_1:def 3;

      reconsider q11 = (h2 /. k9) as Point of ( TOP-REAL 2);

       |.((g2 /. j) - (g2 /. (j + 1))).| < e by A181, A208, A209;

      then |.(ps - (g2 /. j)).| < e by A210, XXREAL_0: 2;

      then |.(ps - (h2 /. k9)).| <= ( |.(ps - (g2 /. j)).| + |.((g2 /. j) - (h2 /. k9)).|) & ( |.(ps - (g2 /. j)).| + |.((g2 /. j) - (h2 /. k9)).|) < (e + e) by A212, TOPRNS_1: 34, XREAL_1: 8;

      then |.(ps - (h2 /. k9)).| < (e + e) by XXREAL_0: 2;

      then |.(p11 - q11).| <= ( |.(p11 - ps).| + |.(ps - q11).|) & ( |.(p11 - ps).| + |.(ps - q11).|) < ((e + e) + (e + e)) by A205, TOPRNS_1: 34, XREAL_1: 8;

      then

       A215: |.(p11 - q11).| < (((e + e) + e) + e) by XXREAL_0: 2;

      (h2 /. k9) = (g1 . (hb . k9)) by A151, A213;

      then

       A216: (h2 /. k9) in ( rng g) by A18, A25, A214, A36, FUNCT_1:def 3;

      reconsider x1 = p11, x2 = q11 as Point of ( Euclid 2) by EUCLID: 22;

      ( dom f1) = ( [#] I[01] ) by A13, A16, TOPS_2:def 5

      .= the carrier of I[01] ;

      then (h1 /. k) in P by A16, A31, A206, A204, A111, FUNCT_1:def 3;

      then ( min_dist_min (P9,Q9)) <= ( dist (x1,x2)) by A11, A12, A216, A189, WEIERSTR: 34;

      then ( min_dist_min (P9,Q9)) <= |.(p11 - q11).| by Th28;

      then ( min_dist_min (P9,Q9)) < (4 * e) by A215, XXREAL_0: 2;

      then ((4 * e) - (5 * e)) > 0 by XREAL_1: 50;

      then (((4 - 5) * e) / e) > 0 by A21, XREAL_1: 139;

      then (4 - 5) > 0 by A20;

      hence contradiction;

    end;

    reserve X,Y for non empty TopSpace;

    theorem :: JGRAPH_1:45

    

     Th44: for f be Function of X, Y, P be non empty Subset of Y, f1 be Function of X, (Y | P) st f = f1 & f is continuous holds f1 is continuous

    proof

      let f be Function of X, Y, P be non empty Subset of Y, f1 be Function of X, (Y | P);

      assume that

       A1: f = f1 and

       A2: f is continuous;

      

       A3: ( [#] Y) <> {} ;

      

       A4: for P1 be Subset of (Y | P) st P1 is open holds (f1 " P1) is open

      proof

        let P1 be Subset of (Y | P);

        assume P1 is open;

        then P1 in the topology of (Y | P) by PRE_TOPC:def 2;

        then

        consider Q be Subset of Y such that

         A5: Q in the topology of Y and

         A6: P1 = (Q /\ ( [#] (Y | P))) by PRE_TOPC:def 4;

        reconsider Q as Subset of Y;

        

         A7: (f " Q) = (f1 " (( rng f1) /\ Q)) by A1, RELAT_1: 133;

        

         A8: ( [#] (Y | P)) = P by PRE_TOPC:def 5;

        then (( rng f1) /\ Q) c= (P /\ Q) by XBOOLE_1: 26;

        then

         A9: (f1 " (( rng f1) /\ Q)) c= (f1 " P1) by A6, A8, RELAT_1: 143;

        Q is open by A5, PRE_TOPC:def 2;

        then

         A10: (f " Q) is open by A3, A2, TOPS_2: 43;

        (f1 " P1) c= (f " Q) by A1, A6, RELAT_1: 143, XBOOLE_1: 17;

        hence thesis by A10, A7, A9, XBOOLE_0:def 10;

      end;

      ( [#] (Y | P)) <> {} ;

      hence thesis by A4, TOPS_2: 43;

    end;

    theorem :: JGRAPH_1:46

    

     Th45: for f be Function of X, Y, P be non empty Subset of Y st X is compact & Y is T_2 & f is continuous one-to-one & P = ( rng f) holds ex f1 be Function of X, (Y | P) st f = f1 & f1 is being_homeomorphism

    proof

      let f be Function of X, Y, P be non empty Subset of Y such that

       A1: X is compact and

       A2: Y is T_2 and

       A3: f is continuous one-to-one and

       A4: P = ( rng f);

      the carrier of (Y | P) = P & ( dom f) = the carrier of X by FUNCT_2:def 1, PRE_TOPC: 8;

      then

      reconsider f2 = f as Function of X, (Y | P) by A4, FUNCT_2: 1;

      

       A5: ( dom f2) = ( [#] X) & f2 is continuous by A3, Th44, FUNCT_2:def 1;

      ( rng f2) = ( [#] (Y | P)) & (Y | P) is T_2 by A2, A4, PRE_TOPC:def 5, TOPMETR: 2;

      hence thesis by A1, A3, A5, COMPTS_1: 17;

    end;

    ::$Notion-Name

    theorem :: JGRAPH_1:47

    for f,g be Function of I[01] , ( TOP-REAL 2), a,b,c,d be Real, O,I be Point of I[01] st O = 0 & I = 1 & f is continuous one-to-one & g is continuous one-to-one & ((f . O) `1 ) = a & ((f . I) `1 ) = b & ((g . O) `2 ) = c & ((g . I) `2 ) = d & (for r be Point of I[01] holds a <= ((f . r) `1 ) & ((f . r) `1 ) <= b & a <= ((g . r) `1 ) & ((g . r) `1 ) <= b & c <= ((f . r) `2 ) & ((f . r) `2 ) <= d & c <= ((g . r) `2 ) & ((g . r) `2 ) <= d) holds ( rng f) meets ( rng g)

    proof

      let f,g be Function of I[01] , ( TOP-REAL 2), a,b,c,d be Real, O,I be Point of I[01] ;

      assume that

       A1: O = 0 & I = 1 and

       A2: f is continuous one-to-one and

       A3: g is continuous one-to-one and

       A4: ((f . O) `1 ) = a and

       A5: ((f . I) `1 ) = b and

       A6: ((g . O) `2 ) = c and

       A7: ((g . I) `2 ) = d and

       A8: for r be Point of I[01] holds a <= ((f . r) `1 ) & ((f . r) `1 ) <= b & a <= ((g . r) `1 ) & ((g . r) `1 ) <= b & c <= ((f . r) `2 ) & ((f . r) `2 ) <= d & c <= ((g . r) `2 ) & ((g . r) `2 ) <= d;

      reconsider P = ( rng f) as non empty Subset of ( TOP-REAL 2);

      

       A9: I[01] is compact by HEINE: 4, TOPMETR: 20;

      then

      consider f1 be Function of I[01] , (( TOP-REAL 2) | P) such that

       A10: f = f1 and

       A11: f1 is being_homeomorphism by A2, Th45;

      reconsider Q = ( rng g) as non empty Subset of ( TOP-REAL 2);

      consider g1 be Function of I[01] , (( TOP-REAL 2) | Q) such that

       A12: g = g1 and

       A13: g1 is being_homeomorphism by A3, A9, Th45;

      reconsider q2 = (g1 . I) as Point of ( TOP-REAL 2) by A7, A12;

      reconsider q1 = (g1 . O) as Point of ( TOP-REAL 2) by A6, A12;

      

       A14: Q is_an_arc_of (q1,q2) by A1, A13, TOPREAL1:def 1;

      reconsider p2 = (f1 . I) as Point of ( TOP-REAL 2) by A5, A10;

      reconsider p1 = (f1 . O) as Point of ( TOP-REAL 2) by A4, A10;

      

       A15: for p be Point of ( TOP-REAL 2) st p in P holds (p1 `1 ) <= (p `1 ) & (p `1 ) <= (p2 `1 )

      proof

        let p be Point of ( TOP-REAL 2);

        assume p in P;

        then ex x be object st x in ( dom f1) & p = (f1 . x) by A10, FUNCT_1:def 3;

        hence thesis by A4, A5, A8, A10;

      end;

      

       A16: for p be Point of ( TOP-REAL 2) st p in Q holds (p1 `1 ) <= (p `1 ) & (p `1 ) <= (p2 `1 )

      proof

        let p be Point of ( TOP-REAL 2);

        assume p in Q;

        then ex x be object st x in ( dom g1) & p = (g1 . x) by A12, FUNCT_1:def 3;

        hence thesis by A4, A5, A8, A10, A12;

      end;

      

       A17: for p be Point of ( TOP-REAL 2) st p in Q holds (q1 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 )

      proof

        let p be Point of ( TOP-REAL 2);

        assume p in Q;

        then ex x be object st x in ( dom g1) & p = (g1 . x) by A12, FUNCT_1:def 3;

        hence thesis by A6, A7, A8, A12;

      end;

      

       A18: for p be Point of ( TOP-REAL 2) st p in P holds (q1 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 )

      proof

        let p be Point of ( TOP-REAL 2);

        assume p in P;

        then ex x be object st x in ( dom f1) & p = (f1 . x) by A10, FUNCT_1:def 3;

        hence thesis by A6, A7, A8, A10, A12;

      end;

      P is_an_arc_of (p1,p2) by A1, A11, TOPREAL1:def 1;

      hence thesis by A14, A15, A16, A18, A17, Th43;

    end;