set BE = DIJK:NextBestEdges L;
set e = choose (DIJK:NextBestEdges L);
set nE = (L `2 ) \/ {(choose (DIJK:NextBestEdges L))};
set V = the_Vertices_of G;
set E = the_Edges_of G;
set s = (the_Source_of G) . (choose (DIJK:NextBestEdges L));
set t = (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)));

now

assume S1: DIJK:NextBestEdges L <> {} ; :: thesis: [((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))})] is DIJK:Labeling of G
choose (DIJK:NextBestEdges L) in DIJK:NextBestEdges L by S1;
then reconsider e' = choose (DIJK:NextBestEdges L) as Element of the_Edges_of G ;
AAa: ( choose (DIJK:NextBestEdges L) in DIJK:NextBestEdges L & DIJK:NextBestEdges L c= the_Edges_of G ) by S1;
reconsider t' = (the_Target_of G) . (choose (DIJK:NextBestEdges L)) as Element of the_Vertices_of G by AAa, FUNCT_2:7;
A2: {t'} c= the_Vertices_of G ;
dom ((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)))))) = (dom (L `1 )) \/ {((the_Target_of G) . (choose (DIJK:NextBestEdges L)))} by Tw0;
then D1: dom ((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)))))) c= the_Vertices_of G by A2, XBOOLE_1:8;
rng ((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)))))) c= REAL ;
then A: (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))))) in PFuncs (the_Vertices_of G),REAL by D1, PARTFUN1:def 5;
E1a: L `2 in bool (the_Edges_of G) by MCART_1:10;
{e'} c= the_Edges_of G by AAa, ZFMISC_1:37;
then (L `2 ) \/ {(choose (DIJK:NextBestEdges L))} c= the_Edges_of G by E1a, XBOOLE_1:8;
hence [((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))})] is DIJK:Labeling of G by A, ZFMISC_1:def 2; :: thesis: verum

end;

hence ( ( DIJK:NextBestEdges L = {} implies L is DIJK:Labeling of G ) & ( not DIJK:NextBestEdges L = {} implies [((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))})] is DIJK:Labeling of G ) ) ; :: thesis: verum