let U, V be set ; 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; 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; 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; 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; ( 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 ) ) )
; ( P is_shortestpath_of v1,v2,U,W iff P is_shortestpath_of v1,v2,W )
hereby ( 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
;
P is_shortestpath_of v1,v2,WA3:
now for Q being oriented Chain of G st Q is_orientedpath_of v1,v2 holds
cost (P,W) <= cost (Q,W)let Q be
oriented Chain of
G;
( Q is_orientedpath_of v1,v2 implies cost (P,W) <= cost (Q,W) )assume
Q is_orientedpath_of v1,
v2
;
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;
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;
verum
end;
hereby verum
assume A4:
P is_shortestpath_of v1,
v2,
W
;
P is_shortestpath_of v1,v2,U,WA5:
now for Q being oriented Chain of G st Q is_orientedpath_of v1,v2,U holds
cost (P,W) <= cost (Q,W)let Q be
oriented Chain of
G;
( Q is_orientedpath_of v1,v2,U implies cost (P,W) <= cost (Q,W) )assume
Q is_orientedpath_of v1,
v2,
U
;
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;
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;
verum
end;