theorem Th39: :: GLIB_006:35

for G being _Graph
for W1, W2, W3 being Walk of G holds
( W1 .first() = (W1 .replaceWith (W2,W3)) .first() & W1 .last() = (W1 .replaceWith (W2,W3)) .last() )