for G being _finite nonnegative-weighted WGraph
for s being Vertex of G
for n being Nat
for G2 being inducedWSubgraph of G, dom (((DIJK:CompSeq s) . n) `1),((DIJK:CompSeq s) . n) `2 holds
( G2 is_mincost_DTree_rooted_at s & ( for v being Vertex of G st v in dom (((DIJK:CompSeq s) . n) `1) holds
G .min_DPath_cost (s,v) = (((DIJK:CompSeq s) . n) `1) . v ) )