set V = the_Vertices_of G;
set E = the_Edges_of G;
set BE = DIJK:NextBestEdges L;
set e = choose (DIJK:NextBestEdges L);
set nE = (L `2) \/ {(choose (DIJK:NextBestEdges L))};
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 A1: 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
then choose (DIJK:NextBestEdges L) in DIJK:NextBestEdges L ;
then reconsider e9 = choose (DIJK:NextBestEdges L) as Element of the_Edges_of G ;
A2: choose (DIJK:NextBestEdges L) in DIJK:NextBestEdges L by A1;
then reconsider t9 = (the_Target_of G) . (choose (DIJK:NextBestEdges L)) as Element of the_Vertices_of G by FUNCT_2:5;
( L `2 in bool (the_Edges_of G) & {e9} c= the_Edges_of G ) by A2, MCART_1:10, ZFMISC_1:31;
then A3: (L `2) \/ {(choose (DIJK:NextBestEdges L))} c= the_Edges_of G by XBOOLE_1:8;
( {t9} 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 Lm1;
then A4: 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 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 (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 A4, PARTFUN1:def 3;
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 A3, 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