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 and

A3: ( e1 in the carrier' of G & e1 orientedly_joins v1,v2 ) by Def6;

e = e1 by A1, A3, Th10;

hence Weight (v1,v2,W) = W . e by A2, A3, Def7; :: thesis: verum

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 and

A3: ( e1 in the carrier' of G & e1 orientedly_joins v1,v2 ) by Def6;

e = e1 by A1, A3, Th10;

hence Weight (v1,v2,W) = W . e by A2, A3, Def7; :: thesis: verum