let G be real-weighted WGraph; :: thesis: 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)
let W be Walk of G; :: thesis: for e being set st e in (W .last()) .edgesInOut() holds
(W .addEdge e) .cost() = (W .cost()) + ((the_Weight_of G) . e)
let e be set ; :: thesis: ( e in (W .last()) .edgesInOut() implies (W .addEdge e) .cost() = (W .cost()) + ((the_Weight_of G) . e) )
set W2 = W .addEdge e;
assume e in (W .last()) .edgesInOut() ; :: thesis: (W .addEdge e) .cost() = (W .cost()) + ((the_Weight_of G) . e)
then (W .addEdge e) .weightSeq() = (W .weightSeq()) ^ <*((the_Weight_of G) . e)*> by Th24;
then Sum ((W .addEdge e) .weightSeq()) = (Sum (W .weightSeq())) + (Sum <*((the_Weight_of G) . e)*>) by RVSUM_1:105;
hence (W .addEdge e) .cost() = (W .cost()) + ((the_Weight_of G) . e) by FINSOP_1:12; :: thesis: verum