let G be real-weighted WGraph; :: thesis: for v1, v2 being Vertex of G
for e being set st e Joins v1,v2,G holds
(G .walkOf v1,e,v2) .cost() = (the_Weight_of G) . e
let v1, v2 be Vertex of G; :: thesis: for e being set st e Joins v1,v2,G holds
(G .walkOf v1,e,v2) .cost() = (the_Weight_of G) . e
let e be set ; :: thesis: ( e Joins v1,v2,G implies (G .walkOf v1,e,v2) .cost() = (the_Weight_of G) . e )
set W = G .walkOf v1,e,v2;
assume e Joins v1,v2,G ; :: thesis: (G .walkOf v1,e,v2) .cost() = (the_Weight_of G) . e
then (G .walkOf v1,e,v2) .weightSeq() = <*((the_Weight_of G) . e)*> by Th21;
hence (G .walkOf v1,e,v2) .cost() = (the_Weight_of G) . e by FINSOP_1:12; :: thesis: verum