let G be finite real-weighted WGraph; :: thesis: for src being Vertex of G
for n being Nat holds dom (((DIJK:CompSeq src) . n) `1) c= G .reachableDFrom src
let src be Vertex of G; :: thesis: for n being Nat holds dom (((DIJK:CompSeq src) . n) `1) c= G .reachableDFrom src
set DCS = DIJK:CompSeq src;
defpred S₁[ Nat] means dom (((DIJK:CompSeq src) . $1) `1) c= G .reachableDFrom src;
(DIJK:CompSeq src) . 0 = DIJK:Init src by Def11;
then A1: dom (((DIJK:CompSeq src) . 0) `1) = {src} by Th17;

now

let k be Nat; :: thesis: ( dom (((DIJK:CompSeq src) . k) `1) c= G .reachableDFrom src implies dom (((DIJK:CompSeq src) . (k + 1)) `1) c= G .reachableDFrom src )
assume A2: dom (((DIJK:CompSeq src) . k) `1) c= G .reachableDFrom src ; :: thesis: dom (((DIJK:CompSeq src) . (k + 1)) `1) c= G .reachableDFrom src
set Gk = (DIJK:CompSeq src) . k;
set NextG = (DIJK:CompSeq src) . (k + 1);
set BestEdges = DIJK:NextBestEdges ((DIJK:CompSeq src) . k);
set e = choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k));
set NextEG = (((DIJK:CompSeq src) . k) `2) \/ {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k)))};
set v1 = (the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k)));
set target = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k)));
set pc = (((DIJK:CompSeq src) . k) `1) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k))));
set ec = (the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k)));
A3: (DIJK:CompSeq src) . (k + 1) = DIJK:Step ((DIJK:CompSeq src) . k) by Def11;

now

let x be set ; :: thesis: ( x in dom (((DIJK:CompSeq src) . (k + 1)) `1) implies x in G .reachableDFrom src )
assume A4: x in dom (((DIJK:CompSeq src) . (k + 1)) `1) ; :: thesis: x in G .reachableDFrom src

now

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

suppose DIJK:NextBestEdges ((DIJK:CompSeq src) . k) = {} ; :: thesis: x in G .reachableDFrom src

then (DIJK:CompSeq src) . k = (DIJK:CompSeq src) . (k + 1) by A3, Def8;
hence x in G .reachableDFrom src by A2, A4; :: thesis: verum

end;

suppose A5: DIJK:NextBestEdges ((DIJK:CompSeq src) . k) <> {} ; :: thesis: x in G .reachableDFrom src

set xx = x;
reconsider xx = x as Vertex of G by A4;
choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k)) DSJoins dom (((DIJK:CompSeq src) . k) `1),(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . k) `1)),G by A5, Def7;
then A6: (the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k))) in dom (((DIJK:CompSeq src) . k) `1) by GLIB_000:def 16;
then reconsider v19 = (the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k))) as Vertex of G ;
(DIJK:CompSeq src) . (k + 1) = [((((DIJK:CompSeq src) . k) `1) +* (((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k)))) .--> (((((DIJK:CompSeq src) . k) `1) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k))))))),((((DIJK:CompSeq src) . k) `2) \/ {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k)))})] by A3, A5, Def8;
then A7: ((DIJK:CompSeq src) . (k + 1)) `1 = (((DIJK:CompSeq src) . k) `1) +* (((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k)))) .--> (((((DIJK:CompSeq src) . k) `1) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k)))))) by MCART_1:7;

now

per cases ( xx in dom (((DIJK:CompSeq src) . k) `1) or not xx in dom (((DIJK:CompSeq src) . k) `1) ) ;

suppose xx in dom (((DIJK:CompSeq src) . k) `1) ; :: thesis: xx in G .reachableDFrom src

hence xx in G .reachableDFrom src by A2; :: thesis: verum

end;

suppose A8: not xx in dom (((DIJK:CompSeq src) . k) `1) ; :: thesis: xx in G .reachableDFrom src

A9: choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k)) in DIJK:NextBestEdges ((DIJK:CompSeq src) . k) by A5;
(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k))) = xx by A4, A7, A8, Lm2;
then choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . k)) DJoins v19,xx,G by A9, GLIB_000:def 14;
hence xx in G .reachableDFrom src by A2, A6, GLIB_002:19; :: thesis: verum

end;

end;

end;

hence x in G .reachableDFrom src ; :: thesis: verum

end;

end;

end;

hence x in G .reachableDFrom src ; :: thesis: verum

end;

hence dom (((DIJK:CompSeq src) . (k + 1)) `1) c= G .reachableDFrom src by TARSKI:def 3; :: thesis: verum

end;

then A10: for k being Nat st S₁[k] holds
S₁[k + 1] ;
src in G .reachableDFrom src by GLIB_002:18;
then A11: S₁[ 0 ] by A1, ZFMISC_1:31;
for n being Nat holds S₁[n] from NAT_1:sch 2(A11, A10);
hence for n being Nat holds dom (((DIJK:CompSeq src) . n) `1) c= G .reachableDFrom src ; :: thesis: verum