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