theorem :: GLIB_003:25

for G being real-weighted WGraph
for W being Walk of G
for e being set st e in (W .last()) .edgesInOut() holds
(W .addEdge e) .cost() = (W .cost()) + ((the_Weight_of G) . e)