let G be finite real-weighted WGraph; :: thesis: for s being Vertex of G
for n being Nat holds card (dom (((DIJK:CompSeq s) . n) `1 )) = min (n + 1),(card (G .reachableDFrom s))
let src be Vertex of G; :: thesis: for n being Nat holds card (dom (((DIJK:CompSeq src) . n) `1 )) = min (n + 1),(card (G .reachableDFrom src))
set DCS = DIJK:CompSeq src;
set VL0 = dom (((DIJK:CompSeq src) . 0 ) `1 );
set RFS = G .reachableDFrom src;
defpred S<sub>1</sub>[ Nat] means card (dom (((DIJK:CompSeq src) . $1) `1 )) = min ($1 + 1),(card (G .reachableDFrom src));
(DIJK:CompSeq src) . 0 = DIJK:Init src by Def7;
then A1: card (dom (((DIJK:CompSeq src) . 0 ) `1 )) = card {src} by Th15
.= 1 by CARD_1:50 ;
src in G .reachableDFrom src by GLIB_002:18;
then {src} c= G .reachableDFrom src by ZFMISC_1:37;
then card {src} <= card (G .reachableDFrom src) by NAT_1:44;
then 0 + 1 <= card (G .reachableDFrom src) by CARD_1:50;
then A2: S₁[ 0 ] by A1, XXREAL_0:def 9;

now

let k be Nat; :: thesis: ( card (dom (((DIJK:CompSeq src) . k) `1 )) = min (k + 1),(card (G .reachableDFrom src)) implies card (dom (((DIJK:CompSeq src) . (k + 1)) `1 )) = min ((k + 1) + 1),(card (G .reachableDFrom src)) )
assume A3: card (dom (((DIJK:CompSeq src) . k) `1 )) = min (k + 1),(card (G .reachableDFrom src)) ; :: thesis: card (dom (((DIJK:CompSeq src) . (k + 1)) `1 )) = min ((k + 1) + 1),(card (G .reachableDFrom src))
A4: (DIJK:CompSeq src) . (k + 1) = DIJK:Step ((DIJK:CompSeq src) . k) by Def7;
set Gk = (DIJK:CompSeq src) . k;
set Gk1b = (DIJK:CompSeq src) . (k + 1);
set BestEdges = DIJK:NextBestEdges ((DIJK:CompSeq src) . k);

now

per cases ( DIJK:NextBestEdges ((DIJK:CompSeq src) . k) = {} or DIJK:NextBestEdges ((DIJK:CompSeq src) . k) <> {} ) ;

suppose A5: DIJK:NextBestEdges ((DIJK:CompSeq src) . k) = {} ; :: thesis: card (dom (((DIJK:CompSeq src) . (k + 1)) `1 )) = min ((k + 1) + 1),(card (G .reachableDFrom src))

then A6: card (dom (((DIJK:CompSeq src) . (k + 1)) `1 )) = card (dom (((DIJK:CompSeq src) . k) `1 )) by A4, Th13;
A7: card (dom (((DIJK:CompSeq src) . k) `1 )) = card (G .reachableDFrom src) by A5, Th19;
A8: card (dom (((DIJK:CompSeq src) . (k + 1)) `1 )) = card (G .reachableDFrom src) by A5, A6, Th19;
card (G .reachableDFrom src) <= k + 1 by A3, A7, XXREAL_0:def 9;
then card (G .reachableDFrom src) <= (k + 1) + 1 by NAT_1:12;
hence card (dom (((DIJK:CompSeq src) . (k + 1)) `1 )) = min ((k + 1) + 1),(card (G .reachableDFrom src)) by A8, XXREAL_0:def 9; :: thesis: verum

end;

suppose A9: DIJK:NextBestEdges ((DIJK:CompSeq src) . k) <> {} ; :: thesis: card (dom (((DIJK:CompSeq src) . (k + 1)) `1 )) = min ((k + 1) + 1),(card (G .reachableDFrom src))

then A10: card (dom (((DIJK:CompSeq src) . (k + 1)) `1 )) = (card (dom (((DIJK:CompSeq src) . k) `1 ))) + 1 by A4, Th13;
A11: dom (((DIJK:CompSeq src) . k) `1 ) <> G .reachableDFrom src by A9, Th19;

A12: now

assume A13: card (dom (((DIJK:CompSeq src) . k) `1 )) = card (G .reachableDFrom src) ; :: thesis: contradiction
dom (((DIJK:CompSeq src) . k) `1 ) c= G .reachableDFrom src by Th18;
then dom (((DIJK:CompSeq src) . k) `1 ) c< G .reachableDFrom src by A11, XBOOLE_0:def 8;
hence contradiction by A13, CARD_2:67; :: thesis: verum

end;

then A14: card (dom (((DIJK:CompSeq src) . (k + 1)) `1 )) = (k + 1) + 1 by A3, A10, XXREAL_0:15;
( k + 1 <= card (G .reachableDFrom src) & k + 1 <> card (G .reachableDFrom src) ) by A3, A12, XXREAL_0:def 9;
then A15: (k + 1) + 1 <= (card (G .reachableDFrom src)) + 1 by XREAL_1:8;
(k + 1) + 1 <> (card (G .reachableDFrom src)) + 1 by A3, A12;
then (k + 1) + 1 < (card (G .reachableDFrom src)) + 1 by A15, XXREAL_0:1;
then (k + 1) + 1 <= card (G .reachableDFrom src) by NAT_1:13;
hence card (dom (((DIJK:CompSeq src) . (k + 1)) `1 )) = min ((k + 1) + 1),(card (G .reachableDFrom src)) by A14, XXREAL_0:def 9; :: thesis: verum

end;

end;

end;

hence card (dom (((DIJK:CompSeq src) . (k + 1)) `1 )) = min ((k + 1) + 1),(card (G .reachableDFrom src)) ; :: thesis: verum

end;

then A16: for k being Nat st S₁[k] holds
S₁[k + 1] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A16);
hence for n being Nat holds card (dom (((DIJK:CompSeq src) . n) `1 )) = min (n + 1),(card (G .reachableDFrom src)) ; :: thesis: verum