let G be _Graph; :: thesis: for W1, W3 being Walk of G
for e being object holds
( W1 .first() = (W1 .replaceEdgeWith (e,W3)) .first() & W1 .last() = (W1 .replaceEdgeWith (e,W3)) .last() )
let W1, W3 be Walk of G; :: thesis: for e being object holds
( W1 .first() = (W1 .replaceEdgeWith (e,W3)) .first() & W1 .last() = (W1 .replaceEdgeWith (e,W3)) .last() )
let e be object ; :: thesis: ( W1 .first() = (W1 .replaceEdgeWith (e,W3)) .first() & W1 .last() = (W1 .replaceEdgeWith (e,W3)) .last() )

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 ) ;

suppose ( e Joins W3 .first() ,W3 .last() ,G & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 ) ; :: thesis: ( W1 .first() = (W1 .replaceEdgeWith (e,W3)) .first() & W1 .last() = (W1 .replaceEdgeWith (e,W3)) .last() )

then consider W2 being Walk of G such that
A1: W1 .replaceEdgeWith (e,W3) = W1 .replaceWith (W2,W3) by Th46;
thus ( W1 .first() = (W1 .replaceEdgeWith (e,W3)) .first() & W1 .last() = (W1 .replaceEdgeWith (e,W3)) .last() ) by A1, Th39; :: thesis: verum

end;

suppose ( not e Joins W3 .first() ,W3 .last() ,G or not G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 ) ; :: thesis: ( W1 .first() = (W1 .replaceEdgeWith (e,W3)) .first() & W1 .last() = (W1 .replaceEdgeWith (e,W3)) .last() )

hence ( W1 .first() = (W1 .replaceEdgeWith (e,W3)) .first() & W1 .last() = (W1 .replaceEdgeWith (e,W3)) .last() ) by Def6; :: thesis: verum

end;

end;