let e be set ; :: thesis: for G being oriented Graph
for v1, v2 being Vertex of G
for W being Function of the carrier' of G,Real>=0 st e in the carrier' of G & e orientedly_joins v1,v2 holds
Weight v1,v2,W = W . e
let G be oriented Graph; :: thesis: for v1, v2 being Vertex of G
for W being Function of the carrier' of G,Real>=0 st e in the carrier' of G & e orientedly_joins v1,v2 holds
Weight v1,v2,W = W . e
let v1, v2 be Vertex of G; :: thesis: for W being Function of the carrier' of G,Real>=0 st e in the carrier' of G & e orientedly_joins v1,v2 holds
Weight v1,v2,W = W . e
let W be Function of the carrier' of G,Real>=0 ; :: thesis: ( e in the carrier' of G & e orientedly_joins v1,v2 implies Weight v1,v2,W = W . e )
set EG = the carrier' of G;
assume A1: ( e in the carrier' of G & e orientedly_joins v1,v2 ) ; :: thesis: Weight v1,v2,W = W . e
then consider e1 being set such that
A2: ( XEdge v1,v2 = e1 & e1 in the carrier' of G & e1 orientedly_joins v1,v2 ) by Def6;
e = e1 by A1, A2, Th10;
hence Weight v1,v2,W = W . e by A2, Def7; :: thesis: verum