let G be _Graph; :: thesis: for W1, W2 being Walk of G
for e being object st W2 is_odd_substring_of W1, 0 & e Joins W2 .first() ,W2 .last() ,G holds
ex W3 being Walk of G st W1 .replaceWithEdge (W2,e) = W1 .replaceWith (W2,W3)
let W1, W2 be Walk of G; :: thesis: for e being object st W2 is_odd_substring_of W1, 0 & e Joins W2 .first() ,W2 .last() ,G holds
ex W3 being Walk of G st W1 .replaceWithEdge (W2,e) = W1 .replaceWith (W2,W3)
let e be object ; :: thesis: ( W2 is_odd_substring_of W1, 0 & e Joins W2 .first() ,W2 .last() ,G implies ex W3 being Walk of G st W1 .replaceWithEdge (W2,e) = W1 .replaceWith (W2,W3) )
assume A1: ( W2 is_odd_substring_of W1, 0 & e Joins W2 .first() ,W2 .last() ,G ) ; :: thesis: ex W3 being Walk of G st W1 .replaceWithEdge (W2,e) = W1 .replaceWith (W2,W3)
take G .walkOf ((W2 .first()),e,(W2 .last())) ; :: thesis: W1 .replaceWithEdge (W2,e) = W1 .replaceWith (W2,(G .walkOf ((W2 .first()),e,(W2 .last()))))
thus W1 .replaceWithEdge (W2,e) = W1 .replaceWith (W2,(G .walkOf ((W2 .first()),e,(W2 .last())))) by A1, Def7; :: thesis: verum