let G be _finite real-weighted WGraph; :: thesis: for s being Vertex of G holds ((DIJK:CompSeq s) .Lifespan()) + 1 = card (G .reachableDFrom s)
let src be Vertex of G; :: thesis: ((DIJK:CompSeq src) .Lifespan()) + 1 = card (G .reachableDFrom src)
set DCS = DIJK:CompSeq src;
set RFS = G .reachableDFrom src;
consider k being Nat such that
A1: card (G .reachableDFrom src) = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;

A2: now :: thesis: for n being Nat st (DIJK:CompSeq src) . n = (DIJK:CompSeq src) . (n + 1) holds
k <= n

let n be Nat; :: thesis: ( (DIJK:CompSeq src) . n = (DIJK:CompSeq src) . (n + 1) implies k <= n )
set Gn = (DIJK:CompSeq src) . n;
set Gn1 = (DIJK:CompSeq src) . (n + 1);
assume A3: (DIJK:CompSeq src) . n = (DIJK:CompSeq src) . (n + 1) ; :: thesis: k <= n

now :: thesis: not n < k

assume n < k ; :: thesis: contradiction
then A4: n + 1 < card (G .reachableDFrom src) by A1, XREAL_1:8;
then A5: (n + 1) + 1 <= card (G .reachableDFrom src) by NAT_1:13;
card (dom (((DIJK:CompSeq src) . n) `1)) = min ((n + 1),(card (G .reachableDFrom src))) by Th21;
then A6: card (dom (((DIJK:CompSeq src) . n) `1)) = n + 1 by A4, XXREAL_0:def 9;
card (dom (((DIJK:CompSeq src) . (n + 1)) `1)) = min (((n + 1) + 1),(card (G .reachableDFrom src))) by Th21;
then 0 + (n + 1) = 1 + (n + 1) by A3, A6, A5, XXREAL_0:def 9;
hence contradiction ; :: thesis: verum

end;

hence k <= n ; :: thesis: verum

end;

set Gk = (DIJK:CompSeq src) . k;
set Gk1 = (DIJK:CompSeq src) . (k + 1);
A7: card (G .reachableDFrom src) <= (card (G .reachableDFrom src)) + 1 by NAT_1:11;
A8: (DIJK:CompSeq src) . (k + 1) = DIJK:Step ((DIJK:CompSeq src) . k) by Def11;
( card (dom (((DIJK:CompSeq src) . (k + 1)) `1)) = min (((card (G .reachableDFrom src)) + 1),(card (G .reachableDFrom src))) & card (dom (((DIJK:CompSeq src) . k) `1)) = min ((card (G .reachableDFrom src)),(card (G .reachableDFrom src))) ) by A1, Th21;
then card (dom (((DIJK:CompSeq src) . (k + 1)) `1)) = card (dom (((DIJK:CompSeq src) . k) `1)) by A7, XXREAL_0:def 9;
then DIJK:NextBestEdges ((DIJK:CompSeq src) . k) = {} by A8, Th15;
then (DIJK:CompSeq src) . k = (DIJK:CompSeq src) . (k + 1) by A8, Def8;
hence ((DIJK:CompSeq src) .Lifespan()) + 1 = card (G .reachableDFrom src) by A1, A2, GLIB_000:def 56; :: thesis: verum