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

end;

A6: (F .: W1) .vertices() c= the_Vertices_of H2

proof

(F .: W1) .vertices() = (F _V) .: (W1 .vertices()) by GLIB_010:135;
then A7: (F .: W1) .vertices() c= (F _V) .: (the_Vertices_of H1) by A2, RELAT_1:123;
(F _V) .: (the_Vertices_of H1) c= the_Vertices_of H2 by A3, FUNCT_1:75;
hence (F .: W1) .vertices() c= the_Vertices_of H2 by A7, XBOOLE_1:1; :: thesis: verum

end;

(F .: W1) .edges() c= the_Edges_of H2

proof

(F .: W1) .edges() = (F _E) .: (W1 .edges()) by GLIB_010:136;
then A8: (F .: W1) .edges() c= (F _E) .: (the_Edges_of H1) by A2, RELAT_1:123;
(F _E) .: (the_Edges_of H1) c= the_Edges_of H2 by A3, FUNCT_1:75;
hence (F .: W1) .edges() c= the_Edges_of H2 by A8, XBOOLE_1:1; :: thesis: verum

end;

hence F .: W1 is Walk of H2 by A1, A6, GLIB_001:170; :: thesis: verum