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

now :: thesis: ( DIJK:NextBestEdges L <> {} implies [((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})] is DIJK:Labeling of G )

assume A1: DIJK:NextBestEdges L <> {} ; :: thesis: [((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})] is DIJK:Labeling of G
then the Element of DIJK:NextBestEdges L in DIJK:NextBestEdges L ;
then reconsider e9 = the Element of DIJK:NextBestEdges L as Element of the_Edges_of G ;
A2: the Element of DIJK:NextBestEdges L in DIJK:NextBestEdges L by A1;
then reconsider t9 = (the_Target_of G) . the Element of 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, ZFMISC_1:31;
then A3: (L `2) \/ { the Element of 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) . 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)))) = (dom (L `1)) \/ {((the_Target_of G) . the Element of DIJK:NextBestEdges L)} ) by Lm1;
then A4: dom ((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)))) c= the_Vertices_of G by XBOOLE_1:8;
rng ((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)))) c= REAL ;
then (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))) in PFuncs ((the_Vertices_of G),REAL) by A4, PARTFUN1:def 3;
hence [((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})] 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) . 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})] is DIJK:Labeling of G ) ) ; :: thesis: verum