glib_011.miz



    begin

    definition

      let G1,G2 be _Graph;

      :: GLIB_011:def1

      mode PVertexMapping of G1,G2 -> PartFunc of ( the_Vertices_of G1), ( the_Vertices_of G2) means

      : Def1: for v,w be Vertex of G1 st v in ( dom it ) & w in ( dom it ) & (v,w) are_adjacent holds ((it /. v),(it /. w)) are_adjacent ;

      existence

      proof

        take the empty PartFunc of ( the_Vertices_of G1), ( the_Vertices_of G2);

        thus thesis;

      end;

    end

    theorem :: GLIB_011:1

    

     Th1: for G1,G2 be _Graph holds for f be PartFunc of ( the_Vertices_of G1), ( the_Vertices_of G2) holds f is PVertexMapping of G1, G2 iff for v,w,e be object st v in ( dom f) & w in ( dom f) & e Joins (v,w,G1) holds ex e9 be object st e9 Joins ((f . v),(f . w),G2)

    proof

      let G1,G2 be _Graph;

      let f be PartFunc of ( the_Vertices_of G1), ( the_Vertices_of G2);

      hereby

        assume

         A1: f is PVertexMapping of G1, G2;

        let v,w,e be object;

        assume

         A2: v in ( dom f) & w in ( dom f) & e Joins (v,w,G1);

        then

        reconsider v0 = v, w0 = w as Vertex of G1;

        (v0,w0) are_adjacent by A2, CHORD:def 3;

        then

        consider e9 be object such that

         A3: e9 Joins ((f /. v0),(f /. w0),G2) by A1, A2, Def1, CHORD:def 3;

        take e9;

        (f /. v0) = (f . v) & (f /. w0) = (f . w) by A2, PARTFUN1:def 6;

        hence e9 Joins ((f . v),(f . w),G2) by A3;

      end;

      assume

       A4: for v,w,e be object st v in ( dom f) & w in ( dom f) & e Joins (v,w,G1) holds ex e9 be object st e9 Joins ((f . v),(f . w),G2);

      let v,w be Vertex of G1;

      assume

       A5: v in ( dom f) & w in ( dom f);

      assume (v,w) are_adjacent ;

      then

      consider e be object such that

       A6: e Joins (v,w,G1) by CHORD:def 3;

      consider e9 be object such that

       A7: e9 Joins ((f . v),(f . w),G2) by A4, A5, A6;

      (f /. v) = (f . v) & (f /. w) = (f . w) by A5, PARTFUN1:def 6;

      hence thesis by A7, CHORD:def 3;

    end;

    definition

      let G1,G2 be _Graph, f be PVertexMapping of G1, G2;

      :: GLIB_011:def2

      attr f is directed means

      : Def2: for v,w,e be object st v in ( dom f) & w in ( dom f) & e DJoins (v,w,G1) holds ex e9 be object st e9 DJoins ((f . v),(f . w),G2);

      :: GLIB_011:def3

      attr f is continuous means for v,w be Vertex of G1 st v in ( dom f) & w in ( dom f) & ((f /. v),(f /. w)) are_adjacent holds (v,w) are_adjacent ;

      :: GLIB_011:def4

      attr f is Dcontinuous means

      : Def4: for v,w,e9 be object st v in ( dom f) & w in ( dom f) & e9 DJoins ((f . v),(f . w),G2) holds ex e be object st e DJoins (v,w,G1);

    end

    theorem :: GLIB_011:2

    

     Th2: for G1,G2 be _Graph, f be PVertexMapping of G1, G2 holds f is continuous iff for v,w,e9 be object st v in ( dom f) & w in ( dom f) & e9 Joins ((f . v),(f . w),G2) holds ex e be object st e Joins (v,w,G1)

    proof

      let G1,G2 be _Graph;

      let f be PVertexMapping of G1, G2;

      hereby

        assume

         A1: f is continuous;

        let v,w,e9 be object;

        assume

         A2: v in ( dom f) & w in ( dom f) & e9 Joins ((f . v),(f . w),G2);

        then

        reconsider v0 = v, w0 = w as Vertex of G1;

        (f /. v0) = (f . v) & (f /. w0) = (f . w) by A2, PARTFUN1:def 6;

        then ((f /. v0),(f /. w0)) are_adjacent by A2, CHORD:def 3;

        then

        consider e be object such that

         A3: e Joins (v0,w0,G1) by A1, A2, CHORD:def 3;

        take e;

        thus e Joins (v,w,G1) by A3;

      end;

      assume

       A4: for v,w,e9 be object st v in ( dom f) & w in ( dom f) & e9 Joins ((f . v),(f . w),G2) holds ex e be object st e Joins (v,w,G1);

      let v,w be Vertex of G1;

      assume

       A5: v in ( dom f) & w in ( dom f);

      assume ((f /. v),(f /. w)) are_adjacent ;

      then

      consider e9 be object such that

       A6: e9 Joins ((f /. v),(f /. w),G2) by CHORD:def 3;

      (f /. v) = (f . v) & (f /. w) = (f . w) by A5, PARTFUN1:def 6;

      then

      consider e be object such that

       A7: e Joins (v,w,G1) by A4, A5, A6;

      thus thesis by A7, CHORD:def 3;

    end;

    theorem :: GLIB_011:3

    for G1,G2 be _Graph, f be PVertexMapping of G1, G2 holds f is continuous iff for v,w be Vertex of G1 st v in ( dom f) & w in ( dom f) holds (v,w) are_adjacent iff ((f /. v),(f /. w)) are_adjacent by Def1;

    registration

      let G1,G2 be _Graph;

      cluster Dcontinuous -> continuous for PVertexMapping of G1, G2;

      coherence

      proof

        let f be PVertexMapping of G1, G2;

        assume

         A1: f is Dcontinuous;

        now

          let v,w,e9 be object;

          assume

           A2: v in ( dom f) & w in ( dom f) & e9 Joins ((f . v),(f . w),G2);

          per cases by GLIB_000: 16;

            suppose e9 DJoins ((f . v),(f . w),G2);

            then

            consider e be object such that

             A3: e DJoins (v,w,G1) by A1, A2;

            take e;

            thus e Joins (v,w,G1) by A3, GLIB_000: 16;

          end;

            suppose e9 DJoins ((f . w),(f . v),G2);

            then

            consider e be object such that

             A4: e DJoins (w,v,G1) by A1, A2;

            take e;

            thus e Joins (v,w,G1) by A4, GLIB_000: 16;

          end;

        end;

        hence thesis by Th2;

      end;

      cluster empty -> one-to-one Dcontinuous directed continuous for PVertexMapping of G1, G2;

      coherence ;

      cluster total -> non empty for PVertexMapping of G1, G2;

      coherence ;

      cluster onto -> non empty for PVertexMapping of G1, G2;

      coherence

      proof

        let f be PVertexMapping of G1, G2;

        assume f is onto;

        then ( rng f) = ( the_Vertices_of G2) by FUNCT_2:def 3;

        hence thesis;

      end;

    end

    registration

      let G1 be simple _Graph, G2 be _Graph;

      cluster Dcontinuous -> directed for PVertexMapping of G1, G2;

      coherence

      proof

        let f be PVertexMapping of G1, G2;

        assume

         A1: f is Dcontinuous;

        let v,w,e be object;

        assume

         A2: v in ( dom f) & w in ( dom f) & e DJoins (v,w,G1);

        then

         A3: e Joins (v,w,G1) by GLIB_000: 16;

        then

        consider e9 be object such that

         A4: e9 Joins ((f . v),(f . w),G2) by A2, Th1;

        take e9;

        assume not e9 DJoins ((f . v),(f . w),G2);

        then e9 DJoins ((f . w),(f . v),G2) by A4, GLIB_000: 16;

        then

        consider e0 be object such that

         A5: e0 DJoins (w,v,G1) by A1, A2;

        e0 Joins (v,w,G1) by A5, GLIB_000: 16;

        then e = e0 by A3, GLIB_000:def 20;

        then (( the_Source_of G1) . e) = w by A5, GLIB_000:def 14;

        then v = w by A2, GLIB_000:def 14;

        hence contradiction by A3, GLIB_000: 18;

      end;

    end

    registration

      let G1 be _Graph, G2 be simple _Graph;

      cluster directed continuous -> Dcontinuous for PVertexMapping of G1, G2;

      coherence

      proof

        let f be PVertexMapping of G1, G2;

        assume

         A1: f is directed continuous;

        let v,w,e9 be object;

        assume

         A2: v in ( dom f) & w in ( dom f) & e9 DJoins ((f . v),(f . w),G2);

        then

         A3: e9 Joins ((f . v),(f . w),G2) by GLIB_000: 16;

        then

        consider e be object such that

         A4: e Joins (v,w,G1) by A1, A2, Th2;

        take e;

        assume not e DJoins (v,w,G1);

        then e DJoins (w,v,G1) by A4, GLIB_000: 16;

        then

        consider e0 be object such that

         A5: e0 DJoins ((f . w),(f . v),G2) by A1, A2;

        e0 Joins ((f . v),(f . w),G2) by A5, GLIB_000: 16;

        then e0 = e9 by A3, GLIB_000:def 20;

        then (( the_Source_of G2) . e9) = (f . w) by A5, GLIB_000:def 14;

        then (f . w) = (f . v) by A2, GLIB_000:def 14;

        hence contradiction by A3, GLIB_000: 18;

      end;

    end

    registration

      let G1 be _trivial _Graph, G2 be _Graph;

      cluster -> directed for PVertexMapping of G1, G2;

      coherence

      proof

        let f be PVertexMapping of G1, G2;

        consider v0 be Vertex of G1 such that

         A1: ( the_Vertices_of G1) = {v0} by GLIB_000: 22;

        let v,w,e be object;

        assume

         A2: v in ( dom f) & w in ( dom f) & e DJoins (v,w,G1);

        then e Joins (v,w,G1) by GLIB_000: 16;

        then

        consider e9 be object such that

         A3: e9 Joins ((f . v),(f . w),G2) by A2, Th1;

        take e9;

        v = v0 & w = v0 by A1, A2, TARSKI:def 1;

        hence e9 DJoins ((f . v),(f . w),G2) by A3, GLIB_000: 16;

      end;

      cluster continuous -> Dcontinuous for PVertexMapping of G1, G2;

      coherence

      proof

        let f be PVertexMapping of G1, G2;

        assume

         A4: f is continuous;

        consider v0 be Vertex of G1 such that

         A5: ( the_Vertices_of G1) = {v0} by GLIB_000: 22;

        let v,w,e9 be object;

        assume

         A6: v in ( dom f) & w in ( dom f) & e9 DJoins ((f . v),(f . w),G2);

        then e9 Joins ((f . v),(f . w),G2) by GLIB_000: 16;

        then

        consider e be object such that

         A7: e Joins (v,w,G1) by A4, A6, Th2;

        take e;

        v = v0 & w = v0 by A5, A6, TARSKI:def 1;

        hence e DJoins (v,w,G1) by A7, GLIB_000: 16;

      end;

      cluster non empty -> total for PVertexMapping of G1, G2;

      coherence

      proof

        let f be PVertexMapping of G1, G2;

        assume

         A8: f is non empty;

        consider v be Vertex of G1 such that

         A9: ( the_Vertices_of G1) = {v} by GLIB_000: 22;

        ( dom f) = ( the_Vertices_of G1) by A8, A9, ZFMISC_1: 33;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let G1 be _Graph, G2 be _trivial _Graph;

      cluster non empty -> onto for PVertexMapping of G1, G2;

      coherence

      proof

        let f be PVertexMapping of G1, G2;

        assume

         A1: f is non empty;

        consider v be Vertex of G2 such that

         A2: ( the_Vertices_of G2) = {v} by GLIB_000: 22;

        ( rng f) = ( the_Vertices_of G2) by A1, A2, ZFMISC_1: 33;

        hence thesis by FUNCT_2:def 3;

      end;

    end

    registration

      let G1 be _Graph, G2 be _trivial loopless _Graph;

      cluster -> Dcontinuous continuous for PVertexMapping of G1, G2;

      coherence

      proof

        let f be PVertexMapping of G1, G2;

        consider v0 be Vertex of G2 such that

         A1: ( the_Vertices_of G2) = {v0} by GLIB_000: 22;

        now

          let v,w,e9 be object;

          assume

           A2: v in ( dom f) & w in ( dom f) & e9 DJoins ((f . v),(f . w),G2);

          then (f . v) in ( rng f) & (f . w) in ( rng f) by FUNCT_1: 3;

          then (f . v) = v0 & (f . w) = v0 by A1, TARSKI:def 1;

          then e9 Joins (v0,v0,G2) by A2, GLIB_000: 16;

          hence ex e be object st e DJoins (v,w,G1) by GLIB_000: 18;

        end;

        hence f is Dcontinuous;

        hence f is continuous;

      end;

    end

    registration

      let G1,G2 be _Graph;

      cluster empty one-to-one directed continuous Dcontinuous for PVertexMapping of G1, G2;

      existence

      proof

        set f = the empty PartFunc of ( the_Vertices_of G1), ( the_Vertices_of G2);

        for v,w be Vertex of G1 st v in ( dom f) & w in ( dom f) & (v,w) are_adjacent holds ((f /. v),(f /. w)) are_adjacent ;

        then

        reconsider f as PVertexMapping of G1, G2 by Def1;

        take f;

        thus thesis;

      end;

    end

    theorem :: GLIB_011:4

    for G1,G2 be _Graph holds for f be PartFunc of ( the_Vertices_of G1), ( the_Vertices_of G2) holds f is directed PVertexMapping of G1, G2 iff for v,w,e be object st v in ( dom f) & w in ( dom f) & e DJoins (v,w,G1) holds ex e9 be object st e9 DJoins ((f . v),(f . w),G2)

    proof

      let G1,G2 be _Graph;

      let f be PartFunc of ( the_Vertices_of G1), ( the_Vertices_of G2);

      thus f is directed PVertexMapping of G1, G2 implies for v,w,e be object st v in ( dom f) & w in ( dom f) & e DJoins (v,w,G1) holds ex e9 be object st e9 DJoins ((f . v),(f . w),G2) by Def2;

      assume

       A1: for v,w,e be object st v in ( dom f) & w in ( dom f) & e DJoins (v,w,G1) holds ex e9 be object st e9 DJoins ((f . v),(f . w),G2);

      now

        let v,w,e be object;

        assume

         A2: v in ( dom f) & w in ( dom f) & e Joins (v,w,G1);

        per cases by GLIB_000: 16;

          suppose e DJoins (v,w,G1);

          then

          consider e9 be object such that

           A3: e9 DJoins ((f . v),(f . w),G2) by A1, A2;

          take e9;

          thus e9 Joins ((f . v),(f . w),G2) by A3, GLIB_000: 16;

        end;

          suppose e DJoins (w,v,G1);

          then

          consider e9 be object such that

           A4: e9 DJoins ((f . w),(f . v),G2) by A1, A2;

          take e9;

          thus e9 Joins ((f . v),(f . w),G2) by A4, GLIB_000: 16;

        end;

      end;

      hence thesis by A1, Th1, Def2;

    end;

    registration

      let G1 be loopless _Graph, G2 be _Graph;

      cluster non empty one-to-one directed for PVertexMapping of G1, G2;

      existence

      proof

        set v1 = the Vertex of G1, v2 = the Vertex of G2;

        set f = (v1 .--> v2);

        f = ( {v1} --> v2) by FUNCOP_1:def 9;

        then

        reconsider f as one-to-one PartFunc of ( the_Vertices_of G1), ( the_Vertices_of G2);

        now

          let v,w be Vertex of G1;

          assume

           A1: v in ( dom f) & w in ( dom f) & (v,w) are_adjacent ;

          then v = v1 & w = v1 by FUNCOP_1: 75;

          hence ((f /. v),(f /. w)) are_adjacent by A1, GLIB_009: 39;

        end;

        then

        reconsider f as PVertexMapping of G1, G2 by Def1;

        take f;

        thus f is non empty one-to-one;

        thus f is directed

        proof

          let v,w,e be object;

          assume

           A2: v in ( dom f) & w in ( dom f) & e DJoins (v,w,G1);

          then v = v1 & w = v1 by FUNCOP_1: 75;

          then e Joins (v1,v1,G1) by A2, GLIB_000: 16;

          hence thesis by GLIB_000: 18;

        end;

      end;

    end

    registration

      let G1,G2 be loopless _Graph;

      cluster non empty one-to-one directed continuous Dcontinuous for PVertexMapping of G1, G2;

      existence

      proof

        set v1 = the Vertex of G1, v2 = the Vertex of G2;

        set f = (v1 .--> v2);

        f = ( {v1} --> v2) by FUNCOP_1:def 9;

        then

        reconsider f as one-to-one PartFunc of ( the_Vertices_of G1), ( the_Vertices_of G2);

        now

          let v,w be Vertex of G1;

          assume

           A1: v in ( dom f) & w in ( dom f) & (v,w) are_adjacent ;

          then v = v1 & w = v1 by FUNCOP_1: 75;

          hence ((f /. v),(f /. w)) are_adjacent by A1, GLIB_009: 39;

        end;

        then

        reconsider f as PVertexMapping of G1, G2 by Def1;

        take f;

        thus f is non empty one-to-one;

        thus f is directed

        proof

          let v,w,e be object;

          assume

           A2: v in ( dom f) & w in ( dom f) & e DJoins (v,w,G1);

          then v = v1 & w = v1 by FUNCOP_1: 75;

          then e Joins (v1,v1,G1) by A2, GLIB_000: 16;

          hence thesis by GLIB_000: 18;

        end;

        thus f is continuous

        proof

          let v,w be Vertex of G1;

          assume

           A3: v in ( dom f) & w in ( dom f) & ((f /. v),(f /. w)) are_adjacent ;

          then v = v1 & w = v1 by FUNCOP_1: 75;

          hence (v,w) are_adjacent by A3, GLIB_009: 39;

        end;

        thus f is Dcontinuous

        proof

          let v,w,e9 be object;

          assume

           A4: v in ( dom f) & w in ( dom f) & e9 DJoins ((f . v),(f . w),G2);

          then v = v1 & w = v1 by FUNCOP_1: 75;

          then e9 Joins ((f . v1),(f . v1),G2) by A4, GLIB_000: 16;

          hence thesis by GLIB_000: 18;

        end;

      end;

    end

    registration

      let G1,G2 be non loopless _Graph;

      cluster non empty one-to-one directed continuous Dcontinuous for PVertexMapping of G1, G2;

      existence

      proof

        consider v1 be object such that

         A1: ex e1 be object st e1 Joins (v1,v1,G1) by GLIB_000: 18;

        reconsider v1 as Vertex of G1 by A1, GLIB_000: 13;

        consider v2 be object such that

         A2: ex e2 be object st e2 Joins (v2,v2,G2) by GLIB_000: 18;

        reconsider v2 as Vertex of G2 by A2, GLIB_000: 13;

        set f = (v1 .--> v2);

        f = ( {v1} --> v2) by FUNCOP_1:def 9;

        then

        reconsider f as one-to-one PartFunc of ( the_Vertices_of G1), ( the_Vertices_of G2);

        now

          let v,w be Vertex of G1;

          assume

           A3: v in ( dom f) & w in ( dom f) & (v,w) are_adjacent ;

          then v = v1 & w = v1 by FUNCOP_1: 75;

          then (f /. v) = (f . v1) & (f /. w) = (f . v1) by A3, PARTFUN1:def 6;

          then (f /. v) = v2 & (f /. w) = v2 by FUNCOP_1: 72;

          hence ((f /. v),(f /. w)) are_adjacent by A2, CHORD:def 3;

        end;

        then

        reconsider f as PVertexMapping of G1, G2 by Def1;

        take f;

        thus f is non empty one-to-one;

        thus f is directed

        proof

          let v,w,e be object;

          assume v in ( dom f) & w in ( dom f) & e DJoins (v,w,G1);

          then v = v1 & w = v1 by FUNCOP_1: 75;

          then

           A4: (f . v) = v2 & (f . w) = v2 by FUNCOP_1: 72;

          then

          consider e2 be object such that

           A5: e2 Joins ((f . v),(f . w),G2) by A2;

          take e2;

          thus thesis by A4, A5, GLIB_000: 16;

        end;

        thus f is continuous

        proof

          let v,w be Vertex of G1;

          assume v in ( dom f) & w in ( dom f) & ((f /. v),(f /. w)) are_adjacent ;

          then v = v1 & w = v1 by FUNCOP_1: 75;

          hence (v,w) are_adjacent by A1, CHORD:def 3;

        end;

        thus f is Dcontinuous

        proof

          let v,w,e9 be object;

          assume v in ( dom f) & w in ( dom f) & e9 DJoins ((f . v),(f . w),G2);

          then

           A6: v = v1 & w = v1 by FUNCOP_1: 75;

          then

          consider e1 be object such that

           A7: e1 Joins (v,w,G1) by A1;

          take e1;

          thus thesis by A6, A7, GLIB_000: 16;

        end;

      end;

    end

    theorem :: GLIB_011:5

    

     Th5: for G be _Graph holds ( id ( the_Vertices_of G)) is directed continuous Dcontinuous PVertexMapping of G, G

    proof

      let G be _Graph;

      set f = ( id ( the_Vertices_of G));

       A1:

      now

        let v,w,e be object;

        assume

         A2: v in ( dom f) & w in ( dom f) & e Joins (v,w,G);

        take e;

        e Joins (v,(f . w),G) by A2, FUNCT_1: 18;

        hence e Joins ((f . v),(f . w),G) by A2, FUNCT_1: 18;

      end;

       A3:

      now

        let v,w,e be object;

        assume

         A4: v in ( dom f) & w in ( dom f) & e DJoins (v,w,G);

        take e;

        e DJoins (v,(f . w),G) by A4, FUNCT_1: 18;

        hence e DJoins ((f . v),(f . w),G) by A4, FUNCT_1: 18;

      end;

       A5:

      now

        let v,w,e be object;

        assume

         A6: v in ( dom f) & w in ( dom f) & e Joins ((f . v),(f . w),G);

        take e;

        e Joins (v,(f . w),G) by A6, FUNCT_1: 18;

        hence e Joins (v,w,G) by A6, FUNCT_1: 18;

      end;

      now

        let v,w,e be object;

        assume

         A7: v in ( dom f) & w in ( dom f) & e DJoins ((f . v),(f . w),G);

        take e;

        e DJoins (v,(f . w),G) by A7, FUNCT_1: 18;

        hence e DJoins (v,w,G) by A7, FUNCT_1: 18;

      end;

      hence thesis by A1, A3, A5, Th1, Th2, Def2, Def4;

    end;

    theorem :: GLIB_011:6

    for G1,G2 be _Graph, f be PVertexMapping of G1, G2 st f is total holds (G2 is loopless implies G1 is loopless) & (G2 is edgeless implies G1 is edgeless)

    proof

      let G1,G2 be _Graph, f be PVertexMapping of G1, G2;

      assume

       A1: f is total;

      hereby

        assume

         A2: G2 is loopless;

        assume not G1 is loopless;

        then

        consider v be object such that

         A3: ex e be object st e Joins (v,v,G1) by GLIB_000: 18;

        consider e be object such that

         A4: e Joins (v,v,G1) by A3;

        v in ( the_Vertices_of G1) by A4, GLIB_000: 13;

        then v in ( dom f) by A1, PARTFUN1:def 2;

        then

        consider e9 be object such that

         A5: e9 Joins ((f . v),(f . v),G2) by A4, Th1;

        thus contradiction by A2, A5, GLIB_000: 18;

      end;

      hereby

        assume

         A6: G2 is edgeless;

        assume not G1 is edgeless;

        then

        consider e be object such that

         A7: e in ( the_Edges_of G1) by XBOOLE_0:def 1;

        set v = (( the_Source_of G1) . e), w = (( the_Target_of G1) . e);

        

         A8: e Joins (v,w,G1) by A7, GLIB_000:def 13;

        then v in ( the_Vertices_of G1) & w in ( the_Vertices_of G1) by GLIB_000: 13;

        then v in ( dom f) & w in ( dom f) by A1, FUNCT_2:def 1;

        then

        consider e9 be object such that

         A9: e9 Joins ((f . v),(f . w),G2) by A8, Th1;

        e9 in ( the_Edges_of G2) by A9, GLIB_000:def 13;

        hence contradiction by A6;

      end;

    end;

    theorem :: GLIB_011:7

    for G1,G2 be _Graph, f be continuous PVertexMapping of G1, G2 st f is onto holds (G1 is loopless implies G2 is loopless) & (G1 is edgeless implies G2 is edgeless)

    proof

      let G1,G2 be _Graph, f be continuous PVertexMapping of G1, G2;

      assume

       A1: f is onto;

      hereby

        assume

         A2: G1 is loopless;

        assume not G2 is loopless;

        then

        consider v be object such that

         A3: ex e be object st e Joins (v,v,G2) by GLIB_000: 18;

        consider e be object such that

         A4: e Joins (v,v,G2) by A3;

        v in ( the_Vertices_of G2) by A4, GLIB_000: 13;

        then v in ( rng f) by A1, FUNCT_2:def 3;

        then

        consider v0 be object such that

         A5: v0 in ( dom f) & (f . v0) = v by FUNCT_1:def 3;

        consider e0 be object such that

         A6: e0 Joins (v0,v0,G1) by A4, A5, Th2;

        thus contradiction by A2, A6, GLIB_000: 18;

      end;

      hereby

        assume

         A7: G1 is edgeless;

        assume not G2 is edgeless;

        then

        consider e9 be object such that

         A8: e9 in ( the_Edges_of G2) by XBOOLE_0:def 1;

        set v = (( the_Source_of G2) . e9), w = (( the_Target_of G2) . e9);

        

         A9: e9 Joins (v,w,G2) by A8, GLIB_000:def 13;

        then v in ( the_Vertices_of G2) & w in ( the_Vertices_of G2) by GLIB_000: 13;

        then

         A10: v in ( rng f) & w in ( rng f) by A1, FUNCT_2:def 3;

        then

        consider v0 be object such that

         A11: v0 in ( dom f) & (f . v0) = v by FUNCT_1:def 3;

        consider w0 be object such that

         A12: w0 in ( dom f) & (f . w0) = w by A10, FUNCT_1:def 3;

        consider e be object such that

         A13: e Joins (v0,w0,G1) by A9, A11, A12, Th2;

        e in ( the_Edges_of G1) by A13, GLIB_000:def 13;

        hence contradiction by A7;

      end;

    end;

    definition

      let G1,G2 be _Graph, f be PVertexMapping of G1, G2;

      :: GLIB_011:def5

      attr f is isomorphism means f is total one-to-one onto & for v,w be Vertex of G1 holds ( card (G1 .edgesBetween ( {v}, {w}))) = ( card (G2 .edgesBetween ( {(f . v)}, {(f . w)})));

      :: GLIB_011:def6

      attr f is Disomorphism means f is total one-to-one onto & for v,w be Vertex of G1 holds ( card (G1 .edgesDBetween ( {v}, {w}))) = ( card (G2 .edgesDBetween ( {(f . v)}, {(f . w)}))) & ( card (G1 .edgesDBetween ( {w}, {v}))) = ( card (G2 .edgesDBetween ( {(f . w)}, {(f . v)})));

    end

    registration

      let G1,G2 be _Graph;

      cluster isomorphism -> total one-to-one onto continuous for PVertexMapping of G1, G2;

      coherence

      proof

        let f be PVertexMapping of G1, G2;

        assume

         A1: f is isomorphism;

        hence f is total one-to-one onto;

        now

          let v,w,e9 be object;

          assume

           A2: v in ( dom f) & w in ( dom f) & e9 Joins ((f . v),(f . w),G2);

          then

          reconsider v0 = v, w0 = w as Vertex of G1;

          (f . v) in {(f . v)} & (f . w) in {(f . w)} by TARSKI:def 1;

          then e9 SJoins ( {(f . v)}, {(f . w)},G2) by A2, GLIB_000: 17;

          then e9 in (G2 .edgesBetween ( {(f . v)}, {(f . w)})) by GLIB_000:def 30;

          then ( card (G2 .edgesBetween ( {(f . v0)}, {(f . w0)}))) <> 0 ;

          then ( card (G1 .edgesBetween ( {v0}, {w0}))) <> 0 by A1;

          then (G1 .edgesBetween ( {v0}, {w0})) <> {} ;

          then

          consider e be object such that

           A3: e in (G1 .edgesBetween ( {v0}, {w0})) by XBOOLE_0:def 1;

          take e;

          e SJoins ( {v}, {w},G1) by A3, GLIB_000:def 30;

          then e in ( the_Edges_of G1) & ((( the_Source_of G1) . e) in {v} & (( the_Target_of G1) . e) in {w} or (( the_Source_of G1) . e) in {w} & (( the_Target_of G1) . e) in {v}) by GLIB_000:def 15;

          then e in ( the_Edges_of G1) & ((( the_Source_of G1) . e) = v & (( the_Target_of G1) . e) = w or (( the_Source_of G1) . e) = w & (( the_Target_of G1) . e) = v) by TARSKI:def 1;

          hence e Joins (v,w,G1) by GLIB_000:def 13;

        end;

        hence thesis by Th2;

      end;

      cluster Disomorphism -> total one-to-one onto isomorphism continuous directed Dcontinuous for PVertexMapping of G1, G2;

      coherence

      proof

        let f be PVertexMapping of G1, G2;

        assume

         A4: f is Disomorphism;

        hence f is total one-to-one onto;

        now

          let v,w be Vertex of G1;

          per cases ;

            suppose

             A5: v <> w;

            then

             A6: (f . v) <> (f . w) by A4, FUNCT_2: 19;

            

            thus ( card (G1 .edgesBetween ( {v}, {w}))) = ( card ((G1 .edgesDBetween ( {v}, {w})) \/ (G1 .edgesDBetween ( {w}, {v})))) by A5, GLIB_009: 14

            .= (( card (G1 .edgesDBetween ( {v}, {w}))) +` ( card (G1 .edgesDBetween ( {w}, {v})))) by A5, GLIB_009: 14, CARD_2: 35

            .= (( card (G1 .edgesDBetween ( {v}, {w}))) +` ( card (G2 .edgesDBetween ( {(f . w)}, {(f . v)})))) by A4

            .= (( card (G2 .edgesDBetween ( {(f . v)}, {(f . w)}))) +` ( card (G2 .edgesDBetween ( {(f . w)}, {(f . v)})))) by A4

            .= ( card ((G2 .edgesDBetween ( {(f . v)}, {(f . w)})) \/ (G2 .edgesDBetween ( {(f . w)}, {(f . v)})))) by A6, GLIB_009: 14, CARD_2: 35

            .= ( card (G2 .edgesBetween ( {(f . v)}, {(f . w)}))) by A6, GLIB_009: 14;

          end;

            suppose

             A7: v = w;

            

            thus ( card (G1 .edgesBetween ( {v}, {w}))) = ( card (G1 .edgesDBetween ( {v}, {w}))) by A7, GLIB_009: 15

            .= ( card (G2 .edgesDBetween ( {(f . v)}, {(f . w)}))) by A4

            .= ( card (G2 .edgesBetween ( {(f . v)}, {(f . w)}))) by A7, GLIB_009: 15;

          end;

        end;

        hence f is isomorphism by A4;

        hence f is continuous;

        now

          let v,w,e be object;

          assume

           A8: v in ( dom f) & w in ( dom f) & e DJoins (v,w,G1);

          then

          reconsider v0 = v, w0 = w as Vertex of G1;

          v in {v} & w in {w} by TARSKI:def 1;

          then e DSJoins ( {v}, {w},G1) by A8, GLIB_009: 7;

          then e in (G1 .edgesDBetween ( {v}, {w})) by GLIB_000:def 31;

          then ( card (G1 .edgesDBetween ( {v0}, {w0}))) <> 0 ;

          then ( card (G2 .edgesDBetween ( {(f . v0)}, {(f . w0)}))) <> 0 by A4;

          then (G2 .edgesDBetween ( {(f . v)}, {(f . w)})) <> {} ;

          then

          consider e9 be object such that

           A9: e9 in (G2 .edgesDBetween ( {(f . v)}, {(f . w)})) by XBOOLE_0:def 1;

          take e9;

          e9 DSJoins ( {(f . v)}, {(f . w)},G2) by A9, GLIB_000:def 31;

          then e9 in ( the_Edges_of G2) & (( the_Source_of G2) . e9) in {(f . v)} & (( the_Target_of G2) . e9) in {(f . w)} by GLIB_000:def 16;

          then e9 in ( the_Edges_of G2) & (( the_Source_of G2) . e9) = (f . v) & (( the_Target_of G2) . e9) = (f . w) by TARSKI:def 1;

          hence e9 DJoins ((f . v),(f . w),G2) by GLIB_000:def 14;

        end;

        hence f is directed;

        now

          let v,w,e9 be object;

          assume

           A10: v in ( dom f) & w in ( dom f) & e9 DJoins ((f . v),(f . w),G2);

          then

          reconsider v0 = v, w0 = w as Vertex of G1;

          (f . v) in {(f . v)} & (f . w) in {(f . w)} by TARSKI:def 1;

          then e9 DSJoins ( {(f . v)}, {(f . w)},G2) by A10, GLIB_009: 7;

          then e9 in (G2 .edgesDBetween ( {(f . v)}, {(f . w)})) by GLIB_000:def 31;

          then ( card (G2 .edgesDBetween ( {(f . v0)}, {(f . w0)}))) <> 0 ;

          then ( card (G1 .edgesDBetween ( {v0}, {w0}))) <> 0 by A4;

          then (G1 .edgesDBetween ( {v}, {w})) <> {} ;

          then

          consider e be object such that

           A11: e in (G1 .edgesDBetween ( {v}, {w})) by XBOOLE_0:def 1;

          take e;

          e DSJoins ( {v}, {w},G1) by A11, GLIB_000:def 31;

          then e in ( the_Edges_of G1) & (( the_Source_of G1) . e) in {v} & (( the_Target_of G1) . e) in {w} by GLIB_000:def 16;

          then e in ( the_Edges_of G1) & (( the_Source_of G1) . e) = v & (( the_Target_of G1) . e) = w by TARSKI:def 1;

          hence e DJoins (v,w,G1) by GLIB_000:def 14;

        end;

        hence f is Dcontinuous;

      end;

    end

    theorem :: GLIB_011:8

    

     Th8: for G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2 st f is total one-to-one continuous holds for v,w be Vertex of G1 holds ( card (G1 .edgesBetween ( {v}, {w}))) = ( card (G2 .edgesBetween ( {(f . v)}, {(f . w)})))

    proof

      let G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2;

      assume

       A1: f is total one-to-one continuous;

      let v,w be Vertex of G1;

      per cases ;

        suppose

         A2: (G1 .edgesBetween ( {v}, {w})) = {} ;

        (G2 .edgesBetween ( {(f . v)}, {(f . w)})) = {}

        proof

          assume (G2 .edgesBetween ( {(f . v)}, {(f . w)})) <> {} ;

          then

          consider e2 be object such that

           A3: (G2 .edgesBetween ( {(f . v)}, {(f . w)})) = {e2} by ZFMISC_1: 131;

          set v1 = (( the_Source_of G2) . e2), v2 = (( the_Target_of G2) . e2);

          e2 in (G2 .edgesBetween ( {(f . v)}, {(f . w)})) by A3, TARSKI:def 1;

          then e2 SJoins ( {(f . v)}, {(f . w)},G2) by GLIB_000:def 30;

          then

           A4: e2 in ( the_Edges_of G2) & (v1 in {(f . v)} & v2 in {(f . w)} or v1 in {(f . w)} & v2 in {(f . v)}) by GLIB_000:def 15;

          then v1 = (f . v) & v2 = (f . w) or v1 = (f . w) & v2 = (f . v) by TARSKI:def 1;

          then

           A5: e2 Joins ((f . v),(f . w),G2) by A4, GLIB_000:def 13;

          v in ( the_Vertices_of G1) & w in ( the_Vertices_of G1) & f is total by A1;

          then v in ( dom f) & w in ( dom f) by FUNCT_2:def 1;

          then

          consider e1 be object such that

           A6: e1 Joins (v,w,G1) by A1, A5, Th2;

          v in {v} & w in {w} by TARSKI:def 1;

          then e1 SJoins ( {v}, {w},G1) by A6, GLIB_000: 17;

          hence contradiction by A2, GLIB_000:def 30;

        end;

        hence ( card (G1 .edgesBetween ( {v}, {w}))) = ( card (G2 .edgesBetween ( {(f . v)}, {(f . w)}))) by A2;

      end;

        suppose (G1 .edgesBetween ( {v}, {w})) <> {} ;

        then

        consider e1 be object such that

         A7: (G1 .edgesBetween ( {v}, {w})) = {e1} by ZFMISC_1: 131;

        set v1 = (( the_Source_of G1) . e1), v2 = (( the_Target_of G1) . e1);

        e1 in (G1 .edgesBetween ( {v}, {w})) by A7, TARSKI:def 1;

        then e1 SJoins ( {v}, {w},G1) by GLIB_000:def 30;

        then

         A8: e1 in ( the_Edges_of G1) & (v1 in {v} & v2 in {w} or v1 in {w} & v2 in {v}) by GLIB_000:def 15;

        then v1 = v & v2 = w or v1 = w & v2 = v by TARSKI:def 1;

        then

         A9: e1 Joins (v,w,G1) by A8, GLIB_000:def 13;

        v in ( the_Vertices_of G1) & w in ( the_Vertices_of G1) & f is total by A1;

        then v in ( dom f) & w in ( dom f) by FUNCT_2:def 1;

        then

        consider e2 be object such that

         A10: e2 Joins ((f . v),(f . w),G2) by A9, Th1;

        (f . v) in {(f . v)} & (f . w) in {(f . w)} by TARSKI:def 1;

        then e2 SJoins ( {(f . v)}, {(f . w)},G2) by A10, GLIB_000: 17;

        then e2 in (G2 .edgesBetween ( {(f . v)}, {(f . w)})) by GLIB_000:def 30;

        then

        consider e be object such that

         A11: (G2 .edgesBetween ( {(f . v)}, {(f . w)})) = {e} by ZFMISC_1: 131;

        ( card (G1 .edgesBetween ( {v}, {w}))) = 1 & ( card (G2 .edgesBetween ( {(f . v)}, {(f . w)}))) = 1 by A7, A11, CARD_1: 30;

        hence ( card (G1 .edgesBetween ( {v}, {w}))) = ( card (G2 .edgesBetween ( {(f . v)}, {(f . w)})));

      end;

    end;

    definition

      let G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2;

      :: original: isomorphism

      redefine

      :: GLIB_011:def7

      attr f is isomorphism means f is total one-to-one onto continuous;

      compatibility by Th8;

    end

    registration

      let G1,G2 be non-multi _Graph;

      cluster total one-to-one onto continuous -> isomorphism for PVertexMapping of G1, G2;

      coherence ;

    end

    theorem :: GLIB_011:9

    

     Th9: for G1,G2 be non-Dmulti _Graph, f be PVertexMapping of G1, G2 st f is total one-to-one directed Dcontinuous holds for v,w be Vertex of G1 holds ( card (G1 .edgesDBetween ( {v}, {w}))) = ( card (G2 .edgesDBetween ( {(f . v)}, {(f . w)}))) & ( card (G1 .edgesDBetween ( {w}, {v}))) = ( card (G2 .edgesDBetween ( {(f . w)}, {(f . v)})))

    proof

      let G1,G2 be non-Dmulti _Graph, f be PVertexMapping of G1, G2;

      assume

       A1: f is total one-to-one directed Dcontinuous;

      let v,w be Vertex of G1;

      hereby

        per cases ;

          suppose

           A2: (G1 .edgesDBetween ( {v}, {w})) = {} ;

          (G2 .edgesDBetween ( {(f . v)}, {(f . w)})) = {}

          proof

            assume (G2 .edgesDBetween ( {(f . v)}, {(f . w)})) <> {} ;

            then

            consider e2 be object such that

             A3: (G2 .edgesDBetween ( {(f . v)}, {(f . w)})) = {e2} by ZFMISC_1: 131;

            set v1 = (( the_Source_of G2) . e2), v2 = (( the_Target_of G2) . e2);

            e2 in (G2 .edgesDBetween ( {(f . v)}, {(f . w)})) by A3, TARSKI:def 1;

            then e2 DSJoins ( {(f . v)}, {(f . w)},G2) by GLIB_000:def 31;

            then

             A4: e2 in ( the_Edges_of G2) & v1 in {(f . v)} & v2 in {(f . w)} by GLIB_000:def 16;

            then

             A5: v1 = (f . v) & v2 = (f . w) by TARSKI:def 1;

            v in ( the_Vertices_of G1) & w in ( the_Vertices_of G1) & f is total by A1;

            then v in ( dom f) & w in ( dom f) by FUNCT_2:def 1;

            then

            consider e1 be object such that

             A6: e1 DJoins (v,w,G1) by A1, A4, A5, GLIB_000:def 14;

            v in {v} & w in {w} by TARSKI:def 1;

            then e1 DSJoins ( {v}, {w},G1) by A6, GLIB_009: 7;

            hence contradiction by A2, GLIB_000:def 31;

          end;

          hence ( card (G1 .edgesDBetween ( {v}, {w}))) = ( card (G2 .edgesDBetween ( {(f . v)}, {(f . w)}))) by A2;

        end;

          suppose (G1 .edgesDBetween ( {v}, {w})) <> {} ;

          then

          consider e1 be object such that

           A7: (G1 .edgesDBetween ( {v}, {w})) = {e1} by ZFMISC_1: 131;

          set v1 = (( the_Source_of G1) . e1), v2 = (( the_Target_of G1) . e1);

          e1 in (G1 .edgesDBetween ( {v}, {w})) by A7, TARSKI:def 1;

          then e1 DSJoins ( {v}, {w},G1) by GLIB_000:def 31;

          then

           A8: e1 in ( the_Edges_of G1) & v1 in {v} & v2 in {w} by GLIB_000:def 16;

          then v1 = v & v2 = w by TARSKI:def 1;

          then

           A9: e1 DJoins (v,w,G1) by A8, GLIB_000:def 14;

          v in ( the_Vertices_of G1) & w in ( the_Vertices_of G1) & f is total by A1;

          then v in ( dom f) & w in ( dom f) by FUNCT_2:def 1;

          then

          consider e2 be object such that

           A10: e2 DJoins ((f . v),(f . w),G2) by A1, A9;

          (f . v) in {(f . v)} & (f . w) in {(f . w)} by TARSKI:def 1;

          then e2 DSJoins ( {(f . v)}, {(f . w)},G2) by A10, GLIB_009: 7;

          then e2 in (G2 .edgesDBetween ( {(f . v)}, {(f . w)})) by GLIB_000:def 31;

          then

          consider e be object such that

           A11: (G2 .edgesDBetween ( {(f . v)}, {(f . w)})) = {e} by ZFMISC_1: 131;

          ( card (G1 .edgesDBetween ( {v}, {w}))) = 1 & ( card (G2 .edgesDBetween ( {(f . v)}, {(f . w)}))) = 1 by A7, A11, CARD_1: 30;

          hence ( card (G1 .edgesDBetween ( {v}, {w}))) = ( card (G2 .edgesDBetween ( {(f . v)}, {(f . w)})));

        end;

      end;

      per cases ;

        suppose

         A12: (G1 .edgesDBetween ( {w}, {v})) = {} ;

        (G2 .edgesDBetween ( {(f . w)}, {(f . v)})) = {}

        proof

          assume (G2 .edgesDBetween ( {(f . w)}, {(f . v)})) <> {} ;

          then

          consider e2 be object such that

           A13: (G2 .edgesDBetween ( {(f . w)}, {(f . v)})) = {e2} by ZFMISC_1: 131;

          set v1 = (( the_Source_of G2) . e2), v2 = (( the_Target_of G2) . e2);

          e2 in (G2 .edgesDBetween ( {(f . w)}, {(f . v)})) by A13, TARSKI:def 1;

          then e2 DSJoins ( {(f . w)}, {(f . v)},G2) by GLIB_000:def 31;

          then

           A14: e2 in ( the_Edges_of G2) & v1 in {(f . w)} & v2 in {(f . v)} by GLIB_000:def 16;

          then

           A15: v1 = (f . w) & v2 = (f . v) by TARSKI:def 1;

          v in ( the_Vertices_of G1) & w in ( the_Vertices_of G1) & f is total by A1;

          then v in ( dom f) & w in ( dom f) by FUNCT_2:def 1;

          then

          consider e1 be object such that

           A16: e1 DJoins (w,v,G1) by A1, A14, A15, GLIB_000:def 14;

          v in {v} & w in {w} by TARSKI:def 1;

          then e1 DSJoins ( {w}, {v},G1) by A16, GLIB_009: 7;

          hence contradiction by A12, GLIB_000:def 31;

        end;

        hence ( card (G1 .edgesDBetween ( {w}, {v}))) = ( card (G2 .edgesDBetween ( {(f . w)}, {(f . v)}))) by A12;

      end;

        suppose (G1 .edgesDBetween ( {w}, {v})) <> {} ;

        then

        consider e1 be object such that

         A17: (G1 .edgesDBetween ( {w}, {v})) = {e1} by ZFMISC_1: 131;

        set v1 = (( the_Source_of G1) . e1), v2 = (( the_Target_of G1) . e1);

        e1 in (G1 .edgesDBetween ( {w}, {v})) by A17, TARSKI:def 1;

        then e1 DSJoins ( {w}, {v},G1) by GLIB_000:def 31;

        then

         A18: e1 in ( the_Edges_of G1) & v1 in {w} & v2 in {v} by GLIB_000:def 16;

        then v1 = w & v2 = v by TARSKI:def 1;

        then

         A19: e1 DJoins (w,v,G1) by A18, GLIB_000:def 14;

        v in ( the_Vertices_of G1) & w in ( the_Vertices_of G1) & f is total by A1;

        then v in ( dom f) & w in ( dom f) by FUNCT_2:def 1;

        then

        consider e2 be object such that

         A20: e2 DJoins ((f . w),(f . v),G2) by A1, A19;

        (f . v) in {(f . v)} & (f . w) in {(f . w)} by TARSKI:def 1;

        then e2 DSJoins ( {(f . w)}, {(f . v)},G2) by A20, GLIB_009: 7;

        then e2 in (G2 .edgesDBetween ( {(f . w)}, {(f . v)})) by GLIB_000:def 31;

        then

        consider e be object such that

         A21: (G2 .edgesDBetween ( {(f . w)}, {(f . v)})) = {e} by ZFMISC_1: 131;

        ( card (G1 .edgesDBetween ( {w}, {v}))) = 1 & ( card (G2 .edgesDBetween ( {(f . w)}, {(f . v)}))) = 1 by A17, A21, CARD_1: 30;

        hence ( card (G1 .edgesDBetween ( {w}, {v}))) = ( card (G2 .edgesDBetween ( {(f . w)}, {(f . v)})));

      end;

    end;

    definition

      let G1,G2 be non-Dmulti _Graph, f be PVertexMapping of G1, G2;

      :: original: Disomorphism

      redefine

      :: GLIB_011:def8

      attr f is Disomorphism means f is total one-to-one onto directed Dcontinuous;

      compatibility by Th9;

    end

    registration

      let G1,G2 be non-Dmulti _Graph;

      cluster total one-to-one onto directed Dcontinuous -> Disomorphism for PVertexMapping of G1, G2;

      coherence ;

    end

    registration

      let G be _Graph;

      cluster Disomorphism isomorphism for PVertexMapping of G, G;

      existence

      proof

        reconsider f = ( id ( the_Vertices_of G)) as PVertexMapping of G, G by Th5;

        take f;

        thus f is Disomorphism;

        thus f is isomorphism;

      end;

    end

    theorem :: GLIB_011:10

    for G be _Graph holds ( id ( the_Vertices_of G)) is Disomorphism isomorphism PVertexMapping of G, G

    proof

      let G be _Graph;

      reconsider f = ( id ( the_Vertices_of G)) as PVertexMapping of G, G by Th5;

      f is Disomorphism;

      hence thesis;

    end;

    definition

      let G1,G2 be _Graph, f be PVertexMapping of G1, G2;

      :: GLIB_011:def9

      attr f is invertible means f is one-to-one continuous;

    end

    registration

      let G1,G2 be _Graph;

      cluster invertible -> one-to-one continuous for PVertexMapping of G1, G2;

      coherence ;

      cluster one-to-one continuous -> invertible for PVertexMapping of G1, G2;

      coherence ;

      cluster isomorphism -> invertible for PVertexMapping of G1, G2;

      coherence ;

      cluster Disomorphism -> invertible for PVertexMapping of G1, G2;

      coherence ;

      cluster empty invertible for PVertexMapping of G1, G2;

      existence

      proof

        take the empty one-to-one continuous PVertexMapping of G1, G2;

        thus thesis;

      end;

    end

    registration

      let G1,G2 be loopless _Graph;

      cluster non empty directed invertible for PVertexMapping of G1, G2;

      existence

      proof

        take the non empty directed one-to-one continuous PVertexMapping of G1, G2;

        thus thesis;

      end;

    end

    registration

      let G1,G2 be non loopless _Graph;

      cluster non empty directed invertible for PVertexMapping of G1, G2;

      existence

      proof

        take the non empty directed one-to-one continuous PVertexMapping of G1, G2;

        thus thesis;

      end;

    end

    definition

      let G1,G2 be _Graph, f be invertible PVertexMapping of G1, G2;

      :: original: "

      redefine

      func f " -> PVertexMapping of G2, G1 ;

      coherence

      proof

        now

          let v,w,e be object;

          assume

           A1: v in ( dom (f " )) & w in ( dom (f " )) & e Joins (v,w,G2);

          then

           A2: v in ( rng f) & w in ( rng f) by FUNCT_1: 33;

          then

          consider v0 be object such that

           A3: v0 in ( dom f) & (f . v0) = v by FUNCT_1:def 3;

          consider w0 be object such that

           A4: w0 in ( dom f) & (f . w0) = w by A2, FUNCT_1:def 3;

          consider e0 be object such that

           A5: e0 Joins (v0,w0,G1) by A1, A3, A4, Th2;

          take e0;

          ((f " ) . v) = v0 & ((f " ) . w) = w0 by A3, A4, FUNCT_1: 34;

          hence e0 Joins (((f " ) . v),((f " ) . w),G1) by A5;

        end;

        hence thesis by Th1;

      end;

    end

    registration

      let G1,G2 be _Graph, f be invertible PVertexMapping of G1, G2;

      cluster (f " ) -> one-to-one continuous invertible;

      coherence

      proof

        let g be PVertexMapping of G2, G1;

        assume

         A1: g = (f " );

        hence

         A2: g is one-to-one;

        now

          let v,w,e9 be object;

          assume v in ( dom g);

          then v in ( rng f) by A1, FUNCT_1: 33;

          then

          consider v0 be object such that

           A3: v0 in ( dom f) & (f . v0) = v by FUNCT_1:def 3;

          assume w in ( dom g);

          then w in ( rng f) by A1, FUNCT_1: 33;

          then

          consider w0 be object such that

           A4: w0 in ( dom f) & (f . w0) = w by FUNCT_1:def 3;

          assume e9 Joins ((g . v),(g . w),G1);

          then e9 Joins (v0,(g . (f . w0)),G1) by A1, A3, A4, FUNCT_1: 34;

          then e9 Joins (v0,w0,G1) by A1, A4, FUNCT_1: 34;

          then

          consider e be object such that

           A5: e Joins ((f . v0),(f . w0),G2) by A3, A4, Th1;

          take e;

          thus e Joins (v,w,G2) by A3, A4, A5;

        end;

        hence g is continuous invertible by A2, Th2;

      end;

    end

    definition

      let G1,G2,G3 be _Graph;

      let f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3;

      :: original: *

      redefine

      func g * f -> PVertexMapping of G1, G3 ;

      coherence

      proof

        now

          let v,w,e be object;

          assume

           A1: v in ( dom (g * f)) & w in ( dom (g * f)) & e Joins (v,w,G1);

          then

           A2: v in ( dom f) & w in ( dom f) & (f . v) in ( dom g) & (f . w) in ( dom g) by FUNCT_1: 11;

          then

          consider e8 be object such that

           A3: e8 Joins ((f . v),(f . w),G2) by A1, Th1;

          consider e9 be object such that

           A4: e9 Joins ((g . (f . v)),(g . (f . w)),G3) by A2, A3, Th1;

          take e9;

          ((g * f) . v) = (g . (f . v)) & ((g * f) . w) = (g . (f . w)) by A1, FUNCT_1: 12;

          hence e9 Joins (((g * f) . v),((g * f) . w),G3) by A4;

        end;

        hence thesis by Th1;

      end;

    end

    theorem :: GLIB_011:11

    for G1,G2,G3 be _Graph holds for f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3 st f is continuous & g is continuous holds (g * f) is continuous

    proof

      let G1,G2,G3 be _Graph;

      let f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3;

      assume

       A1: f is continuous & g is continuous;

      now

        let v,w,e9 be object;

        assume

         A2: v in ( dom (g * f)) & w in ( dom (g * f)) & e9 Joins (((g * f) . v),((g * f) . w),G3);

        then e9 Joins ((g . (f . v)),((g * f) . w),G3) by FUNCT_1: 12;

        then

         A3: e9 Joins ((g . (f . v)),(g . (f . w)),G3) by A2, FUNCT_1: 12;

        (f . v) in ( dom g) & (f . w) in ( dom g) by A2, FUNCT_1: 11;

        then

        consider e8 be object such that

         A4: e8 Joins ((f . v),(f . w),G2) by A1, A3, Th2;

        v in ( dom f) & w in ( dom f) by A2, FUNCT_1: 11;

        then

        consider e be object such that

         A5: e Joins (v,w,G1) by A1, A4, Th2;

        take e;

        thus e Joins (v,w,G1) by A5;

      end;

      hence thesis by Th2;

    end;

    theorem :: GLIB_011:12

    for G1,G2,G3 be _Graph holds for f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3 st f is directed & g is directed holds (g * f) is directed

    proof

      let G1,G2,G3 be _Graph;

      let f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3;

      assume

       A1: f is directed & g is directed;

      now

        let v,w,e9 be object;

        assume

         A2: v in ( dom (g * f)) & w in ( dom (g * f)) & e9 DJoins (v,w,G1);

        then v in ( dom f) & w in ( dom f) by FUNCT_1: 11;

        then

        consider e8 be object such that

         A3: e8 DJoins ((f . v),(f . w),G2) by A1, A2;

        (f . v) in ( dom g) & (f . w) in ( dom g) by A2, FUNCT_1: 11;

        then

        consider e be object such that

         A4: e DJoins ((g . (f . v)),(g . (f . w)),G3) by A1, A3;

        take e;

        e DJoins (((g * f) . v),(g . (f . w)),G3) by A2, A4, FUNCT_1: 12;

        hence e DJoins (((g * f) . v),((g * f) . w),G3) by A2, FUNCT_1: 12;

      end;

      hence thesis;

    end;

    theorem :: GLIB_011:13

    for G1,G2,G3 be _Graph holds for f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3 st f is Dcontinuous & g is Dcontinuous holds (g * f) is Dcontinuous

    proof

      let G1,G2,G3 be _Graph;

      let f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3;

      assume

       A1: f is Dcontinuous & g is Dcontinuous;

      now

        let v,w,e9 be object;

        assume

         A2: v in ( dom (g * f)) & w in ( dom (g * f)) & e9 DJoins (((g * f) . v),((g * f) . w),G3);

        then e9 DJoins ((g . (f . v)),((g * f) . w),G3) by FUNCT_1: 12;

        then

         A3: e9 DJoins ((g . (f . v)),(g . (f . w)),G3) by A2, FUNCT_1: 12;

        (f . v) in ( dom g) & (f . w) in ( dom g) by A2, FUNCT_1: 11;

        then

        consider e8 be object such that

         A4: e8 DJoins ((f . v),(f . w),G2) by A1, A3;

        v in ( dom f) & w in ( dom f) by A2, FUNCT_1: 11;

        then

        consider e be object such that

         A5: e DJoins (v,w,G1) by A1, A4;

        take e;

        thus e DJoins (v,w,G1) by A5;

      end;

      hence thesis;

    end;

    theorem :: GLIB_011:14

    for G1,G2,G3 be _Graph holds for f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3 st f is isomorphism & g is isomorphism holds (g * f) is isomorphism

    proof

      let G1,G2,G3 be _Graph;

      let f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3;

      assume

       A1: f is isomorphism & g is isomorphism;

      hence (g * f) is total one-to-one onto by FUNCT_2: 27;

      let v,w be Vertex of G1;

      v in ( the_Vertices_of G1) & w in ( the_Vertices_of G1);

      then

       A2: v in ( dom f) & w in ( dom f) by A1, PARTFUN1:def 2;

      then

       A3: (f . v) in ( rng f) & (f . w) in ( rng f) by FUNCT_1: 3;

      

      thus ( card (G1 .edgesBetween ( {v}, {w}))) = ( card (G2 .edgesBetween ( {(f . v)}, {(f . w)}))) by A1

      .= ( card (G3 .edgesBetween ( {(g . (f . v))}, {(g . (f . w))}))) by A1, A3

      .= ( card (G3 .edgesBetween ( {((g * f) . v)}, {(g . (f . w))}))) by A2, FUNCT_1: 13

      .= ( card (G3 .edgesBetween ( {((g * f) . v)}, {((g * f) . w)}))) by A2, FUNCT_1: 13;

    end;

    theorem :: GLIB_011:15

    for G1,G2,G3 be _Graph holds for f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3 st f is Disomorphism & g is Disomorphism holds (g * f) is Disomorphism

    proof

      let G1,G2,G3 be _Graph;

      let f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3;

      assume

       A1: f is Disomorphism & g is Disomorphism;

      hence (g * f) is total one-to-one onto by FUNCT_2: 27;

      let v,w be Vertex of G1;

      v in ( the_Vertices_of G1) & w in ( the_Vertices_of G1);

      then

       A2: v in ( dom f) & w in ( dom f) by A1, PARTFUN1:def 2;

      then

       A3: (f . v) in ( rng f) & (f . w) in ( rng f) by FUNCT_1: 3;

      

      thus ( card (G1 .edgesDBetween ( {v}, {w}))) = ( card (G2 .edgesDBetween ( {(f . v)}, {(f . w)}))) by A1

      .= ( card (G3 .edgesDBetween ( {(g . (f . v))}, {(g . (f . w))}))) by A1, A3

      .= ( card (G3 .edgesDBetween ( {((g * f) . v)}, {(g . (f . w))}))) by A2, FUNCT_1: 13

      .= ( card (G3 .edgesDBetween ( {((g * f) . v)}, {((g * f) . w)}))) by A2, FUNCT_1: 13;

      

      thus ( card (G1 .edgesDBetween ( {w}, {v}))) = ( card (G2 .edgesDBetween ( {(f . w)}, {(f . v)}))) by A1

      .= ( card (G3 .edgesDBetween ( {(g . (f . w))}, {(g . (f . v))}))) by A1, A3

      .= ( card (G3 .edgesDBetween ( {((g * f) . w)}, {(g . (f . v))}))) by A2, FUNCT_1: 13

      .= ( card (G3 .edgesDBetween ( {((g * f) . w)}, {((g * f) . v)}))) by A2, FUNCT_1: 13;

    end;

    begin

    theorem :: GLIB_011:16

    

     Th16: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st for v,w be Vertex of G1 st v in ( dom (F _V )) & w in ( dom (F _V )) & (v,w) are_adjacent holds ex e be object st e in ( dom (F _E )) & e Joins (v,w,G1) holds (F _V ) is PVertexMapping of G1, G2

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: for v,w be Vertex of G1 st v in ( dom (F _V )) & w in ( dom (F _V )) & (v,w) are_adjacent holds ex e be object st e in ( dom (F _E )) & e Joins (v,w,G1);

      let v,w be Vertex of G1;

      assume

       A2: v in ( dom (F _V )) & w in ( dom (F _V )) & (v,w) are_adjacent ;

      then

      consider e be object such that

       A3: e in ( dom (F _E )) & e Joins (v,w,G1) by A1;

      

       A4: ((F _V ) /. v) = ((F _V ) . v) & ((F _V ) /. w) = ((F _V ) . w) by A2, PARTFUN1:def 6;

      ((F _E ) . e) Joins (((F _V ) . v),((F _V ) . w),G2) by A2, A3, GLIB_010: 4;

      hence (((F _V ) /. v),((F _V ) /. w)) are_adjacent by A4, CHORD:def 3;

    end;

    theorem :: GLIB_011:17

    

     Th17: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st ( dom (F _E )) = ( the_Edges_of G1) holds (F _V ) is PVertexMapping of G1, G2

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: ( dom (F _E )) = ( the_Edges_of G1);

      now

        let v,w be Vertex of G1;

        assume v in ( dom (F _V )) & w in ( dom (F _V )) & (v,w) are_adjacent ;

        then

        consider e be object such that

         A2: e Joins (v,w,G1) by CHORD:def 3;

        take e;

        thus e in ( dom (F _E )) by A1, A2, GLIB_000:def 13;

        thus e Joins (v,w,G1) by A2;

      end;

      hence thesis by Th16;

    end;

    theorem :: GLIB_011:18

    

     Th18: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is total holds (F _V ) is PVertexMapping of G1, G2

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume F is total;

      then ( dom (F _E )) = ( the_Edges_of G1) by GLIB_010:def 11;

      hence thesis by Th17;

    end;

    theorem :: GLIB_011:19

    

     Th19: for G1,G2 be _Graph, F be directed PGraphMapping of G1, G2 st for v,w be object st v in ( dom (F _V )) & w in ( dom (F _V )) & ex e be object st e DJoins (v,w,G1) holds ex e be object st e in ( dom (F _E )) & e DJoins (v,w,G1) holds (F _V ) is directed PVertexMapping of G1, G2

    proof

      let G1,G2 be _Graph, F be directed PGraphMapping of G1, G2;

      assume

       A1: for v,w be object st v in ( dom (F _V )) & w in ( dom (F _V )) & ex e be object st e DJoins (v,w,G1) holds ex e be object st e in ( dom (F _E )) & e DJoins (v,w,G1);

      now

        let v,w,e be object;

        assume

         A2: v in ( dom (F _V )) & w in ( dom (F _V )) & e Joins (v,w,G1);

        per cases by GLIB_000: 16;

          suppose e DJoins (v,w,G1);

          then

          consider e0 be object such that

           A3: e0 in ( dom (F _E )) & e0 DJoins (v,w,G1) by A1, A2;

          reconsider e9 = ((F _E ) . e0) as object;

          take e9;

          e0 Joins (v,w,G1) by A3, GLIB_000: 16;

          hence e9 Joins (((F _V ) . v),((F _V ) . w),G2) by A2, A3, GLIB_010: 4;

        end;

          suppose e DJoins (w,v,G1);

          then

          consider e0 be object such that

           A4: e0 in ( dom (F _E )) & e0 DJoins (w,v,G1) by A1, A2;

          reconsider e9 = ((F _E ) . e0) as object;

          take e9;

          e0 Joins (v,w,G1) by A4, GLIB_000: 16;

          hence e9 Joins (((F _V ) . v),((F _V ) . w),G2) by A2, A4, GLIB_010: 4;

        end;

      end;

      then

       A5: (F _V ) is PVertexMapping of G1, G2 by Th1;

      now

        let v,w,e be object;

        assume

         A6: v in ( dom (F _V )) & w in ( dom (F _V )) & e DJoins (v,w,G1);

        then

        consider e0 be object such that

         A7: e0 in ( dom (F _E )) & e0 DJoins (v,w,G1) by A1;

        reconsider e9 = ((F _E ) . e0) as object;

        take e9;

        thus e9 DJoins (((F _V ) . v),((F _V ) . w),G2) by A6, A7, GLIB_010:def 14;

      end;

      hence thesis by A5, Def2;

    end;

    theorem :: GLIB_011:20

    

     Th20: for G1,G2 be _Graph, F be directed PGraphMapping of G1, G2 st ( dom (F _E )) = ( the_Edges_of G1) holds (F _V ) is directed PVertexMapping of G1, G2

    proof

      let G1,G2 be _Graph, F be directed PGraphMapping of G1, G2;

      assume

       A1: ( dom (F _E )) = ( the_Edges_of G1);

      for v,w be object st v in ( dom (F _V )) & w in ( dom (F _V )) holds (ex e be object st e DJoins (v,w,G1)) implies (ex e be object st e in ( dom (F _E )) & e DJoins (v,w,G1)) by A1, GLIB_000:def 14;

      hence thesis by Th19;

    end;

    theorem :: GLIB_011:21

    

     Th21: for G1,G2 be _Graph, F be directed PGraphMapping of G1, G2 st F is total holds (F _V ) is directed PVertexMapping of G1, G2

    proof

      let G1,G2 be _Graph, F be directed PGraphMapping of G1, G2;

      assume F is total;

      then ( dom (F _E )) = ( the_Edges_of G1) by GLIB_010:def 11;

      hence thesis by Th20;

    end;

    theorem :: GLIB_011:22

    

     Th22: for G1,G2 be _Graph, F be semi-continuous PGraphMapping of G1, G2 st (F _V ) is PVertexMapping of G1, G2 & for v,w be Vertex of G1 st v in ( dom (F _V )) & w in ( dom (F _V )) & (((F _V ) /. v),((F _V ) /. w)) are_adjacent holds ex e9 be object st e9 in ( rng (F _E )) & e9 Joins (((F _V ) . v),((F _V ) . w),G2) holds (F _V ) is continuous PVertexMapping of G1, G2

    proof

      let G1,G2 be _Graph, F be semi-continuous PGraphMapping of G1, G2;

      assume that

       A1: (F _V ) is PVertexMapping of G1, G2 and

       A2: for v,w be Vertex of G1 st v in ( dom (F _V )) & w in ( dom (F _V )) & (((F _V ) /. v),((F _V ) /. w)) are_adjacent holds ex e9 be object st e9 in ( rng (F _E )) & e9 Joins (((F _V ) . v),((F _V ) . w),G2);

      reconsider f = (F _V ) as PVertexMapping of G1, G2 by A1;

      now

        let v,w,e9 be object;

        assume

         A3: v in ( dom f) & w in ( dom f) & e9 Joins ((f . v),(f . w),G2);

        then e9 Joins ((f /. v),(f . w),G2) by PARTFUN1:def 6;

        then e9 Joins ((f /. v),(f /. w),G2) by A3, PARTFUN1:def 6;

        then

        consider e8 be object such that

         A4: e8 in ( rng (F _E )) & e8 Joins ((f . v),(f . w),G2) by A2, A3, CHORD:def 3;

        consider e be object such that

         A5: e in ( dom (F _E )) & ((F _E ) . e) = e8 by A4, FUNCT_1:def 3;

        take e;

        thus e Joins (v,w,G1) by A3, A4, A5, GLIB_010:def 15;

      end;

      hence thesis by Th2;

    end;

    theorem :: GLIB_011:23

    

     Th23: for G1,G2 be _Graph, F be semi-continuous PGraphMapping of G1, G2 st ( dom (F _E )) = ( the_Edges_of G1) & ( rng (F _E )) = ( the_Edges_of G2) holds (F _V ) is continuous PVertexMapping of G1, G2

    proof

      let G1,G2 be _Graph, F be semi-continuous PGraphMapping of G1, G2;

      assume

       A1: ( dom (F _E )) = ( the_Edges_of G1) & ( rng (F _E )) = ( the_Edges_of G2);

      then

       A2: (F _V ) is PVertexMapping of G1, G2 by Th17;

      now

        let v,w be Vertex of G1;

        assume

         A3: v in ( dom (F _V )) & w in ( dom (F _V )) & (((F _V ) /. v),((F _V ) /. w)) are_adjacent ;

        then

        consider e be object such that

         A4: e Joins (((F _V ) /. v),((F _V ) /. w),G2) by CHORD:def 3;

        take e;

        thus e in ( rng (F _E )) by A1, A4, GLIB_000:def 13;

        e Joins (((F _V ) . v),((F _V ) /. w),G2) by A3, A4, PARTFUN1:def 6;

        hence e Joins (((F _V ) . v),((F _V ) . w),G2) by A3, PARTFUN1:def 6;

      end;

      hence thesis by A2, Th22;

    end;

    theorem :: GLIB_011:24

    for G1,G2 be _Graph, F be semi-continuous PGraphMapping of G1, G2 st F is total onto holds (F _V ) is continuous PVertexMapping of G1, G2

    proof

      let G1,G2 be _Graph, F be semi-continuous PGraphMapping of G1, G2;

      assume F is total onto;

      then ( dom (F _E )) = ( the_Edges_of G1) & ( rng (F _E )) = ( the_Edges_of G2) by GLIB_010:def 11, GLIB_010:def 12;

      hence thesis by Th23;

    end;

    

     Lm1: for x be object, f be Function st x in ( dom f) holds (f .: {x}) = {(f . x)}

    proof

      let x be object, f be Function;

      assume

       A1: x in ( dom f);

      

      thus (f .: {x}) = ( Im (f,x)) by RELAT_1:def 16

      .= {(f . x)} by A1, FUNCT_1: 59;

    end;

    theorem :: GLIB_011:25

    

     Th25: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is isomorphism holds ex f be PVertexMapping of G1, G2 st (F _V ) = f & f is isomorphism

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is isomorphism;

      then

      reconsider f = (F _V ) as PVertexMapping of G1, G2 by Th18;

      take f;

      thus (F _V ) = f;

      

       A2: ( dom f) = ( the_Vertices_of G1) by A1, GLIB_010:def 11;

      hence f is total by PARTFUN1:def 2;

      thus f is one-to-one by A1;

      ( rng f) = ( the_Vertices_of G2) by A1, GLIB_010:def 12;

      hence f is onto by FUNCT_2:def 3;

      let v,w be Vertex of G1;

      ( card (G1 .edgesBetween ( {v}, {w}))) = ( card (G2 .edgesBetween (((F _V ) .: {v}),((F _V ) .: {w})))) by A1, GLIB_010: 86

      .= ( card (G2 .edgesBetween (((F _V ) .: {v}), {((F _V ) . w)}))) by A2, Lm1

      .= ( card (G2 .edgesBetween ( {(f . v)}, {(f . w)}))) by A2, Lm1;

      hence thesis;

    end;

    theorem :: GLIB_011:26

    

     Th26: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is Disomorphism holds ex f be directed PVertexMapping of G1, G2 st (F _V ) = f & f is Disomorphism

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is Disomorphism;

      then

      reconsider f = (F _V ) as directed PVertexMapping of G1, G2 by Th21;

      take f;

      thus (F _V ) = f;

      

       A2: ( dom f) = ( the_Vertices_of G1) by A1, GLIB_010:def 11;

      hence f is total by PARTFUN1:def 2;

      thus f is one-to-one by A1;

      ( rng f) = ( the_Vertices_of G2) by A1, GLIB_010:def 12;

      hence f is onto by FUNCT_2:def 3;

      let v,w be Vertex of G1;

      

       A3: ( card (G1 .edgesDBetween ( {v}, {w}))) = ( card (G2 .edgesDBetween (((F _V ) .: {v}),((F _V ) .: {w})))) by A1, GLIB_010: 88

      .= ( card (G2 .edgesDBetween (((F _V ) .: {v}), {((F _V ) . w)}))) by A2, Lm1

      .= ( card (G2 .edgesDBetween ( {(f . v)}, {(f . w)}))) by A2, Lm1;

      ( card (G1 .edgesDBetween ( {w}, {v}))) = ( card (G2 .edgesDBetween (((F _V ) .: {w}),((F _V ) .: {v})))) by A1, GLIB_010: 88

      .= ( card (G2 .edgesDBetween (((F _V ) .: {w}), {((F _V ) . v)}))) by A2, Lm1

      .= ( card (G2 .edgesDBetween ( {(f . w)}, {(f . v)}))) by A2, Lm1;

      hence thesis by A3;

    end;

    theorem :: GLIB_011:27

    

     Th27: for G1,G2 be _Graph, f be PVertexMapping of G1, G2 holds for E1 be RepEdgeSelection of G1, E2 be RepEdgeSelection of G2 holds ex F be PGraphMapping of G1, G2 st (F _V ) = f & ( dom (F _E )) = (E1 /\ (G1 .edgesBetween ( dom f))) & ( rng (F _E )) c= (E2 /\ (G2 .edgesBetween ( rng f)))

    proof

      let G1,G2 be _Graph, f be PVertexMapping of G1, G2;

      let E1 be RepEdgeSelection of G1, E2 be RepEdgeSelection of G2;

      defpred P[ object, object] means ex v,w be object st v in ( dom f) & w in ( dom f) & $1 in E1 & $2 in E2 & $1 Joins (v,w,G1) & $2 Joins ((f . v),(f . w),G2);

      

       A1: for e1,e2,e3 be object st e1 in (E1 /\ (G1 .edgesBetween ( dom f))) & P[e1, e2] & P[e1, e3] holds e2 = e3

      proof

        let e1,e2,e3 be object;

        assume

         A2: e1 in (E1 /\ (G1 .edgesBetween ( dom f))) & P[e1, e2] & P[e1, e3];

        then

        consider v2,w2 be object such that

         A3: v2 in ( dom f) & w2 in ( dom f) & e1 in E1 & e2 in E2 & e1 Joins (v2,w2,G1) & e2 Joins ((f . v2),(f . w2),G2);

        consider v3,w3 be object such that

         A4: v3 in ( dom f) & w3 in ( dom f) & e1 in E1 & e3 in E2 & e1 Joins (v3,w3,G1) & e3 Joins ((f . v3),(f . w3),G2) by A2;

        v2 = v3 & w2 = w3 or v2 = w3 & w2 = v3 by A3, A4, GLIB_000: 15;

        then (f . v2) = (f . v3) & (f . w2) = (f . w3) or (f . v2) = (f . w3) & (f . w2) = (f . v3);

        then

         A5: e3 Joins ((f . v2),(f . w2),G2) by A4, GLIB_000: 14;

        then

        consider e0 be object such that e0 Joins ((f . v2),(f . w2),G2) & e0 in E2 and

         A6: for e9 be object st e9 Joins ((f . v2),(f . w2),G2) & e9 in E2 holds e9 = e0 by GLIB_009:def 5;

        e2 = e0 & e3 = e0 by A3, A4, A5, A6;

        hence e2 = e3;

      end;

      

       A7: for e1 be object st e1 in (E1 /\ (G1 .edgesBetween ( dom f))) holds ex e2 be object st P[e1, e2]

      proof

        let e1 be object;

        set v = (( the_Source_of G1) . e1), w = (( the_Target_of G1) . e1);

        assume

         A8: e1 in (E1 /\ (G1 .edgesBetween ( dom f)));

        then e1 in (G1 .edgesBetween ( dom f)) by XBOOLE_0:def 4;

        then

         A9: e1 in ( the_Edges_of G1) & v in ( dom f) & w in ( dom f) by GLIB_000: 31;

        then

         A10: e1 Joins (v,w,G1) by GLIB_000:def 13;

        then

        consider e0 be object such that

         A11: e0 Joins ((f . v),(f . w),G2) by A9, Th1;

        consider e2 be object such that

         A12: e2 Joins ((f . v),(f . w),G2) & e2 in E2 and for e9 be object st e9 Joins ((f . v),(f . w),G2) & e9 in E2 holds e9 = e2 by A11, GLIB_009:def 5;

        take e2, v, w;

        thus v in ( dom f) & w in ( dom f) & e1 in E1 by A8, A9, XBOOLE_0:def 4;

        thus e2 in E2 & e1 Joins (v,w,G1) & e2 Joins ((f . v),(f . w),G2) by A10, A12;

      end;

      consider g be Function such that

       A13: ( dom g) = (E1 /\ (G1 .edgesBetween ( dom f))) and

       A14: for e1 be object st e1 in (E1 /\ (G1 .edgesBetween ( dom f))) holds P[e1, (g . e1)] from FUNCT_1:sch 2( A1, A7);

      for y be object holds y in ( rng g) implies y in (E2 /\ (G2 .edgesBetween ( rng f)))

      proof

        let y be object;

        assume y in ( rng g);

        then

        consider x be object such that

         A15: x in ( dom g) & (g . x) = y by FUNCT_1:def 3;

        consider v,w be object such that

         A16: v in ( dom f) & w in ( dom f) & x in E1 & (g . x) in E2 and

         A17: x Joins (v,w,G1) & (g . x) Joins ((f . v),(f . w),G2) by A13, A14, A15;

        (f . v) in ( rng f) & (f . w) in ( rng f) by A16, FUNCT_1: 3;

        then (( the_Source_of G2) . y) in ( rng f) & (( the_Target_of G2) . y) in ( rng f) & y in ( the_Edges_of G2) by A15, A17, GLIB_000:def 13;

        then y in (G2 .edgesBetween ( rng f)) by GLIB_000: 31;

        hence y in (E2 /\ (G2 .edgesBetween ( rng f))) by A15, A16, XBOOLE_0:def 4;

      end;

      then

       A18: ( rng g) c= (E2 /\ (G2 .edgesBetween ( rng f))) by TARSKI:def 3;

      ( rng g) c= ( the_Edges_of G2) by A18, XBOOLE_1: 1;

      then

      reconsider g as PartFunc of ( the_Edges_of G1), ( the_Edges_of G2) by A13, RELSET_1: 4;

      now

        hereby

          let e be object;

          assume e in ( dom g);

          then

          consider v,w be object such that

           A19: v in ( dom f) & w in ( dom f) & e in E1 & (g . e) in E2 & e Joins (v,w,G1) & (g . e) Joins ((f . v),(f . w),G2) by A13, A14;

          thus (( the_Source_of G1) . e) in ( dom f) & (( the_Target_of G1) . e) in ( dom f) by A19, GLIB_000:def 13;

        end;

        let e,v,w be object;

        assume e in ( dom g) & v in ( dom f) & w in ( dom f);

        then

        consider v0,w0 be object such that

         A20: v0 in ( dom f) & w0 in ( dom f) & e in E1 & (g . e) in E2 & e Joins (v0,w0,G1) & (g . e) Joins ((f . v0),(f . w0),G2) by A13, A14;

        assume e Joins (v,w,G1);

        then v = v0 & w = w0 or v = w0 & w = v0 by A20, GLIB_000: 15;

        hence (g . e) Joins ((f . v),(f . w),G2) by A20, GLIB_000: 14;

      end;

      then

      reconsider F = [f, g] as PGraphMapping of G1, G2 by GLIB_010: 8;

      take F;

      thus thesis by A13, A18;

    end;

    definition

      let G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2;

      :: GLIB_011:def10

      func PVM2PGM (f) -> PGraphMapping of G1, G2 means

      : Def10: (it _V ) = f & ( dom (it _E )) = (G1 .edgesBetween ( dom f)) & ( rng (it _E )) c= (G2 .edgesBetween ( rng f));

      existence

      proof

        set E1 = the RepEdgeSelection of G1, E2 = the RepEdgeSelection of G2;

        consider F be PGraphMapping of G1, G2 such that

         A1: (F _V ) = f & ( dom (F _E )) = (E1 /\ (G1 .edgesBetween ( dom f))) & ( rng (F _E )) c= (E2 /\ (G2 .edgesBetween ( rng f))) by Th27;

        take F;

        thus (F _V ) = f by A1;

        

         A2: E1 = ( the_Edges_of G1) & E2 = ( the_Edges_of G2) by GLIB_009: 74;

        hence ( dom (F _E )) = (G1 .edgesBetween ( dom f)) by A1, XBOOLE_1: 28;

        thus ( rng (F _E )) c= (G2 .edgesBetween ( rng f)) by A1, A2, XBOOLE_1: 28;

      end;

      uniqueness by GLIB_010: 40;

    end

    theorem :: GLIB_011:28

    

     Th28: for G1,G2 be non-multi _Graph holds for f be PVertexMapping of G1, G2 holds (( PVM2PGM f) _V ) = f by Def10;

    registration

      let G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2;

      reduce (( PVM2PGM f) _V ) to f;

      reducibility by Th28;

    end

    theorem :: GLIB_011:29

    

     Th29: for G1,G2 be _Graph, f be directed PVertexMapping of G1, G2 holds for E1 be RepDEdgeSelection of G1, E2 be RepDEdgeSelection of G2 holds ex F be directed PGraphMapping of G1, G2 st (F _V ) = f & ( dom (F _E )) = (E1 /\ (G1 .edgesBetween ( dom f))) & ( rng (F _E )) c= (E2 /\ (G2 .edgesBetween ( rng f)))

    proof

      let G1,G2 be _Graph, f be directed PVertexMapping of G1, G2;

      let E1 be RepDEdgeSelection of G1, E2 be RepDEdgeSelection of G2;

      defpred P[ object, object] means ex v,w be object st v in ( dom f) & w in ( dom f) & $1 in E1 & $2 in E2 & $1 DJoins (v,w,G1) & $2 DJoins ((f . v),(f . w),G2);

      

       A1: for e1,e2,e3 be object st e1 in (E1 /\ (G1 .edgesBetween ( dom f))) & P[e1, e2] & P[e1, e3] holds e2 = e3

      proof

        let e1,e2,e3 be object;

        assume

         A2: e1 in (E1 /\ (G1 .edgesBetween ( dom f))) & P[e1, e2] & P[e1, e3];

        then

        consider v2,w2 be object such that

         A3: v2 in ( dom f) & w2 in ( dom f) & e1 in E1 & e2 in E2 & e1 DJoins (v2,w2,G1) & e2 DJoins ((f . v2),(f . w2),G2);

        consider v3,w3 be object such that

         A4: v3 in ( dom f) & w3 in ( dom f) & e1 in E1 & e3 in E2 & e1 DJoins (v3,w3,G1) & e3 DJoins ((f . v3),(f . w3),G2) by A2;

        

         A5: v2 = v3 & w2 = w3 by A3, A4, GLIB_009: 6;

        then

        consider e0 be object such that e0 DJoins ((f . v2),(f . w2),G2) & e0 in E2 and

         A6: for e9 be object st e9 DJoins ((f . v2),(f . w2),G2) & e9 in E2 holds e9 = e0 by A4, GLIB_009:def 6;

        e2 = e0 & e3 = e0 by A3, A4, A5, A6;

        hence e2 = e3;

      end;

      

       A7: for e1 be object st e1 in (E1 /\ (G1 .edgesBetween ( dom f))) holds ex e2 be object st P[e1, e2]

      proof

        let e1 be object;

        set v = (( the_Source_of G1) . e1), w = (( the_Target_of G1) . e1);

        assume

         A8: e1 in (E1 /\ (G1 .edgesBetween ( dom f)));

        then e1 in (G1 .edgesBetween ( dom f)) by XBOOLE_0:def 4;

        then

         A9: e1 in ( the_Edges_of G1) & v in ( dom f) & w in ( dom f) by GLIB_000: 31;

        then

         A10: e1 DJoins (v,w,G1) by GLIB_000:def 14;

        then

        consider e0 be object such that

         A11: e0 DJoins ((f . v),(f . w),G2) by A9, Def2;

        consider e2 be object such that

         A12: e2 DJoins ((f . v),(f . w),G2) & e2 in E2 and for e9 be object st e9 DJoins ((f . v),(f . w),G2) & e9 in E2 holds e9 = e2 by A11, GLIB_009:def 6;

        take e2, v, w;

        thus v in ( dom f) & w in ( dom f) & e1 in E1 by A8, A9, XBOOLE_0:def 4;

        thus e2 in E2 & e1 DJoins (v,w,G1) & e2 DJoins ((f . v),(f . w),G2) by A10, A12;

      end;

      consider g be Function such that

       A13: ( dom g) = (E1 /\ (G1 .edgesBetween ( dom f))) and

       A14: for e1 be object st e1 in (E1 /\ (G1 .edgesBetween ( dom f))) holds P[e1, (g . e1)] from FUNCT_1:sch 2( A1, A7);

      for y be object holds y in ( rng g) implies y in (E2 /\ (G2 .edgesBetween ( rng f)))

      proof

        let y be object;

        assume y in ( rng g);

        then

        consider x be object such that

         A15: x in ( dom g) & (g . x) = y by FUNCT_1:def 3;

        consider v,w be object such that

         A16: v in ( dom f) & w in ( dom f) & x in E1 & (g . x) in E2 and

         A17: x DJoins (v,w,G1) & (g . x) DJoins ((f . v),(f . w),G2) by A13, A14, A15;

        (f . v) in ( rng f) & (f . w) in ( rng f) by A16, FUNCT_1: 3;

        then (( the_Source_of G2) . y) in ( rng f) & (( the_Target_of G2) . y) in ( rng f) & y in ( the_Edges_of G2) by A15, A17, GLIB_000:def 14;

        then y in (G2 .edgesBetween ( rng f)) by GLIB_000: 31;

        hence y in (E2 /\ (G2 .edgesBetween ( rng f))) by A15, A16, XBOOLE_0:def 4;

      end;

      then

       A18: ( rng g) c= (E2 /\ (G2 .edgesBetween ( rng f))) by TARSKI:def 3;

      ( rng g) c= ( the_Edges_of G2) by A18, XBOOLE_1: 1;

      then

      reconsider g as PartFunc of ( the_Edges_of G1), ( the_Edges_of G2) by A13, RELSET_1: 4;

      now

        hereby

          let e be object;

          assume e in ( dom g);

          then

          consider v,w be object such that

           A19: v in ( dom f) & w in ( dom f) & e in E1 & (g . e) in E2 & e DJoins (v,w,G1) & (g . e) DJoins ((f . v),(f . w),G2) by A13, A14;

          thus (( the_Source_of G1) . e) in ( dom f) & (( the_Target_of G1) . e) in ( dom f) by A19, GLIB_000:def 14;

        end;

        let e,v,w be object;

        assume e in ( dom g) & v in ( dom f) & w in ( dom f);

        then

        consider v0,w0 be object such that v0 in ( dom f) & w0 in ( dom f) & e in E1 & (g . e) in E2 and

         A20: e DJoins (v0,w0,G1) & (g . e) DJoins ((f . v0),(f . w0),G2) by A13, A14;

        assume e DJoins (v,w,G1);

        then v = v0 & w = w0 by A20, GLIB_009: 6;

        hence (g . e) DJoins ((f . v),(f . w),G2) by A20;

      end;

      then

      reconsider F = [f, g] as directed PGraphMapping of G1, G2 by GLIB_010: 30;

      take F;

      thus thesis by A13, A18;

    end;

    definition

      let G1,G2 be non-Dmulti _Graph;

      let f be directed PVertexMapping of G1, G2;

      :: GLIB_011:def11

      func DPVM2PGM (f) -> directed PGraphMapping of G1, G2 means

      : Def11: (it _V ) = f & ( dom (it _E )) = (G1 .edgesBetween ( dom f)) & ( rng (it _E )) c= (G2 .edgesBetween ( rng f));

      existence

      proof

        set E1 = the RepDEdgeSelection of G1, E2 = the RepDEdgeSelection of G2;

        consider F be directed PGraphMapping of G1, G2 such that

         A1: (F _V ) = f & ( dom (F _E )) = (E1 /\ (G1 .edgesBetween ( dom f))) & ( rng (F _E )) c= (E2 /\ (G2 .edgesBetween ( rng f))) by Th29;

        take F;

        thus (F _V ) = f by A1;

        

         A2: E1 = ( the_Edges_of G1) & E2 = ( the_Edges_of G2) by GLIB_009: 76;

        hence ( dom (F _E )) = (G1 .edgesBetween ( dom f)) by A1, XBOOLE_1: 28;

        thus ( rng (F _E )) c= (G2 .edgesBetween ( rng f)) by A1, A2, XBOOLE_1: 28;

      end;

      uniqueness by GLIB_010: 41;

    end

    theorem :: GLIB_011:30

    

     Th30: for G1,G2 be non-Dmulti _Graph holds for f be directed PVertexMapping of G1, G2 holds (( DPVM2PGM f) _V ) = f by Def11;

    registration

      let G1,G2 be non-Dmulti _Graph;

      let f be directed PVertexMapping of G1, G2;

      reduce (( DPVM2PGM f) _V ) to f;

      reducibility by Th30;

    end

    theorem :: GLIB_011:31

    for G1,G2 be non-multi _Graph holds for f be directed PVertexMapping of G1, G2 holds ( PVM2PGM f) = ( DPVM2PGM f)

    proof

      let G1,G2 be non-multi _Graph;

      let f be directed PVertexMapping of G1, G2;

      

       A1: (( PVM2PGM f) _V ) = f & (( DPVM2PGM f) _V ) = f;

      ( dom (( PVM2PGM f) _E )) = (G1 .edgesBetween ( dom f)) & ( dom (( DPVM2PGM f) _E )) = (G1 .edgesBetween ( dom f)) by Def10, Def11;

      hence thesis by A1, GLIB_010: 40;

    end;

    theorem :: GLIB_011:32

    

     Th32: for G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2 st f is total holds ( PVM2PGM f) is total

    proof

      let G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2;

      assume f is total;

      then

       A1: ( dom f) = ( the_Vertices_of G1) by PARTFUN1:def 2;

      

       A2: ( dom (( PVM2PGM f) _E )) = (G1 .edgesBetween ( dom f)) by Def10

      .= ( the_Edges_of G1) by A1, GLIB_000: 34;

      (( PVM2PGM f) _V ) = f;

      hence thesis by A1, A2, GLIB_010:def 11;

    end;

    theorem :: GLIB_011:33

    

     Th33: for G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2 st f is total holds ( DPVM2PGM f) is total

    proof

      let G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2;

      assume f is total;

      then

       A1: ( dom f) = ( the_Vertices_of G1) by PARTFUN1:def 2;

      

       A2: ( dom (( DPVM2PGM f) _E )) = (G1 .edgesBetween ( dom f)) by Def11

      .= ( the_Edges_of G1) by A1, GLIB_000: 34;

      (( DPVM2PGM f) _V ) = f;

      hence thesis by A1, A2, GLIB_010:def 11;

    end;

    theorem :: GLIB_011:34

    

     Th34: for G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2 st f is one-to-one holds ( PVM2PGM f) is one-to-one

    proof

      let G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2;

      assume

       A1: f is one-to-one;

      then

       A2: (( PVM2PGM f) _V ) is one-to-one;

      set g = (( PVM2PGM f) _E );

      for x1,x2 be object st x1 in ( dom g) & x2 in ( dom g) & (g . x1) = (g . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        set v1 = (( the_Source_of G1) . x1), w1 = (( the_Target_of G1) . x1), v2 = (( the_Source_of G1) . x2), w2 = (( the_Target_of G1) . x2);

        assume

         A3: x1 in ( dom g) & x2 in ( dom g) & (g . x1) = (g . x2);

        then x1 in (G1 .edgesBetween ( dom f)) by Def10;

        then

         A4: x1 in ( the_Edges_of G1) & v1 in ( dom f) & w1 in ( dom f) by GLIB_000: 31;

        then

         A5: x1 Joins (v1,w1,G1) by GLIB_000:def 13;

        then (g . x1) Joins (((( PVM2PGM f) _V ) . v1),((( PVM2PGM f) _V ) . w1),G2) by A3, A4, GLIB_010: 4;

        then

         A6: (g . x1) Joins ((f . v1),(f . w1),G2);

        x2 in (G1 .edgesBetween ( dom f)) by A3, Def10;

        then

         A7: x2 in ( the_Edges_of G1) & v2 in ( dom f) & w2 in ( dom f) by GLIB_000: 31;

        then

         A8: x2 Joins (v2,w2,G1) by GLIB_000:def 13;

        then (g . x2) Joins (((( PVM2PGM f) _V ) . v2),((( PVM2PGM f) _V ) . w2),G2) by A3, A7, GLIB_010: 4;

        per cases by A3, A6, GLIB_000: 15;

          suppose (f . v1) = (f . v2) & (f . w1) = (f . w2);

          then v1 = v2 & w1 = w2 by A1, A4, A7, FUNCT_1:def 4;

          hence x1 = x2 by A5, A8, GLIB_000:def 20;

        end;

          suppose (f . v1) = (f . w2) & (f . w1) = (f . v2);

          then v1 = w2 & w1 = v2 by A1, A4, A7, FUNCT_1:def 4;

          then x2 Joins (v1,w1,G1) by A8, GLIB_000: 14;

          hence x1 = x2 by A5, GLIB_000:def 20;

        end;

      end;

      then g is one-to-one by FUNCT_1:def 4;

      hence thesis by A2, GLIB_010:def 13;

    end;

    theorem :: GLIB_011:35

    

     Th35: for G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2 st f is one-to-one holds ( DPVM2PGM f) is one-to-one

    proof

      let G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2;

      assume

       A1: f is one-to-one;

      then

       A2: (( DPVM2PGM f) _V ) is one-to-one;

      set g = (( DPVM2PGM f) _E );

      for x1,x2 be object st x1 in ( dom g) & x2 in ( dom g) & (g . x1) = (g . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        set v1 = (( the_Source_of G1) . x1), w1 = (( the_Target_of G1) . x1), v2 = (( the_Source_of G1) . x2), w2 = (( the_Target_of G1) . x2);

        assume

         A3: x1 in ( dom g) & x2 in ( dom g) & (g . x1) = (g . x2);

        then x1 in (G1 .edgesBetween ( dom f)) by Def11;

        then

         A4: x1 in ( the_Edges_of G1) & v1 in ( dom f) & w1 in ( dom f) by GLIB_000: 31;

        then

         A5: x1 DJoins (v1,w1,G1) by GLIB_000:def 14;

        then (g . x1) DJoins (((( DPVM2PGM f) _V ) . v1),((( DPVM2PGM f) _V ) . w1),G2) by A3, A4, GLIB_010:def 14;

        then

         A6: (g . x1) DJoins ((f . v1),(f . w1),G2);

        x2 in (G1 .edgesBetween ( dom f)) by A3, Def11;

        then

         A7: x2 in ( the_Edges_of G1) & v2 in ( dom f) & w2 in ( dom f) by GLIB_000: 31;

        then

         A8: x2 DJoins (v2,w2,G1) by GLIB_000:def 14;

        then (g . x2) DJoins (((( DPVM2PGM f) _V ) . v2),((( DPVM2PGM f) _V ) . w2),G2) by A3, A7, GLIB_010:def 14;

        then (f . v1) = (f . v2) & (f . w1) = (f . w2) by A3, A6, GLIB_009: 6;

        then v1 = v2 & w1 = w2 by A1, A4, A7, FUNCT_1:def 4;

        hence x1 = x2 by A5, A8, GLIB_000:def 21;

      end;

      then g is one-to-one by FUNCT_1:def 4;

      hence thesis by A2, GLIB_010:def 13;

    end;

    theorem :: GLIB_011:36

    

     Th36: for G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2 st f is onto continuous holds ( PVM2PGM f) is onto

    proof

      let G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2;

      assume

       A1: f is onto continuous;

      then

       A2: ( rng (( PVM2PGM f) _V )) = ( the_Vertices_of G2) by FUNCT_2:def 3;

      set g = (( PVM2PGM f) _E );

      for e be object st e in ( the_Edges_of G2) holds e in ( rng g)

      proof

        let e be object;

        set v2 = (( the_Source_of G2) . e), w2 = (( the_Target_of G2) . e);

        assume e in ( the_Edges_of G2);

        then e in (G2 .edgesBetween ( the_Vertices_of G2)) by GLIB_000: 34;

        then e in (G2 .edgesBetween ( rng f)) by A1, FUNCT_2:def 3;

        then

         A3: e in ( the_Edges_of G2) & v2 in ( rng f) & w2 in ( rng f) by GLIB_000: 31;

        consider v1 be object such that

         A4: v1 in ( dom f) & (f . v1) = v2 by A3, FUNCT_1:def 3;

        consider w1 be object such that

         A5: w1 in ( dom f) & (f . w1) = w2 by A3, FUNCT_1:def 3;

        

         A6: e Joins ((f . v1),(f . w1),G2) by A3, A4, A5, GLIB_000:def 13;

        then

        consider e0 be object such that

         A7: e0 Joins (v1,w1,G1) by A1, A4, A5, Th2;

        e0 in (G1 .edgesBetween ( dom f)) by A4, A5, A7, GLIB_000: 32;

        then

         A8: e0 in ( dom g) by Def10;

        then (g . e0) Joins (((( PVM2PGM f) _V ) . v1),((( PVM2PGM f) _V ) . w1),G2) by A4, A5, A7, GLIB_010: 4;

        then (g . e0) = e by A6, GLIB_000:def 20;

        hence e in ( rng g) by A8, FUNCT_1:def 3;

      end;

      then ( the_Edges_of G2) c= ( rng g) by TARSKI:def 3;

      then ( rng g) = ( the_Edges_of G2) by XBOOLE_0:def 10;

      hence thesis by A2, GLIB_010:def 12;

    end;

    theorem :: GLIB_011:37

    

     Th37: for G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2 st f is onto Dcontinuous holds ( DPVM2PGM f) is onto

    proof

      let G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2;

      assume

       A1: f is onto Dcontinuous;

      then

       A2: ( rng (( DPVM2PGM f) _V )) = ( the_Vertices_of G2) by FUNCT_2:def 3;

      set g = (( DPVM2PGM f) _E );

      for e be object st e in ( the_Edges_of G2) holds e in ( rng g)

      proof

        let e be object;

        set v2 = (( the_Source_of G2) . e), w2 = (( the_Target_of G2) . e);

        assume e in ( the_Edges_of G2);

        then e in (G2 .edgesBetween ( the_Vertices_of G2)) by GLIB_000: 34;

        then e in (G2 .edgesBetween ( rng f)) by A1, FUNCT_2:def 3;

        then

         A3: e in ( the_Edges_of G2) & v2 in ( rng f) & w2 in ( rng f) by GLIB_000: 31;

        consider v1 be object such that

         A4: v1 in ( dom f) & (f . v1) = v2 by A3, FUNCT_1:def 3;

        consider w1 be object such that

         A5: w1 in ( dom f) & (f . w1) = w2 by A3, FUNCT_1:def 3;

        e DJoins (v2,w2,G2) by A3, GLIB_000:def 14;

        then

         A6: e DJoins ((f . v1),(f . w1),G2) by A4, A5;

        then

        consider e0 be object such that

         A7: e0 DJoins (v1,w1,G1) by A1, A4, A5;

        e0 Joins (v1,w1,G1) by A7, GLIB_000: 16;

        then e0 in (G1 .edgesBetween ( dom f)) by A4, A5, GLIB_000: 32;

        then

         A8: e0 in ( dom g) by Def11;

        then (g . e0) DJoins (((( DPVM2PGM f) _V ) . v1),((( DPVM2PGM f) _V ) . w1),G2) by A4, A5, A7, GLIB_010:def 14;

        then (g . e0) = e by A6, GLIB_000:def 21;

        hence e in ( rng g) by A8, FUNCT_1:def 3;

      end;

      then ( the_Edges_of G2) c= ( rng g) by TARSKI:def 3;

      then ( rng g) = ( the_Edges_of G2) by XBOOLE_0:def 10;

      hence thesis by A2, GLIB_010:def 12;

    end;

    theorem :: GLIB_011:38

    for G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2 st f is continuous one-to-one holds ( PVM2PGM f) is semi-continuous

    proof

      let G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2;

      assume

       A1: f is continuous one-to-one;

      set g = (( PVM2PGM f) _E );

      now

        let e,v,w be object;

        assume

         A2: e in ( dom g) & v in ( dom (( PVM2PGM f) _V )) & w in ( dom (( PVM2PGM f) _V ));

        assume

         A3: (g . e) Joins (((( PVM2PGM f) _V ) . v),((( PVM2PGM f) _V ) . w),G2);

        then (g . e) Joins ((f . v),(f . w),G2);

        then

        consider e0 be object such that

         A4: e0 Joins (v,w,G1) by A1, A2, Th2;

        e0 in (G1 .edgesBetween ( dom f)) by A2, A4, GLIB_000: 32;

        then

         A5: e0 in ( dom g) by Def10;

        then (g . e0) Joins (((( PVM2PGM f) _V ) . v),((( PVM2PGM f) _V ) . w),G2) by A2, A4, GLIB_010: 4;

        then

         A6: (g . e0) = (g . e) by A3, GLIB_000:def 20;

        ( PVM2PGM f) is one-to-one by A1, Th34;

        hence e Joins (v,w,G1) by A2, A4, A5, A6, FUNCT_1:def 4;

      end;

      hence thesis by GLIB_010:def 15;

    end;

    theorem :: GLIB_011:39

    

     Th39: for G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2 st f is continuous holds ( PVM2PGM f) is continuous

    proof

      let G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2;

      assume

       A1: f is continuous;

      now

        let e9,v,w be object;

        assume

         A2: v in ( dom (( PVM2PGM f) _V )) & w in ( dom (( PVM2PGM f) _V ));

        assume

         A3: e9 Joins (((( PVM2PGM f) _V ) . v),((( PVM2PGM f) _V ) . w),G2);

        then

        consider e be object such that

         A4: e Joins (v,w,G1) by A1, A2, Th2;

        take e;

        thus e Joins (v,w,G1) by A4;

        e in (G1 .edgesBetween ( dom (( PVM2PGM f) _V ))) by A2, A4, GLIB_000: 32;

        hence e in ( dom (( PVM2PGM f) _E )) by Def10;

        then ((( PVM2PGM f) _E ) . e) Joins (((( PVM2PGM f) _V ) . v),((( PVM2PGM f) _V ) . w),G2) by A2, A4, GLIB_010: 4;

        hence ((( PVM2PGM f) _E ) . e) = e9 by A3, GLIB_000:def 20;

      end;

      hence thesis by GLIB_010:def 16;

    end;

    theorem :: GLIB_011:40

    for G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2 st f is one-to-one holds ( DPVM2PGM f) is semi-Dcontinuous semi-continuous

    proof

      let G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2;

      assume f is one-to-one;

      then ( DPVM2PGM f) is one-to-one by Th35;

      hence thesis;

    end;

    theorem :: GLIB_011:41

    

     Th41: for G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2 st f is Dcontinuous holds ( DPVM2PGM f) is Dcontinuous

    proof

      let G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2;

      assume

       A1: f is Dcontinuous;

      now

        let e9,v,w be object;

        assume

         A2: v in ( dom (( DPVM2PGM f) _V )) & w in ( dom (( DPVM2PGM f) _V ));

        then

        reconsider v0 = v, w0 = w as Vertex of G1;

        assume

         A3: e9 DJoins (((( DPVM2PGM f) _V ) . v),((( DPVM2PGM f) _V ) . w),G2);

        then

        consider e be object such that

         A4: e DJoins (v,w,G1) by A1, A2;

        take e;

        thus e DJoins (v,w,G1) by A4;

        e Joins (v,w,G1) by A4, GLIB_000: 16;

        then e in (G1 .edgesBetween ( dom (( DPVM2PGM f) _V ))) by A2, GLIB_000: 32;

        hence e in ( dom (( DPVM2PGM f) _E )) by Def11;

        then ((( DPVM2PGM f) _E ) . e) DJoins (((( DPVM2PGM f) _V ) . v),((( DPVM2PGM f) _V ) . w),G2) by A2, A4, GLIB_010:def 14;

        hence ((( DPVM2PGM f) _E ) . e) = e9 by A3, GLIB_000:def 21;

      end;

      hence thesis by GLIB_010:def 18;

    end;

    theorem :: GLIB_011:42

    for G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2 st f is one-to-one holds ( PVM2PGM f) is one-to-one by Th34;

    theorem :: GLIB_011:43

    for G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2 st f is one-to-one holds ( DPVM2PGM f) is one-to-one by Th35;

    theorem :: GLIB_011:44

    for G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2 st f is total one-to-one holds ( PVM2PGM f) is weak_SG-embedding

    proof

      let G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2;

      assume f is total one-to-one;

      then ( PVM2PGM f) is total one-to-one by Th32, Th34;

      hence thesis;

    end;

    theorem :: GLIB_011:45

    for G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2 st f is total one-to-one holds ( DPVM2PGM f) is weak_SG-embedding

    proof

      let G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2;

      assume f is total one-to-one;

      then ( DPVM2PGM f) is total one-to-one by Th33, Th35;

      hence thesis;

    end;

    theorem :: GLIB_011:46

    for G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2 st f is total one-to-one continuous holds ( PVM2PGM f) is strong_SG-embedding

    proof

      let G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2;

      assume f is total one-to-one continuous;

      then ( PVM2PGM f) is total one-to-one continuous by Th32, Th34, Th39;

      hence thesis;

    end;

    theorem :: GLIB_011:47

    

     Th47: for G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2 st f is isomorphism holds ( PVM2PGM f) is isomorphism

    proof

      let G1,G2 be non-multi _Graph, f be PVertexMapping of G1, G2;

      assume f is isomorphism;

      then ( PVM2PGM f) is total one-to-one onto by Th32, Th34, Th36;

      hence thesis;

    end;

    theorem :: GLIB_011:48

    

     Th48: for G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2 st f is Disomorphism holds ( DPVM2PGM f) is Disomorphism

    proof

      let G1,G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2;

      assume f is Disomorphism;

      then ( DPVM2PGM f) is total one-to-one onto Dcontinuous by Th33, Th35, Th37, Th41;

      hence thesis;

    end;

    theorem :: GLIB_011:49

    for G1,G2 be non-multi _Graph holds G2 is G1 -isomorphic iff ex f be PVertexMapping of G1, G2 st f is isomorphism

    proof

      let G1,G2 be non-multi _Graph;

      hereby

        assume G2 is G1 -isomorphic;

        then

        consider F be PGraphMapping of G1, G2 such that

         A1: F is isomorphism by GLIB_010:def 23;

        consider f be PVertexMapping of G1, G2 such that

         A2: (F _V ) = f & f is isomorphism by A1, Th25;

        take f;

        thus f is isomorphism by A2;

      end;

      given f be PVertexMapping of G1, G2 such that

       A3: f is isomorphism;

      ( PVM2PGM f) is isomorphism by A3, Th47;

      hence thesis by GLIB_010:def 23;

    end;

    theorem :: GLIB_011:50

    for G1,G2 be non-Dmulti _Graph holds G2 is G1 -Disomorphic iff ex f be directed PVertexMapping of G1, G2 st f is Disomorphism

    proof

      let G1,G2 be non-Dmulti _Graph;

      hereby

        assume G2 is G1 -Disomorphic;

        then

        consider F be PGraphMapping of G1, G2 such that

         A1: F is Disomorphism by GLIB_010:def 24;

        consider f be directed PVertexMapping of G1, G2 such that

         A2: (F _V ) = f & f is Disomorphism by A1, Th26;

        take f;

        thus f is Disomorphism by A2;

      end;

      given f be directed PVertexMapping of G1, G2 such that

       A3: f is Disomorphism;

      ( DPVM2PGM f) is Disomorphism by A3, Th48;

      hence thesis by GLIB_010:def 24;

    end;