theorem Th25: :: GRAPHSP:25

for e being set
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