let G be Graph; :: thesis: for p, q being oriented Chain of G
for W being Function
for V being set
for v1, v2 being Vertex of G st p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W holds
cost (p,W) = cost (q,W)
let p, q be oriented Chain of G; :: thesis: for W being Function
for V being set
for v1, v2 being Vertex of G st p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W holds
cost (p,W) = cost (q,W)
let W be Function; :: thesis: for V being set
for v1, v2 being Vertex of G st p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W holds
cost (p,W) = cost (q,W)
let V be set ; :: thesis: for v1, v2 being Vertex of G st p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W holds
cost (p,W) = cost (q,W)
let v1, v2 be Vertex of G; :: thesis: ( p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W implies cost (p,W) = cost (q,W) )
assume that
A1: p is_shortestpath_of v1,v2,V,W and
A2: q is_shortestpath_of v1,v2,V,W ; :: thesis: cost (p,W) = cost (q,W)
q is_orientedpath_of v1,v2,V by A2, GRAPH_5:def 18;
then A3: cost (p,W) <= cost (q,W) by A1, GRAPH_5:def 18;
p is_orientedpath_of v1,v2,V by A1, GRAPH_5:def 18;
then cost (q,W) <= cost (p,W) by A2, GRAPH_5:def 18;
hence cost (p,W) = cost (q,W) by A3, XXREAL_0:1; :: thesis: verum