let G be _Graph; :: thesis: 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 .replaceWith (W2,W3)) .vertices() = (((W1 .cut (1,(W1 .findFirstVertex W2))) .vertices()) \/ (W3 .vertices())) \/ ((W1 .cut ((W1 .findLastVertex W2),(len W1))) .vertices())
let W1, W2, W3 be Walk of G; :: thesis: ( W2 is_odd_substring_of W1, 0 & W2 .first() = W3 .first() & W2 .last() = W3 .last() implies (W1 .replaceWith (W2,W3)) .vertices() = (((W1 .cut (1,(W1 .findFirstVertex W2))) .vertices()) \/ (W3 .vertices())) \/ ((W1 .cut ((W1 .findLastVertex W2),(len W1))) .vertices()) )
assume A1: ( W2 is_odd_substring_of W1, 0 & W2 .first() = W3 .first() & W2 .last() = W3 .last() ) ; :: thesis: (W1 .replaceWith (W2,W3)) .vertices() = (((W1 .cut (1,(W1 .findFirstVertex W2))) .vertices()) \/ (W3 .vertices())) \/ ((W1 .cut ((W1 .findLastVertex W2),(len W1))) .vertices())
reconsider n1 = 1 as odd Element of NAT by POLYFORM:4;
set n2 = W1 .findFirstVertex W2;
set n3 = W1 .findLastVertex W2;
set n4 = len W1;
set W1c = W1 .cut (n1,(W1 .findFirstVertex W2));
set W1ca = (W1 .cut (n1,(W1 .findFirstVertex W2))) .append W3;
set W1c2 = W1 .cut ((W1 .findLastVertex W2),(len W1));
set W1caa = ((W1 .cut (n1,(W1 .findFirstVertex W2))) .append W3) .append (W1 .cut ((W1 .findLastVertex W2),(len W1)));
(W1 .cut (n1,(W1 .findFirstVertex W2))) .last() = W3 .first() by A1, Th38;
then A2: ((W1 .cut (n1,(W1 .findFirstVertex W2))) .append W3) .vertices() = ((W1 .cut (n1,(W1 .findFirstVertex W2))) .vertices()) \/ (W3 .vertices()) by GLIB_001:93;
( ((W1 .cut (n1,(W1 .findFirstVertex W2))) .append W3) .last() = W3 .last() & (W1 .cut ((W1 .findLastVertex W2),(len W1))) .first() = W3 .last() ) by A1, Th38;
then (((W1 .cut (n1,(W1 .findFirstVertex W2))) .append W3) .append (W1 .cut ((W1 .findLastVertex W2),(len W1)))) .vertices() = (((W1 .cut (n1,(W1 .findFirstVertex W2))) .append W3) .vertices()) \/ ((W1 .cut ((W1 .findLastVertex W2),(len W1))) .vertices()) by GLIB_001:93;
hence (W1 .replaceWith (W2,W3)) .vertices() = (((W1 .cut (1,(W1 .findFirstVertex W2))) .vertices()) \/ (W3 .vertices())) \/ ((W1 .cut ((W1 .findLastVertex W2),(len W1))) .vertices()) by A1, A2, Def5; :: thesis: verum