let G1, G2 be _Graph; :: thesis: for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b₁ -valued Walk of G2 holds (F " W2) .edges() = (F _E) " (W2 .edges())
let F be non empty one-to-one PGraphMapping of G1,G2; :: thesis: for W2 being F -valued Walk of G2 holds (F " W2) .edges() = (F _E) " (W2 .edges())
let W2 be F -valued Walk of G2; :: thesis: (F " W2) .edges() = (F _E) " (W2 .edges())
thus (F " W2) .edges() = ((F ") _E) .: (W2 .edges()) by GLIB_010:136
.= (F _E) " (W2 .edges()) by FUNCT_1:85 ; :: thesis: verum