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 Th22; :: 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 A2: v in dom ((DIJK:SSSP G,src) `1 ) by Th25;
(DIJK:SSSP G,src) `2 c= G .edgesBetween (dom ((DIJK:SSSP G,src) `1 )) by Th21;
hence v in the_Vertices_of G2 by A2, GLIB_000:def 39; :: 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 A2, Th22; :: thesis: verum