let G be _finite nonnegative-weighted WGraph; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum