for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b₃ -defined Walk of G1
for n being even Element of NAT st 1 <= n & n <= len W1 holds
(F _E) . (W1 . n) = (F .: W1) . n