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 13;
set Gk = (DIJK:CompSeq src) . k;
set Gk1 = (DIJK:CompSeq src) . (k + 1);
A2: (DIJK:CompSeq src) . (k + 1) = DIJK:Step ((DIJK:CompSeq src) . k) by Def7;
A3: card (dom (((DIJK:CompSeq src) . (k + 1)) `1 )) = min ((card (G .reachableDFrom src)) + 1),(card (G .reachableDFrom src)) by A1, Th20;
A4: card (G .reachableDFrom src) <= (card (G .reachableDFrom src)) + 1 by NAT_1:11;
card (dom (((DIJK:CompSeq src) . k) `1 )) = min (card (G .reachableDFrom src)),(card (G .reachableDFrom src)) by A1, Th20;
then card (dom (((DIJK:CompSeq src) . (k + 1)) `1 )) = card (dom (((DIJK:CompSeq src) . k) `1 )) by A3, A4, XXREAL_0:def 9;
then DIJK:NextBestEdges ((DIJK:CompSeq src) . k) = {} by A2, Th13;
then A5: (DIJK:CompSeq src) . k = (DIJK:CompSeq src) . (k + 1) by A2, Def5;

now

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

now

assume n < k ; :: thesis: contradiction
then A7: n + 1 < card (G .reachableDFrom src) by A1, XREAL_1:10;
card (dom (((DIJK:CompSeq src) . n) `1 )) = min (n + 1),(card (G .reachableDFrom src)) by Th20;
then A8: card (dom (((DIJK:CompSeq src) . n) `1 )) = n + 1 by A7, XXREAL_0:def 9;
A9: card (dom (((DIJK:CompSeq src) . (n + 1)) `1 )) = min ((n + 1) + 1),(card (G .reachableDFrom src)) by Th20;
(n + 1) + 1 <= card (G .reachableDFrom src) by A7, NAT_1:13;
then 0 + (n + 1) = 1 + (n + 1) by A6, A8, A9, XXREAL_0:def 9;
hence contradiction ; :: thesis: verum

end;

hence k <= n ; :: thesis: verum

end;

hence ((DIJK:CompSeq src) .Lifespan() ) + 1 = card (G .reachableDFrom src) by A1, A5, GLIB_000:def 57; :: thesis: verum