let G be finite real-weighted WGraph; :: thesis: for s being Vertex of G holds dom ((DIJK:SSSP G,s) `1 ) = G .reachableDFrom s
let src be Vertex of G; :: thesis: dom ((DIJK:SSSP G,src) `1 ) = G .reachableDFrom src
set Gn = DIJK:SSSP G,src;
set RFS = G .reachableDFrom src;
set DCS = DIJK:CompSeq src;
set n = (DIJK:CompSeq src) .Lifespan() ;
A1: card (dom ((DIJK:SSSP G,src) `1 )) = min (((DIJK:CompSeq src) .Lifespan() ) + 1),(card (G .reachableDFrom src)) by Th21
.= min (card (G .reachableDFrom src)),(card (G .reachableDFrom src)) by Th25
.= card (G .reachableDFrom src) ;

now

assume A2: dom ((DIJK:SSSP G,src) `1 ) <> G .reachableDFrom src ; :: thesis: contradiction
dom ((DIJK:SSSP G,src) `1 ) c= G .reachableDFrom src by Th19;
then dom ((DIJK:SSSP G,src) `1 ) c< G .reachableDFrom src by A2, XBOOLE_0:def 8;
hence contradiction by A1, TREES_1:24; :: thesis: verum

end;

hence dom ((DIJK:SSSP G,src) `1 ) = G .reachableDFrom src ; :: thesis: verum