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