let G be Graph; 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; 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; 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 ; 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; ( 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
; 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; verum