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 :: thesis: for n being Nat st ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1)) holds
((DIJK:CompSeq src) . (n + 1)) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1))

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 = the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n);
set target = (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n);
set val = ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n));
set DnE = (((DIJK:CompSeq src) . n) `2) \/ { the Element of 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 :: thesis: for x being object st x in ((DIJK:CompSeq src) . (n + 1)) `2 holds
x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1))

let x be object ; :: 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 :: thesis: x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1))

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) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) .--> (((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))),((((DIJK:CompSeq src) . n) `2) \/ { the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)})] by A2, Def8;
then A7: ((DIJK:CompSeq src) . (n + 1)) `2 = (((DIJK:CompSeq src) . n) `2) \/ { the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)} ;
((DIJK:CompSeq src) . (n + 1)) `1 = (((DIJK:CompSeq src) . n) `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) .--> (((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) by A6;
then A8: dom (((DIJK:CompSeq src) . (n + 1)) `1) = (dom (((DIJK:CompSeq src) . n) `1)) \/ {((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))} by Lm1;
A9: the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) in DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A5;

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

per cases ( x in ((DIJK:CompSeq src) . n) `2 or x in { the Element of 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))

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

end;

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

then A11: x = the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by TARSKI:def 1;
then (the_Target_of G) . x in {((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))} by TARSKI:def 1;
then A12: (the_Target_of G) . x in dom (((DIJK:CompSeq src) . (n + 1)) `1) by A8, XBOOLE_0:def 3;
the Element of 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 A11;
hence x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1)) by A3, A9, A11, A12, GLIB_000:31; :: 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)) ; :: thesis: verum

end;

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