let G1, G2 be _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2
for V2 being non empty Subset of (the_Vertices_of (rng F))
for H being inducedSubgraph of (rng F),V2 st G1 .edgesBetween ((F _V) " (the_Vertices_of H)) c= dom (F _E) holds
(F _E) " (the_Edges_of H) = G1 .edgesBetween ((F _V) " (the_Vertices_of H))
let F be non empty PGraphMapping of G1,G2; :: thesis: for V2 being non empty Subset of (the_Vertices_of (rng F))
for H being inducedSubgraph of (rng F),V2 st G1 .edgesBetween ((F _V) " (the_Vertices_of H)) c= dom (F _E) holds
(F _E) " (the_Edges_of H) = G1 .edgesBetween ((F _V) " (the_Vertices_of H))
let V2 be non empty Subset of (the_Vertices_of (rng F)); :: thesis: for H being inducedSubgraph of (rng F),V2 st G1 .edgesBetween ((F _V) " (the_Vertices_of H)) c= dom (F _E) holds
(F _E) " (the_Edges_of H) = G1 .edgesBetween ((F _V) " (the_Vertices_of H))
let H be inducedSubgraph of (rng F),V2; :: thesis: ( G1 .edgesBetween ((F _V) " (the_Vertices_of H)) c= dom (F _E) implies (F _E) " (the_Edges_of H) = G1 .edgesBetween ((F _V) " (the_Vertices_of H)) )
assume A1: G1 .edgesBetween ((F _V) " (the_Vertices_of H)) c= dom (F _E) ; :: thesis: (F _E) " (the_Edges_of H) = G1 .edgesBetween ((F _V) " (the_Vertices_of H))
H is Subgraph of G2 by GLIB_000:43;
then A2: (F _E) " (the_Edges_of H) c= G1 .edgesBetween ((F _V) " (the_Vertices_of H)) by Th99;

now :: thesis: for e being object st e in G1 .edgesBetween ((F _V) " (the_Vertices_of H)) holds
e in (F _E) " (the_Edges_of H)

let e be object ; :: thesis: ( e in G1 .edgesBetween ((F _V) " (the_Vertices_of H)) implies e in (F _E) " (the_Edges_of H) )
set v = (the_Source_of G1) . e;
set w = (the_Target_of G1) . e;
assume A3: e in G1 .edgesBetween ((F _V) " (the_Vertices_of H)) ; :: thesis: e in (F _E) " (the_Edges_of H)
then A4: e in dom (F _E) by A1;
A5: ( e in the_Edges_of G1 & (the_Source_of G1) . e in (F _V) " (the_Vertices_of H) & (the_Target_of G1) . e in (F _V) " (the_Vertices_of H) ) by A3, GLIB_000:31;
then A6: ( (the_Source_of G1) . e in dom (F _V) & (F _V) . ((the_Source_of G1) . e) in the_Vertices_of H & (the_Target_of G1) . e in dom (F _V) & (F _V) . ((the_Target_of G1) . e) in the_Vertices_of H ) by FUNCT_1:def 7;
e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A5, GLIB_000:def 13;
then A7: (F _E) . e Joins (F _V) . ((the_Source_of G1) . e),(F _V) . ((the_Target_of G1) . e),G2 by A4, A6, GLIB_010:4;
(F _E) . e in rng (F _E) by A4, FUNCT_1:3;
then (F _E) . e in the_Edges_of (rng F) by GLIB_010:54;
then (F _E) . e Joins (F _V) . ((the_Source_of G1) . e),(F _V) . ((the_Target_of G1) . e), rng F by A7, GLIB_000:73;
then (F _E) . e in (rng F) .edgesBetween (the_Vertices_of H) by A6, GLIB_000:32;
then (F _E) . e in (rng F) .edgesBetween V2 by GLIB_000:def 37;
then (F _E) . e in the_Edges_of H by GLIB_000:def 37;
hence e in (F _E) " (the_Edges_of H) by A4, FUNCT_1:def 7; :: thesis: verum

end;

then G1 .edgesBetween ((F _V) " (the_Vertices_of H)) c= (F _E) " (the_Edges_of H) by TARSKI:def 3;
hence (F _E) " (the_Edges_of H) = G1 .edgesBetween ((F _V) " (the_Vertices_of H)) by A2, XBOOLE_0:def 10; :: thesis: verum