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 )

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

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;A3: now :: thesis: for Q being oriented Chain of G st Q is_orientedpath_of v1,v2 holds

cost (P,W) <= cost (Q,W)

P is_orientedpath_of v1,v2,U
by A2, GRAPH_5:def 18;cost (P,W) <= cost (Q,W)

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;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

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

hereby :: thesis: verum

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

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;A5: now :: thesis: for Q being oriented Chain of G st Q is_orientedpath_of v1,v2,U holds

cost (P,W) <= cost (Q,W)

P is_orientedpath_of v1,v2
by A4, GRAPH_5:def 17;cost (P,W) <= cost (Q,W)

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;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

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