let G be _finite nonnegative-weighted WGraph; for s being Vertex of G
for G2 being inducedWSubgraph of G, dom ((DIJK:SSSP (G,s)) `1),(DIJK:SSSP (G,s)) `2 holds
( G2 is_mincost_DTree_rooted_at s & ( for v being Vertex of G st v in G .reachableDFrom s holds
( v in the_Vertices_of G2 & G .min_DPath_cost (s,v) = ((DIJK:SSSP (G,s)) `1) . v ) ) )
let src be Vertex of G; for G2 being inducedWSubgraph of G, dom ((DIJK:SSSP (G,src)) `1),(DIJK:SSSP (G,src)) `2 holds
( G2 is_mincost_DTree_rooted_at src & ( for v being Vertex of G st v in G .reachableDFrom src holds
( v in the_Vertices_of G2 & G .min_DPath_cost (src,v) = ((DIJK:SSSP (G,src)) `1) . v ) ) )
let G2 be inducedWSubgraph of G, dom ((DIJK:SSSP (G,src)) `1),(DIJK:SSSP (G,src)) `2 ; ( G2 is_mincost_DTree_rooted_at src & ( for v being Vertex of G st v in G .reachableDFrom src holds
( v in the_Vertices_of G2 & G .min_DPath_cost (src,v) = ((DIJK:SSSP (G,src)) `1) . v ) ) )
set Res = DIJK:SSSP (G,src);
set dR = dom ((DIJK:SSSP (G,src)) `1);
thus
G2 is_mincost_DTree_rooted_at src
by Th23; for v being Vertex of G st v in G .reachableDFrom src holds
( v in the_Vertices_of G2 & G .min_DPath_cost (src,v) = ((DIJK:SSSP (G,src)) `1) . v )
let v be Vertex of G; ( v in G .reachableDFrom src implies ( v in the_Vertices_of G2 & G .min_DPath_cost (src,v) = ((DIJK:SSSP (G,src)) `1) . v ) )
assume
v in G .reachableDFrom src
; ( v in the_Vertices_of G2 & G .min_DPath_cost (src,v) = ((DIJK:SSSP (G,src)) `1) . v )
then A1:
v in dom ((DIJK:SSSP (G,src)) `1)
by Th26;
(DIJK:SSSP (G,src)) `2 c= G .edgesBetween (dom ((DIJK:SSSP (G,src)) `1))
by Th22;
hence
v in the_Vertices_of G2
by A1, GLIB_000:def 37; G .min_DPath_cost (src,v) = ((DIJK:SSSP (G,src)) `1) . v
thus
G .min_DPath_cost (src,v) = ((DIJK:SSSP (G,src)) `1) . v
by A1, Th23; verum