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;
reconsider We = (the_Weight_of G) . e as Element of REAL by XREAL_0:def 1;
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 Th17;
then Sum ((W .addEdge e) .weightSeq()) = (Sum (W .weightSeq())) + (Sum <*We*>) by RVSUM_1:75;
hence (W .addEdge e) .cost() = (W .cost()) + ((the_Weight_of G) . e) by FINSOP_1:11; :: thesis: verum