theorem :: GLIB_006:45

for G being _Graph
for W1, W2 being Walk of G
for e being object holds
( W1 .first() = (W1 .replaceWithEdge (W2,e)) .first() & W1 .last() = (W1 .replaceWithEdge (W2,e)) .last() )