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);
reconsider We = (the_Weight_of G) . e as Element of REAL by XREAL_0:def 1;
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() = <*We*> by Th14;
hence (G .walkOf (v1,e,v2)) .cost() = (the_Weight_of G) . e by FINSOP_1:11; :: thesis: verum