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 H2 being inducedSubgraph of (rng F),V2
for H1 being inducedSubgraph of G1,((F _V) " (the_Vertices_of H2)) st G1 .edgesBetween ((F _V) " (the_Vertices_of H2)) c= dom (F _E) holds
rng (F | H1) == H2
let F be non empty PGraphMapping of G1,G2; :: thesis: for V2 being non empty Subset of (the_Vertices_of (rng F))
for H2 being inducedSubgraph of (rng F),V2
for H1 being inducedSubgraph of G1,((F _V) " (the_Vertices_of H2)) st G1 .edgesBetween ((F _V) " (the_Vertices_of H2)) c= dom (F _E) holds
rng (F | H1) == H2
let V2 be non empty Subset of (the_Vertices_of (rng F)); :: thesis: for H2 being inducedSubgraph of (rng F),V2
for H1 being inducedSubgraph of G1,((F _V) " (the_Vertices_of H2)) st G1 .edgesBetween ((F _V) " (the_Vertices_of H2)) c= dom (F _E) holds
rng (F | H1) == H2
let H2 be inducedSubgraph of (rng F),V2; :: thesis: for H1 being inducedSubgraph of G1,((F _V) " (the_Vertices_of H2)) st G1 .edgesBetween ((F _V) " (the_Vertices_of H2)) c= dom (F _E) holds
rng (F | H1) == H2
let H1 be inducedSubgraph of G1,((F _V) " (the_Vertices_of H2)); :: thesis: ( G1 .edgesBetween ((F _V) " (the_Vertices_of H2)) c= dom (F _E) implies rng (F | H1) == H2 )
assume A1: G1 .edgesBetween ((F _V) " (the_Vertices_of H2)) c= dom (F _E) ; :: thesis: rng (F | H1) == H2
A2: H2 is Subgraph of G2 by GLIB_000:43;
A3: (F _E) " (the_Edges_of H2) = G1 .edgesBetween ((F _V) " (the_Vertices_of H2)) by A1, Th101;
set v = the Vertex of H2;
the Vertex of H2 in the_Vertices_of H2 ;
then the Vertex of H2 in the_Vertices_of (rng F) ;
then the Vertex of H2 in rng (F _V) by GLIB_010:54;
then consider x being object such that
A4: ( x in dom (F _V) & (F _V) . x = the Vertex of H2 ) by FUNCT_1:def 3;
A5: x in (F _V) " (the_Vertices_of H2) by A4, FUNCT_1:def 7;
then A6: ( the_Vertices_of H1 = (F _V) " (the_Vertices_of H2) & the_Edges_of H1 = (F _E) " (the_Edges_of H2) ) by A3, GLIB_000:def 37;
the_Vertices_of H2 c= the_Vertices_of (rng F) ;
then A7: the_Vertices_of H2 c= rng (F _V) by GLIB_010:54;
the_Edges_of H2 c= the_Edges_of (rng F) ;
then A8: the_Edges_of H2 c= rng (F _E) by GLIB_010:54;
x in (dom (F _V)) /\ (the_Vertices_of H1) by A6, A4, A5, XBOOLE_0:def 4;
then x in dom ((F | H1) _V) by RELAT_1:61;
then A9: not F | H1 is empty ;
then A10: the_Vertices_of (rng (F | H1)) = rng ((F _V) | (the_Vertices_of H1)) by GLIB_010:54
.= (F _V) .: ((F _V) " (the_Vertices_of H2)) by A6, RELAT_1:115
.= the_Vertices_of H2 by A7, FUNCT_1:77 ;
the_Edges_of (rng (F | H1)) = rng ((F _E) | (the_Edges_of H1)) by A9, GLIB_010:54
.= (F _E) .: ((F _E) " (the_Edges_of H2)) by A6, RELAT_1:115
.= the_Edges_of H2 by A8, FUNCT_1:77 ;
hence rng (F | H1) == H2 by A2, A10, GLIB_000:86; :: thesis: verum