let G be _Graph; :: thesis: for W1, W2 being Walk of G
for e being object holds
( W1 .first() = (W1 .replaceWithEdge (W2,e)) .first() & W1 .last() = (W1 .replaceWithEdge (W2,e)) .last() )
let W1, W2 be Walk of G; :: thesis: for e being object holds
( W1 .first() = (W1 .replaceWithEdge (W2,e)) .first() & W1 .last() = (W1 .replaceWithEdge (W2,e)) .last() )
let e be object ; :: thesis: ( W1 .first() = (W1 .replaceWithEdge (W2,e)) .first() & W1 .last() = (W1 .replaceWithEdge (W2,e)) .last() )
per cases ( ( W2 is_odd_substring_of W1, 0 & e Joins W2 .first() ,W2 .last() ,G ) or not W2 is_odd_substring_of W1, 0 or not e Joins W2 .first() ,W2 .last() ,G ) ;
suppose ( W2 is_odd_substring_of W1, 0 & e Joins W2 .first() ,W2 .last() ,G ) ; :: thesis: ( W1 .first() = (W1 .replaceWithEdge (W2,e)) .first() & W1 .last() = (W1 .replaceWithEdge (W2,e)) .last() )
then consider W3 being Walk of G such that
A1: W1 .replaceWithEdge (W2,e) = W1 .replaceWith (W2,W3) by Th47;
thus ( W1 .first() = (W1 .replaceWithEdge (W2,e)) .first() & W1 .last() = (W1 .replaceWithEdge (W2,e)) .last() ) by A1, Th39; :: thesis: verum
end;
suppose ( not W2 is_odd_substring_of W1, 0 or not e Joins W2 .first() ,W2 .last() ,G ) ; :: thesis: ( W1 .first() = (W1 .replaceWithEdge (W2,e)) .first() & W1 .last() = (W1 .replaceWithEdge (W2,e)) .last() )
hence ( W1 .first() = (W1 .replaceWithEdge (W2,e)) .first() & W1 .last() = (W1 .replaceWithEdge (W2,e)) .last() ) by Def7; :: thesis: verum
end;
end;