theorem Th17: :: GLIB_003:17

for G being WGraph
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)*>