theorem :: GLIB_010:126

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
( W2 .length() = (F " W2) .length() & len W2 = len (F " W2) ) by Th125;