:: deftheorem defines " GLIB_010:def 38 :
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 holds F " W2 = (F ") .: W2;