let G be real-weighted WGraph; 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; 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 ; ( 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
; (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; verum