for G1, G2 being _Graph
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