let G1, G2 be _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2
for V being non empty Subset of (the_Vertices_of (dom F))
for H being inducedSubgraph of G1,V st F is continuous holds
rng (F | H) is inducedSubgraph of G2,((F _V) .: V)
let F be non empty PGraphMapping of G1,G2; :: thesis: for V being non empty Subset of (the_Vertices_of (dom F))
for H being inducedSubgraph of G1,V st F is continuous holds
rng (F | H) is inducedSubgraph of G2,((F _V) .: V)
let V be non empty Subset of (the_Vertices_of (dom F)); :: thesis: for H being inducedSubgraph of G1,V st F is continuous holds
rng (F | H) is inducedSubgraph of G2,((F _V) .: V)
A1: V is non empty Subset of (the_Vertices_of G1) by XBOOLE_1:1;
let H be inducedSubgraph of G1,V; :: thesis: ( F is continuous implies rng (F | H) is inducedSubgraph of G2,((F _V) .: V) )
assume A2: F is continuous ; :: thesis: rng (F | H) is inducedSubgraph of G2,((F _V) .: V)
set v = the Vertex of H;
the Vertex of H in the_Vertices_of H ;
then the Vertex of H in V by A1, GLIB_000:def 37;
then the Vertex of H in (the_Vertices_of H) /\ (the_Vertices_of (dom F)) by XBOOLE_0:def 4;
then the Vertex of H in (the_Vertices_of H) /\ (dom (F _V)) by GLIB_010:54;
then the Vertex of H in dom ((F | H) _V) by RELAT_1:61;
then A3: not F | H is empty ;
then A4: the_Vertices_of (rng (F | H)) = rng ((F | H) _V) by GLIB_010:54
.= (F _V) .: (the_Vertices_of H) by RELAT_1:115
.= (F _V) .: V by A1, GLIB_000:def 37 ;
the_Edges_of (rng (F | H)) = rng ((F | H) _E) by A3, GLIB_010:54
.= (F _E) .: (the_Edges_of H) by RELAT_1:115
.= (F _E) .: (G1 .edgesBetween V) by A1, GLIB_000:def 37
.= G2 .edgesBetween ((F _V) .: V) by A2, Th104 ;
hence rng (F | H) is inducedSubgraph of G2,((F _V) .: V) by A4, GLIB_000:def 37; :: thesis: verum