:: deftheorem Def7 defines Weight GRAPHSP:def 7 :
for G being oriented Graph
for v1, v2 being Vertex of G
for W being Function holds
( ( ex e being set st
( e in the carrier' of G & e orientedly_joins v1,v2 ) implies Weight (v1,v2,W) = W . (XEdge (v1,v2)) ) & ( ( for e being set holds
( not e in the carrier' of G or not e orientedly_joins v1,v2 ) ) implies Weight (v1,v2,W) = - 1 ) );