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)
for W1 being Walk of H1 holds W1 is b1 -defined Walk of G1
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)
for W1 being Walk of H1 holds W1 is F -defined Walk of G1
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)
for W1 being Walk of H1 holds W1 is F -defined Walk of G1
let H1 be inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2); :: thesis: for W1 being Walk of H1 holds W1 is F -defined Walk of G1
let W1 be Walk of H1; :: thesis: W1 is F -defined Walk of G1
A1: ( the_Vertices_of H1 = (F _V) " (the_Vertices_of H2) & the_Edges_of H1 = (F _E) " (the_Edges_of H2) )
proof
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
A2: ( x in dom (F _V) & (F _V) . x = the Vertex of H2 ) by FUNCT_1:def 3;
A3: not (F _V) " (the_Vertices_of H2) is empty by A2, FUNCT_1:def 7;
H2 is Subgraph of G2 by GLIB_000:43;
then (F _E) " (the_Edges_of H2) c= G1 .edgesBetween ((F _V) " (the_Vertices_of H2)) by Th99;
hence ( 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; :: thesis: verum
end;
( the_Vertices_of H1 c= dom (F _V) & the_Edges_of H1 c= dom (F _E) ) by A1, RELAT_1:132;
then A4: ( W1 .vertices() c= dom (F _V) & W1 .edges() c= dom (F _E) ) by XBOOLE_1:1;
reconsider W = W1 as Walk of G1 by GLIB_001:167;
( W .vertices() = W1 .vertices() & W .edges() = W1 .edges() ) by GLIB_001:98, GLIB_001:110;
hence W1 is F -defined Walk of G1 by A4, GLIB_010:def 35; :: thesis: verum