theorem :: GLIB_006:44

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