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
ex W2 being Walk of G st W1 .replaceEdgeWith (e,W3) = W1 .replaceWith (W2,W3)
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
ex W2 being Walk of G st W1 .replaceEdgeWith (e,W3) = W1 .replaceWith (W2,W3)
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 ex W2 being Walk of G st W1 .replaceEdgeWith (e,W3) = W1 .replaceWith (W2,W3) )
assume A1: ( e Joins W3 .first() ,W3 .last() ,G & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 ) ; :: thesis: ex W2 being Walk of G st W1 .replaceEdgeWith (e,W3) = W1 .replaceWith (W2,W3)
take G .walkOf ((W3 .first()),e,(W3 .last())) ; :: thesis: W1 .replaceEdgeWith (e,W3) = W1 .replaceWith ((G .walkOf ((W3 .first()),e,(W3 .last()))),W3)
thus W1 .replaceEdgeWith (e,W3) = W1 .replaceWith ((G .walkOf ((W3 .first()),e,(W3 .last()))),W3) by A1, Def6; :: thesis: verum