let G be _Graph; :: thesis: for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G ex F being PGraphMapping of G, replaceVerticesEdges (V,E) st
( F _V = V & F _E = E & F is Disomorphism )
let V be non empty one-to-one ManySortedSet of the_Vertices_of G; :: thesis: for E being one-to-one ManySortedSet of the_Edges_of G ex F being PGraphMapping of G, replaceVerticesEdges (V,E) st
( F _V = V & F _E = E & F is Disomorphism )
let E be one-to-one ManySortedSet of the_Edges_of G; :: thesis: ex F being PGraphMapping of G, replaceVerticesEdges (V,E) st
( F _V = V & F _E = E & F is Disomorphism )
( the_Vertices_of (replaceVerticesEdges (V,E)) = rng V & the_Vertices_of G = dom V ) by Th1, PARTFUN1:def 2;
then reconsider f = V as Function of (the_Vertices_of G),(the_Vertices_of (replaceVerticesEdges (V,E))) by FUNCT_2:1;
( the_Edges_of (replaceVerticesEdges (V,E)) = rng E & the_Edges_of G = dom E ) by Th1, PARTFUN1:def 2;
then reconsider g = E as Function of (the_Edges_of G),(the_Edges_of (replaceVerticesEdges (V,E))) by FUNCT_2:1;

now :: thesis: ( ( for e being object st e in dom g holds
( (the_Source_of G) . e in dom f & (the_Target_of G) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e DJoins v,w,G holds
g . e DJoins f . v,f . w, replaceVerticesEdges (V,E) ) )

hereby :: thesis: for e, v, w being object st e in dom g & v in dom f & w in dom f & e DJoins v,w,G holds
g . e DJoins f . v,f . w, replaceVerticesEdges (V,E)

let e be object ; :: thesis: ( e in dom g implies ( (the_Source_of G) . e in dom f & (the_Target_of G) . e in dom f ) )
set v = (the_Source_of G) . e;
set w = (the_Target_of G) . e;
assume e in dom g ; :: thesis: ( (the_Source_of G) . e in dom f & (the_Target_of G) . e in dom f )
then A1: e Joins (the_Source_of G) . e,(the_Target_of G) . e,G by GLIB_000:def 13;
dom f = the_Vertices_of G by PARTFUN1:def 2;
hence ( (the_Source_of G) . e in dom f & (the_Target_of G) . e in dom f ) by A1, GLIB_000:13; :: thesis: verum

end;

let e, v, w be object ; :: thesis: ( e in dom g & v in dom f & w in dom f & e DJoins v,w,G implies g . e DJoins f . v,f . w, replaceVerticesEdges (V,E) )
assume ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( e DJoins v,w,G implies g . e DJoins f . v,f . w, replaceVerticesEdges (V,E) )
assume e DJoins v,w,G ; :: thesis: g . e DJoins f . v,f . w, replaceVerticesEdges (V,E)
hence g . e DJoins f . v,f . w, replaceVerticesEdges (V,E) by Th4; :: thesis: verum

end;

then reconsider F = [f,g] as directed PGraphMapping of G, replaceVerticesEdges (V,E) by GLIB_010:30;
take F ; :: thesis: ( F _V = V & F _E = E & F is Disomorphism )
( the_Vertices_of G = dom (F _V) & the_Edges_of G = dom (F _E) ) by PARTFUN1:def 2;
then A2: F is total by GLIB_010:def 11;
( the_Vertices_of (replaceVerticesEdges (V,E)) = rng (F _V) & the_Edges_of (replaceVerticesEdges (V,E)) = rng (F _E) ) by Th1;
then A3: F is onto by GLIB_010:def 12;
( F _V is one-to-one & F _E is one-to-one ) ;
then F is one-to-one by GLIB_010:def 13;
hence ( F _V = V & F _E = E & F is Disomorphism ) by A2, A3; :: thesis: verum