let G1, G2 be _Graph; :: thesis: for F being non empty one-to-one 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 W2 being b₁ -valued Walk of G2 st W2 is Walk of H2 holds
F " W2 is Walk of H1
let F be non empty one-to-one 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 W2 being F -valued Walk of G2 st W2 is Walk of H2 holds
F " W2 is Walk of H1
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 W2 being F -valued Walk of G2 st W2 is Walk of H2 holds
F " W2 is Walk of H1
let H1 be inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2); :: thesis: for W2 being F -valued Walk of G2 st W2 is Walk of H2 holds
F " W2 is Walk of H1
let W2 be F -valued Walk of G2; :: thesis: ( W2 is Walk of H2 implies F " W2 is Walk of H1 )
assume W2 is Walk of H2 ; :: thesis: F " W2 is Walk of H1
then reconsider W = W2 as Walk of H2 ;
A1: ( W .vertices() = W2 .vertices() & W .edges() = W2 .edges() ) by GLIB_001:98, GLIB_001:110;
A2: ( 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
A3: ( x in dom (F _V) & (F _V) . x = the Vertex of H2 ) by FUNCT_1:def 3;
A4: not (F _V) " (the_Vertices_of H2) is empty by A3, 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 A4, GLIB_000:def 37; :: thesis: verum

end;

A5: (F " W2) .vertices() c= the_Vertices_of H1

proof

(F " W2) .vertices() = (F _V) " (W2 .vertices()) by Th95;
hence (F " W2) .vertices() c= the_Vertices_of H1 by A1, A2, RELAT_1:143; :: thesis: verum

end;

(F " W2) .edges() c= the_Edges_of H1

proof

(F " W2) .edges() = (F _E) " (W2 .edges()) by Th96;
hence (F " W2) .edges() c= the_Edges_of H1 by A1, A2, RELAT_1:143; :: thesis: verum

end;

hence F " W2 is Walk of H1 by A5, GLIB_001:170; :: thesis: verum