let V be set ; :: thesis: for W being Function
for G being finite Graph
for P being oriented Chain of G
for v1, v2 being Element of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W
let W be Function; :: thesis: for G being finite Graph
for P being oriented Chain of G
for v1, v2 being Element of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W
let G be finite Graph; :: thesis: for P being oriented Chain of G
for v1, v2 being Element of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W
let P be oriented Chain of G; :: thesis: for v1, v2 being Element of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W
let v1, v2 be Element of G; :: thesis: ( P is_orientedpath_of v1,v2,V & W is_weight>=0of G implies ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W )
assume that
A1: P is_orientedpath_of v1,v2,V and
A2: W is_weight>=0of G ; :: thesis: ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W
AcyclicPaths (v1,v2,V) <> {} by A1, Th42;
then consider r being FinSequence of the carrier' of G such that
A3: r in AcyclicPaths (v1,v2,V) and
A4: for s being FinSequence of the carrier' of G st s in AcyclicPaths (v1,v2,V) holds
cost (r,W) <= cost (s,W) by Th51;
consider t being oriented Simple Chain of G such that
A5: r = t and
A6: t is_acyclicpath_of v1,v2,V by A3;
take t ; :: thesis: t is_shortestpath_of v1,v2,V,W
thus t is_orientedpath_of v1,v2,V by A6; :: according to GRAPH_5:def 18 :: thesis: for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds
cost (t,W) <= cost (q,W)

hereby :: thesis: verum

let s be oriented Chain of G; :: thesis: ( s is_orientedpath_of v1,v2,V implies cost (t,W) <= cost (s,W) )
assume A7: s is_orientedpath_of v1,v2,V ; :: thesis: cost (t,W) <= cost (s,W)
then consider x being Element of the carrier' of G * such that
A8: x in AcyclicPaths s by Th42, SUBSET_1:4;
AcyclicPaths s c= AcyclicPaths (v1,v2,V) by A7, Th39;
then A9: cost (r,W) <= cost (x,W) by A4, A8;
cost (x,W) <= cost (s,W) by A2, A8, Th54;
hence cost (t,W) <= cost (s,W) by A5, A9, XXREAL_0:2; :: thesis: verum

end;