theorem Th131: :: GLIB_010:131

for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b₃ -defined Walk of G1
for v, w being object st W1 is_Walk_from v,w holds
( v in dom (F _V) & w in dom (F _V) )