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 = choose (DIJK:NextBestEdges L);
set nextEG = (L `2 ) \/ {(choose (DIJK:NextBestEdges L))};
set nL = DIJK:Step L;
set src = (the_Source_of G) . (choose (DIJK:NextBestEdges L));
set target = (the_Target_of G) . (choose (DIJK:NextBestEdges L));
set val = ((L `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges L)))) + ((the_Weight_of G) . (choose (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

assume A2: DIJK:NextBestEdges L <> {} ; :: thesis: contradiction
then DIJK:Step L = [((L `1 ) +* (((the_Target_of G) . (choose (DIJK:NextBestEdges L))) .--> (((L `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges L)))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges L)))))),((L `2 ) \/ {(choose (DIJK:NextBestEdges L))})] by Def8;
then (DIJK:Step L) `1 = (L `1 ) +* (((the_Target_of G) . (choose (DIJK:NextBestEdges L))) .--> (((L `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges L)))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges L))))) by MCART_1:7;
then A3: dom ((DIJK:Step L) `1 ) = (dom (L `1 )) \/ {((the_Target_of G) . (choose (DIJK:NextBestEdges L)))} by Lm1;
choose (DIJK:NextBestEdges L) in DIJK:NextBestEdges L by A2;
then reconsider target = (the_Target_of G) . (choose (DIJK:NextBestEdges L)) as Vertex of G by FUNCT_2:7;
choose (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 )) by GLIB_000:def 18;
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:54;
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

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) . (choose (DIJK:NextBestEdges L))) .--> (((L `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges L)))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges L)))))),((L `2 ) \/ {(choose (DIJK:NextBestEdges L))})] by Def8;
then (DIJK:Step L) `1 = (L `1 ) +* (((the_Target_of G) . (choose (DIJK:NextBestEdges L))) .--> (((L `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges L)))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges L))))) by MCART_1:7;
then A6: dom ((DIJK:Step L) `1 ) = (dom (L `1 )) \/ {((the_Target_of G) . (choose (DIJK:NextBestEdges L)))} by Lm1;
choose (DIJK:NextBestEdges L) in DIJK:NextBestEdges L by A5;
then reconsider target = (the_Target_of G) . (choose (DIJK:NextBestEdges L)) as Vertex of G by FUNCT_2:7;
choose (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 )) by GLIB_000:def 18;
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:54; :: thesis: verum