:: deftheorem Def37 defines .: GLIB_010:def 37 :
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b₃ -defined Walk of G1
for b₅ being Walk of G2 holds
( b₅ = F .: W1 iff ( (F _V) * (W1 .vertexSeq()) = b₅ .vertexSeq() & (F _E) * (W1 .edgeSeq()) = b₅ .edgeSeq() ) );