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 :: thesis: not dom ((DIJK:SSSP (G,src)) `1) <> G .reachableDFrom src

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:6; :: thesis: verum

end;

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