let U, V be set ; :: thesis: for G being oriented finite Graph
for P being oriented Chain of G
for W being Function of the carrier' of G,Real>=0
for v1, v2 being Vertex of G st the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) holds
( P is_shortestpath_of v1,v2,U,W iff P is_shortestpath_of v1,v2,W )
let G be oriented finite Graph; :: thesis: for P being oriented Chain of G
for W being Function of the carrier' of G,Real>=0
for v1, v2 being Vertex of G st the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) holds
( P is_shortestpath_of v1,v2,U,W iff P is_shortestpath_of v1,v2,W )
let P be oriented Chain of G; :: thesis: for W being Function of the carrier' of G,Real>=0
for v1, v2 being Vertex of G st the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) holds
( P is_shortestpath_of v1,v2,U,W iff P is_shortestpath_of v1,v2,W )
let W be Function of the carrier' of G,Real>=0 ; :: thesis: for v1, v2 being Vertex of G st the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) holds
( P is_shortestpath_of v1,v2,U,W iff P is_shortestpath_of v1,v2,W )
let v1, v2 be Vertex of G; :: thesis: ( the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) implies ( P is_shortestpath_of v1,v2,U,W iff P is_shortestpath_of v1,v2,W ) )
assume A1: ( the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) ) ; :: thesis: ( P is_shortestpath_of v1,v2,U,W iff P is_shortestpath_of v1,v2,W )

hereby :: thesis: ( P is_shortestpath_of v1,v2,W implies P is_shortestpath_of v1,v2,U,W )

assume A2: P is_shortestpath_of v1,v2,U,W ; :: thesis: P is_shortestpath_of v1,v2,W

A3: now

let Q be oriented Chain of G; :: thesis: ( Q is_orientedpath_of v1,v2 implies cost P,W <= cost Q,W )
assume Q is_orientedpath_of v1,v2 ; :: thesis: cost P,W <= cost Q,W
then Q is_orientedpath_of v1,v2,U by A1, Th12;
hence cost P,W <= cost Q,W by A2, GRAPH_5:def 18; :: thesis: verum

end;

P is_orientedpath_of v1,v2,U by A2, GRAPH_5:def 18;
then P is_orientedpath_of v1,v2 by GRAPH_5:def 4;
hence P is_shortestpath_of v1,v2,W by A3, GRAPH_5:def 17; :: thesis: verum

end;

hereby :: thesis: verum

assume A4: P is_shortestpath_of v1,v2,W ; :: thesis: P is_shortestpath_of v1,v2,U,W

A5: now

let Q be oriented Chain of G; :: thesis: ( Q is_orientedpath_of v1,v2,U implies cost P,W <= cost Q,W )
assume Q is_orientedpath_of v1,v2,U ; :: thesis: cost P,W <= cost Q,W
then Q is_orientedpath_of v1,v2 by GRAPH_5:def 4;
hence cost P,W <= cost Q,W by A4, GRAPH_5:def 17; :: thesis: verum

end;

P is_orientedpath_of v1,v2 by A4, GRAPH_5:def 17;
then P is_orientedpath_of v1,v2,U by A1, Th12;
hence P is_shortestpath_of v1,v2,U,W by A5, GRAPH_5:def 18; :: thesis: verum

end;