let G be _Graph; for W1, W2, W3 being Walk of G holds
( W1 .first() = (W1 .replaceWith (W2,W3)) .first() & W1 .last() = (W1 .replaceWith (W2,W3)) .last() )
let W1, W2, W3 be Walk of G; ( W1 .first() = (W1 .replaceWith (W2,W3)) .first() & W1 .last() = (W1 .replaceWith (W2,W3)) .last() )
per cases
( ( W2 is_odd_substring_of W1, 0 & W2 .first() = W3 .first() & W2 .last() = W3 .last() ) or not W2 is_odd_substring_of W1, 0 or not W2 .first() = W3 .first() or not W2 .last() = W3 .last() )
;
suppose A1:
(
W2 is_odd_substring_of W1,
0 &
W2 .first() = W3 .first() &
W2 .last() = W3 .last() )
;
( W1 .first() = (W1 .replaceWith (W2,W3)) .first() & W1 .last() = (W1 .replaceWith (W2,W3)) .last() )then A2:
W1 .replaceWith (
W2,
W3)
= ((W1 .cut (1,(W1 .findFirstVertex W2))) .append W3) .append (W1 .cut ((W1 .findLastVertex W2),(len W1)))
by Def5;
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))) .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)))) .first() = ((W1 .cut (n1,(W1 .findFirstVertex W2))) .append W3) .first() &
(((W1 .cut (n1,(W1 .findFirstVertex W2))) .append W3) .append (W1 .cut ((W1 .findLastVertex W2),(len W1)))) .last() = (W1 .cut ((W1 .findLastVertex W2),(len W1))) .last() )
by GLIB_001:30;
hence
(
W1 .first() = (W1 .replaceWith (W2,W3)) .first() &
W1 .last() = (W1 .replaceWith (W2,W3)) .last() )
by A1, A2, Th38;
verum end;