let G1, G2 be _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2
for H being Subgraph of rng F
for W being Walk of H holds W is b₁ -valued Walk of G2
let F be non empty PGraphMapping of G1,G2; :: thesis: for H being Subgraph of rng F
for W being Walk of H holds W is F -valued Walk of G2
let H be Subgraph of rng F; :: thesis: for W being Walk of H holds W is F -valued Walk of G2
let W be Walk of H; :: thesis: W is F -valued Walk of G2
H is Subgraph of G2 by GLIB_000:43;
then reconsider W9 = W as Walk of G2 by GLIB_001:167;
( the_Vertices_of H c= the_Vertices_of (rng F) & the_Edges_of H c= the_Edges_of (rng F) ) ;
then ( W .vertices() c= the_Vertices_of (rng F) & W .edges() c= the_Edges_of (rng F) ) by XBOOLE_1:1;
then ( W .vertices() c= rng (F _V) & W .edges() c= rng (F _E) ) by GLIB_010:54;
then ( W9 .vertices() c= rng (F _V) & W9 .edges() c= rng (F _E) ) by GLIB_001:98, GLIB_001:110;
hence W is F -valued Walk of G2 by GLIB_010:def 36; :: thesis: verum