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 .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() )
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 .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() ) )
assume A1: ( W2 is_odd_substring_of W1, 0 & W2 .first() = W3 .first() & W2 .last() = W3 .last() ) ; :: thesis: ( (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() )
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)));
( n1 <= W1 .findFirstVertex W2 & W1 .findFirstVertex W2 <= len W1 ) by A1, Th35;
then A2: ( (W1 .cut (n1,(W1 .findFirstVertex W2))) .first() = W1 . n1 & (W1 .cut (n1,(W1 .findFirstVertex W2))) .last() = W1 . (W1 .findFirstVertex W2) ) by GLIB_001:37;
then A3: (W1 .cut (n1,(W1 .findFirstVertex W2))) .first() = W1 .first() by GLIB_001:def 6;
A4: (W1 .cut (n1,(W1 .findFirstVertex W2))) .last() = W3 .first() by A1, A2, Th34;
then A5: ( ((W1 .cut (n1,(W1 .findFirstVertex W2))) .append W3) .first() = W1 . n1 & ((W1 .cut (n1,(W1 .findFirstVertex W2))) .append W3) .last() = W3 .last() ) by A2, GLIB_001:30;
then A6: ((W1 .cut (n1,(W1 .findFirstVertex W2))) .append W3) .first() = W1 .first() by GLIB_001:def 6;
A7: ((W1 .cut (n1,(W1 .findFirstVertex W2))) .append W3) .last() = W3 .last() by A5;
( W1 .findLastVertex W2 <= len W1 & len W1 <= len W1 ) by A1, Th35;
then A8: ( (W1 .cut ((W1 .findLastVertex W2),(len W1))) .first() = W1 . (W1 .findLastVertex W2) & (W1 .cut ((W1 .findLastVertex W2),(len W1))) .last() = W1 . (len W1) ) by GLIB_001:37;
W1 . (W1 .findLastVertex W2) = W3 .last() by A1, Th34;
then A9: (W1 .cut ((W1 .findLastVertex W2),(len W1))) .first() = W3 .last() by A8;
A10: (W1 .cut ((W1 .findLastVertex W2),(len W1))) .last() = W1 .last() by A8, GLIB_001:def 7;
thus ( (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() ) by A3, A4, A6, A7, A9, A10; :: thesis: verum