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:67;
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:15, GLIB_001:def 13;
hence (W .addEdge e) .weightSeq() = (W .weightSeq()) ^ ((G .walkOf ((W .last()),e,((W .last()) .adj e))) .weightSeq()) by Th16
.= (W .weightSeq()) ^ <*((the_Weight_of G) . e)*> by A1, Th14 ;
:: thesis: verum