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 ));
(DIJK:CompSeq src) . 0 = DIJK:Init src by Def7;
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 A1: S₁[ 0 ] by TARSKI:def 3;

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 A2: ((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 ))
A3: (DIJK:CompSeq src) . (n + 1) = DIJK:Step ((DIJK:CompSeq src) . n) by Def7;

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 )) )
assume A5: x in ((DIJK:CompSeq src) . (n + 1)) `2 ; :: thesis: x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 ))
n <= n + 1 by NAT_1:12;
then A6: ( dom (((DIJK:CompSeq src) . n) `1 ) c= dom (((DIJK:CompSeq src) . (n + 1)) `1 ) & ((DIJK:CompSeq src) . n) `2 c= ((DIJK:CompSeq src) . (n + 1)) `2 ) by Th16;

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 A3, Def5;
hence x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 )) by A2, A5; :: thesis: verum

end;

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

then AAa: (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 A3, Def5;
A8: ((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 AAa, MCART_1:7;
A9: choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) in DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A7;
A11a: ((DIJK:CompSeq src) . (n + 1)) `2 = (((DIJK:CompSeq src) . n) `2 ) \/ {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))} by AAa, MCART_1:7;
A13: 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 Tw0, A8;

now

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

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

B1a: ((DIJK:CompSeq src) . n) `2 in bool (the_Edges_of G) by MCART_1:10;
( x in ((DIJK:CompSeq src) . n) `2 & (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 S1, A2, GLIB_000:34;
hence x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 )) by A6, B1a, 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 A14: 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 A15: (the_Target_of G) . x in dom (((DIJK:CompSeq src) . (n + 1)) `1 ) by A13, 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 A7, Def4;
then (the_Source_of G) . x in dom (((DIJK:CompSeq src) . n) `1 ) by A14, GLIB_000:def 18;
hence x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1 )) by A6, A9, A14, A15, 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 A16: for k being Nat st S₁[k] holds
S₁[k + 1] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A16);
hence for n being Nat holds ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1 )) ; :: thesis: verum