let G be WGraph; :: thesis: for W being Walk of G
for e being set st e in (W .last() ) .edgesInOut() holds
(W .addEdge e) .weightSeq() = (W .weightSeq() ) ^ <*((the_Weight_of G) . e)*>
let W be Walk of G; :: thesis: for e being set st e in (W .last() ) .edgesInOut() holds
(W .addEdge e) .weightSeq() = (W .weightSeq() ) ^ <*((the_Weight_of G) . e)*>
let e be set ; :: thesis: ( e in (W .last() ) .edgesInOut() implies (W .addEdge e) .weightSeq() = (W .weightSeq() ) ^ <*((the_Weight_of G) . e)*> )
set W2 = W .addEdge e;
set WA = G .walkOf (W .last() ),e,((W .last() ) .adj e);
assume e in (W .last() ) .edgesInOut() ; :: thesis: (W .addEdge e) .weightSeq() = (W .weightSeq() ) ^ <*((the_Weight_of G) . e)*>
then A1: e Joins W .last() ,(W .last() ) .adj e,G by GLIB_000:70;
then ( W .addEdge e = W .append (G .walkOf (W .last() ),e,((W .last() ) .adj e)) & W .last() = (G .walkOf (W .last() ),e,((W .last() ) .adj e)) .first() ) by GLIB_001:16, GLIB_001:def 13;
hence (W .addEdge e) .weightSeq() = (W .weightSeq() ) ^ ((G .walkOf (W .last() ),e,((W .last() ) .adj e)) .weightSeq() ) by Th23
.= (W .weightSeq() ) ^ <*((the_Weight_of G) . e)*> by A1, Th21 ;
:: thesis: verum