let G be _Graph; :: thesis: for W1, W3 being Walk of G
for e being object st e Joins W3 .first() ,W3 .last() ,G & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 holds
( e in (W1 .replaceEdgeWith (e,W3)) .edges() iff ( e in (W1 .cut (1,(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))))) .edges() or e in W3 .edges() or e in (W1 .cut ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))),(len W1))) .edges() ) )
let W1, W3 be Walk of G; :: thesis: for e being object st e Joins W3 .first() ,W3 .last() ,G & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 holds
( e in (W1 .replaceEdgeWith (e,W3)) .edges() iff ( e in (W1 .cut (1,(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))))) .edges() or e in W3 .edges() or e in (W1 .cut ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))),(len W1))) .edges() ) )
let e be object ; :: thesis: ( e Joins W3 .first() ,W3 .last() ,G & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 implies ( e in (W1 .replaceEdgeWith (e,W3)) .edges() iff ( e in (W1 .cut (1,(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))))) .edges() or e in W3 .edges() or e in (W1 .cut ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))),(len W1))) .edges() ) ) )
assume that
A1: e Joins W3 .first() ,W3 .last() ,G and
A2: G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 ; :: thesis: ( e in (W1 .replaceEdgeWith (e,W3)) .edges() iff ( e in (W1 .cut (1,(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))))) .edges() or e in W3 .edges() or e in (W1 .cut ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))),(len W1))) .edges() ) )
set W2 = G .walkOf ((W3 .first()),e,(W3 .last()));
set W9 = W1 .replaceWith ((G .walkOf ((W3 .first()),e,(W3 .last()))),W3);
A3: W1 .replaceWith ((G .walkOf ((W3 .first()),e,(W3 .last()))),W3) = W1 .replaceEdgeWith (e,W3) by A1, A2, Def6;
A4: ( (G .walkOf ((W3 .first()),e,(W3 .last()))) .first() = W3 .first() & (G .walkOf ((W3 .first()),e,(W3 .last()))) .last() = W3 .last() ) by A1, GLIB_001:15;
assume ( e in (W1 .cut (1,(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))))) .edges() or e in W3 .edges() or e in (W1 .cut ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))),(len W1))) .edges() ) ; :: thesis: e in (W1 .replaceEdgeWith (e,W3)) .edges()
then ( e in ((W1 .cut (1,(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))))) .edges()) \/ (W3 .edges()) or e in (W1 .cut ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))),(len W1))) .edges() ) by XBOOLE_0:def 3;
then e in (((W1 .cut (1,(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))))) .edges()) \/ (W3 .edges())) \/ ((W1 .cut ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))),(len W1))) .edges()) by XBOOLE_0:def 3;
hence e in (W1 .replaceEdgeWith (e,W3)) .edges() by A2, A3, A4, Th41; :: thesis: verum