for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b₃ -defined Walk of G1 holds (F .: W1) .edges() = (F _E) .: (W1 .edges())