let G be _Graph; 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; 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 ; ( 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
; ( 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;
hereby ( ( 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() ) implies e in (W1 .replaceEdgeWith (e,W3)) .edges() )
assume
e in (W1 .replaceEdgeWith (e,W3)) .edges()
;
( 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() )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 A2, A3, A4, Th41;
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;
hence
(
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() )
by XBOOLE_0:def 3;
verum
end;
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() )
; 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; verum