:: deftheorem defines " GLIB_010:def 39 :
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b₃ -valued Walk of G2
for b₅ being b₃ -defined Walk of G1 holds
( b₅ = F " W2 iff ( (F _V) * (b₅ .vertexSeq()) = W2 .vertexSeq() & (F _E) * (b₅ .edgeSeq()) = W2 .edgeSeq() ) );