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)));
src in G .reachableDFrom src by GLIB_002:18;
then {src} c= G .reachableDFrom src by ZFMISC_1:31;
then card {src} <= card (G .reachableDFrom src) by NAT_1:43;
then A1: 0 + 1 <= card (G .reachableDFrom src) by CARD_1:30;

now :: thesis: for k being Nat st card (dom (((DIJK:CompSeq src) . k) `1)) = min ((k + 1),(card (G .reachableDFrom src))) holds
card (dom (((DIJK:CompSeq src) . (k + 1)) `1)) = min (((k + 1) + 1),(card (G .reachableDFrom src)))

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 A2: 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)))
set Gk = (DIJK:CompSeq src) . k;
set Gk1b = (DIJK:CompSeq src) . (k + 1);
set BestEdges = DIJK:NextBestEdges ((DIJK:CompSeq src) . k);
A3: (DIJK:CompSeq src) . (k + 1) = DIJK:Step ((DIJK:CompSeq src) . k) by Def11;

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

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

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

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

end;

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

then A7: dom (((DIJK:CompSeq src) . k) `1) <> G .reachableDFrom src by Th20;

A8: now :: thesis: not card (dom (((DIJK:CompSeq src) . k) `1)) = card (G .reachableDFrom src)

dom (((DIJK:CompSeq src) . k) `1) c= G .reachableDFrom src by Th19;
then A9: dom (((DIJK:CompSeq src) . k) `1) c< G .reachableDFrom src by A7, XBOOLE_0:def 8;
assume card (dom (((DIJK:CompSeq src) . k) `1)) = card (G .reachableDFrom src) ; :: thesis: contradiction
hence contradiction by A9, CARD_2:48; :: thesis: verum

end;

then k + 1 <= card (G .reachableDFrom src) by A2, XXREAL_0:def 9;
then A10: (k + 1) + 1 <= (card (G .reachableDFrom src)) + 1 by XREAL_1:6;
(k + 1) + 1 <> (card (G .reachableDFrom src)) + 1 by A2, A8;
then (k + 1) + 1 < (card (G .reachableDFrom src)) + 1 by A10, XXREAL_0:1;
then A11: (k + 1) + 1 <= card (G .reachableDFrom src) by NAT_1:13;
card (dom (((DIJK:CompSeq src) . (k + 1)) `1)) = (card (dom (((DIJK:CompSeq src) . k) `1))) + 1 by A3, A6, Th15;
then card (dom (((DIJK:CompSeq src) . (k + 1)) `1)) = (k + 1) + 1 by A2, A8, XXREAL_0:15;
hence card (dom (((DIJK:CompSeq src) . (k + 1)) `1)) = min (((k + 1) + 1),(card (G .reachableDFrom src))) by A11, 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 A12: for k being Nat st S₁[k] holds
S₁[k + 1] ;
(DIJK:CompSeq src) . 0 = DIJK:Init src by Def11;
then card (dom (((DIJK:CompSeq src) . 0) `1)) = card {src}
.= 1 by CARD_1:30 ;
then A13: S<sub>1</sub>[ 0 ] by A1, XXREAL_0:def 9;
for n being Nat holds S<sub>1</sub>[n] from NAT_1:sch 2(A13, A12);
hence for n being Nat holds card (dom (((DIJK:CompSeq src) . n) `1)) = min ((n + 1),(card (G .reachableDFrom src))) ; :: thesis: verum