let G be _finite real-weighted WGraph; :: thesis: for L being DIJK:Labeling of G holds
( ( card (dom ((DIJK:Step L) `1)) = card (dom (L `1)) implies DIJK:NextBestEdges L = {} ) & ( DIJK:NextBestEdges L = {} implies card (dom ((DIJK:Step L) `1)) = card (dom (L `1)) ) & ( card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 implies DIJK:NextBestEdges L <> {} ) & ( DIJK:NextBestEdges L <> {} implies card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 ) )
let L be DIJK:Labeling of G; :: thesis: ( ( card (dom ((DIJK:Step L) `1)) = card (dom (L `1)) implies DIJK:NextBestEdges L = {} ) & ( DIJK:NextBestEdges L = {} implies card (dom ((DIJK:Step L) `1)) = card (dom (L `1)) ) & ( card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 implies DIJK:NextBestEdges L <> {} ) & ( DIJK:NextBestEdges L <> {} implies card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 ) )
set BestEdges = DIJK:NextBestEdges L;
set e = the Element of DIJK:NextBestEdges L;
set nextEG = (L `2) \/ { the Element of DIJK:NextBestEdges L};
set nL = DIJK:Step L;
set src = (the_Source_of G) . the Element of DIJK:NextBestEdges L;
set target = (the_Target_of G) . the Element of DIJK:NextBestEdges L;
set val = ((L `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges L)) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges L);

hereby :: thesis: ( ( DIJK:NextBestEdges L = {} implies card (dom ((DIJK:Step L) `1)) = card (dom (L `1)) ) & ( card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 implies DIJK:NextBestEdges L <> {} ) & ( DIJK:NextBestEdges L <> {} implies card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 ) )

assume A1: card (dom ((DIJK:Step L) `1)) = card (dom (L `1)) ; :: thesis: DIJK:NextBestEdges L = {}

now :: thesis: not DIJK:NextBestEdges L <> {}

assume A2: DIJK:NextBestEdges L <> {} ; :: thesis: contradiction
then DIJK:Step L = [((L `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges L) .--> (((L `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges L)) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges L)))),((L `2) \/ { the Element of DIJK:NextBestEdges L})] by Def8;
then (DIJK:Step L) `1 = (L `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges L) .--> (((L `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges L)) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges L))) ;
then A3: dom ((DIJK:Step L) `1) = (dom (L `1)) \/ {((the_Target_of G) . the Element of DIJK:NextBestEdges L)} by Lm1;
the Element of DIJK:NextBestEdges L in DIJK:NextBestEdges L by A2;
then reconsider target = (the_Target_of G) . the Element of DIJK:NextBestEdges L as Vertex of G by FUNCT_2:5;
the Element of DIJK:NextBestEdges L DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G by A2, Def7;
then target in (the_Vertices_of G) \ (dom (L `1)) ;
then not target in dom (L `1) by XBOOLE_0:def 5;
then card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 by A3, CARD_2:41;
hence contradiction by A1; :: thesis: verum

end;

hence DIJK:NextBestEdges L = {} ; :: thesis: verum

end;

thus ( DIJK:NextBestEdges L = {} implies card (dom ((DIJK:Step L) `1)) = card (dom (L `1)) ) by Def8; :: thesis: ( card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 iff DIJK:NextBestEdges L <> {} )

hereby :: thesis: ( DIJK:NextBestEdges L <> {} implies card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 )

assume A4: card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 ; :: thesis: DIJK:NextBestEdges L <> {}

now :: thesis: not DIJK:NextBestEdges L = {}

assume DIJK:NextBestEdges L = {} ; :: thesis: contradiction
then 0 + (card (dom (L `1))) = (card (dom (L `1))) + 1 by A4, Def8;
hence contradiction ; :: thesis: verum

end;

hence DIJK:NextBestEdges L <> {} ; :: thesis: verum

end;

assume A5: DIJK:NextBestEdges L <> {} ; :: thesis: card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1
then DIJK:Step L = [((L `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges L) .--> (((L `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges L)) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges L)))),((L `2) \/ { the Element of DIJK:NextBestEdges L})] by Def8;
then (DIJK:Step L) `1 = (L `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges L) .--> (((L `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges L)) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges L))) ;
then A6: dom ((DIJK:Step L) `1) = (dom (L `1)) \/ {((the_Target_of G) . the Element of DIJK:NextBestEdges L)} by Lm1;
the Element of DIJK:NextBestEdges L in DIJK:NextBestEdges L by A5;
then reconsider target = (the_Target_of G) . the Element of DIJK:NextBestEdges L as Vertex of G by FUNCT_2:5;
the Element of DIJK:NextBestEdges L DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G by A5, Def7;
then target in (the_Vertices_of G) \ (dom (L `1)) ;
then not target in dom (L `1) by XBOOLE_0:def 5;
hence card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 by A6, CARD_2:41; :: thesis: verum