let G be _Graph; for W1, W3 being Walk of G
for e, u, v being object holds
( W1 is_Walk_from u,v iff W1 .replaceEdgeWith (e,W3) is_Walk_from u,v )
let W1, W3 be Walk of G; for e, u, v being object holds
( W1 is_Walk_from u,v iff W1 .replaceEdgeWith (e,W3) is_Walk_from u,v )
let e, u, v be object ; ( W1 is_Walk_from u,v iff W1 .replaceEdgeWith (e,W3) is_Walk_from u,v )
per cases
( ( e Joins W3 .first() ,W3 .last() ,G & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 ) or not e Joins W3 .first() ,W3 .last() ,G or not G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 )
;
end;