let G be finite real-weighted WGraph; :: thesis: for src being Vertex of G
for n being Nat holds ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1 ))
let src be Vertex of G; :: thesis: for n being Nat holds ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1 ))
set DCS = DIJK:CompSeq src;
set D0 = (DIJK:CompSeq src) . 0 ;
defpred S₁[ Nat] means ((DIJK:CompSeq src) . $1) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . $1) `1 ));

now

let n be Nat; :: thesis: ( ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1 )) implies ((DIJK:CompSeq src) . (n + 1)) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 )) )
set Dn = (DIJK:CompSeq src) . n;
set Dn1 = (DIJK:CompSeq src) . (n + 1);
set BE = DIJK:NextBestEdges ((DIJK:CompSeq src) . n);
set e = choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n));
set target = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)));
set val = ((((DIJK:CompSeq src) . n) `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))));
set DnE = (((DIJK:CompSeq src) . n) `2 ) \/ {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))};
assume A1: ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1 )) ; :: thesis: ((DIJK:CompSeq src) . (n + 1)) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 ))
A2: (DIJK:CompSeq src) . (n + 1) = DIJK:Step ((DIJK:CompSeq src) . n) by Def11;

now

let x be set ; :: thesis: ( x in ((DIJK:CompSeq src) . (n + 1)) `2 implies x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 )) )
n <= n + 1 by NAT_1:12;
then A3: dom (((DIJK:CompSeq src) . n) `1 ) c= dom (((DIJK:CompSeq src) . (n + 1)) `1 ) by Th18;
assume A4: x in ((DIJK:CompSeq src) . (n + 1)) `2 ; :: thesis: x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 ))

now

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

suppose DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} ; :: thesis: x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 ))

then (DIJK:CompSeq src) . (n + 1) = (DIJK:CompSeq src) . n by A2, Def8;
hence x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 )) by A1, A4; :: thesis: verum

end;

suppose A5: DIJK:NextBestEdges ((DIJK:CompSeq src) . n) <> {} ; :: thesis: x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 ))

then A6: (DIJK:CompSeq src) . (n + 1) = [((((DIJK:CompSeq src) . n) `1 ) +* (((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) .--> (((((DIJK:CompSeq src) . n) `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))))),((((DIJK:CompSeq src) . n) `2 ) \/ {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))})] by A2, Def8;
then A7: ((DIJK:CompSeq src) . (n + 1)) `2 = (((DIJK:CompSeq src) . n) `2 ) \/ {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))} by MCART_1:7;
((DIJK:CompSeq src) . (n + 1)) `1 = (((DIJK:CompSeq src) . n) `1 ) +* (((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) .--> (((((DIJK:CompSeq src) . n) `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))))) by A6, MCART_1:7;
then A8: dom (((DIJK:CompSeq src) . (n + 1)) `1 ) = (dom (((DIJK:CompSeq src) . n) `1 )) \/ {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} by Lm1;
A9: choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) in DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A5;

now

per cases ( x in ((DIJK:CompSeq src) . n) `2 or x in {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))} ) by A4, A7, XBOOLE_0:def 3;

suppose A10: x in ((DIJK:CompSeq src) . n) `2 ; :: thesis: x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 ))

A11: ((DIJK:CompSeq src) . n) `2 in bool (the_Edges_of G) by MCART_1:10;
( (the_Source_of G) . x in dom (((DIJK:CompSeq src) . n) `1 ) & (the_Target_of G) . x in dom (((DIJK:CompSeq src) . n) `1 ) ) by A1, A10, GLIB_000:34;
hence x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 )) by A3, A10, A11, GLIB_000:34; :: thesis: verum

end;

suppose x in {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))} ; :: thesis: x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 ))

then A12: x = choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) by TARSKI:def 1;
then (the_Target_of G) . x in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} by TARSKI:def 1;
then A13: (the_Target_of G) . x in dom (((DIJK:CompSeq src) . (n + 1)) `1 ) by A8, XBOOLE_0:def 3;
choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) DSJoins dom (((DIJK:CompSeq src) . n) `1 ),(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1 )),G by A5, Def7;
then (the_Source_of G) . x in dom (((DIJK:CompSeq src) . n) `1 ) by A12, GLIB_000:def 18;
hence x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 )) by A3, A9, A12, A13, GLIB_000:34; :: thesis: verum

end;

end;

end;

hence x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 )) ; :: thesis: verum

end;

end;

end;

hence x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 )) ; :: thesis: verum

end;

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

end;

then A14: for k being Nat st S₁[k] holds
S₁[k + 1] ;
(DIJK:CompSeq src) . 0 = DIJK:Init src by Def11;
then for x being set st x in ((DIJK:CompSeq src) . 0 ) `2 holds
x in G .edgesBetween (dom (((DIJK:CompSeq src) . 0 ) `1 )) by MCART_1:7;
then A15: S₁[ 0 ] by TARSKI:def 3;
for n being Nat holds S₁[n] from NAT_1:sch 2(A15, A14);
hence for n being Nat holds ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1 )) ; :: thesis: verum