let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 .first() = W2 .first() & W1 .last() = W2 .last() holds
W1 .replaceWith (W1,W2) = W2
let W1, W2 be Walk of G; :: thesis: ( W1 .first() = W2 .first() & W1 .last() = W2 .last() implies W1 .replaceWith (W1,W2) = W2 )
assume A1: ( W1 .first() = W2 .first() & W1 .last() = W2 .last() ) ; :: thesis: W1 .replaceWith (W1,W2) = W2
A2: 1 <= len W1 by ABIAN:12;
then A3: W1 is_odd_substring_of W1, 0 by Th15;
reconsider n1 = 1 as odd Element of NAT by POLYFORM:4;
set n2 = W1 .findFirstVertex W1;
set n3 = W1 .findLastVertex W1;
set n4 = len W1;
set W1c = W1 .cut (n1,(W1 .findFirstVertex W1));
set W1ca = (W1 .cut (n1,(W1 .findFirstVertex W1))) .append W2;
set W1c2 = W1 .cut ((W1 .findLastVertex W1),(len W1));
set W1caa = ((W1 .cut (n1,(W1 .findFirstVertex W1))) .append W2) .append (W1 .cut ((W1 .findLastVertex W1),(len W1)));
A4: ( W1 .findFirstVertex W1 = 1 & W1 .findLastVertex W1 = len W1 ) by Th36;
then A5: ( W1 .cut (n1,(W1 .findFirstVertex W1)) is trivial & W1 .cut ((W1 .findLastVertex W1),(len W1)) is trivial ) by A2, GLIB_001:131;
( 1 <= n1 & n1 <= W1 .findFirstVertex W1 & W1 .findFirstVertex W1 <= len W1 ) by A3, Th35;
then (W1 .cut (n1,(W1 .findFirstVertex W1))) .last() = W1 . (W1 .findFirstVertex W1) by GLIB_001:37;
then (W1 .cut (n1,(W1 .findFirstVertex W1))) .last() = W1 .first() by A4, GLIB_001:def 6;
then (W1 .cut (n1,(W1 .findFirstVertex W1))) .last() = W2 .first() by A1;
then (W1 .cut (n1,(W1 .findFirstVertex W1))) .append W2 = W2 by HELLY:16, A5;
then ((W1 .cut (n1,(W1 .findFirstVertex W1))) .append W2) .append (W1 .cut ((W1 .findLastVertex W1),(len W1))) = W2 by A5, GLIB_001:130;
hence W1 .replaceWith (W1,W2) = W2 by A1, A3, Def5; :: thesis: verum