theorem Th38: :: GLIB_006:34

for G being _Graph
for W1, W2, W3 being Walk of G st W2 is_odd_substring_of W1, 0 & W2 .first() = W3 .first() & W2 .last() = W3 .last() holds
( (W1 .cut (1,(W1 .findFirstVertex W2))) .first() = W1 .first() & (W1 .cut (1,(W1 .findFirstVertex W2))) .last() = W3 .first() & ((W1 .cut (1,(W1 .findFirstVertex W2))) .append W3) .first() = W1 .first() & ((W1 .cut (1,(W1 .findFirstVertex W2))) .append W3) .last() = W3 .last() & (W1 .cut ((W1 .findLastVertex W2),(len W1))) .first() = W3 .last() & (W1 .cut ((W1 .findLastVertex W2),(len W1))) .last() = W1 .last() )