let G be real-weighted WGraph; :: thesis: for L being DIJK:Labeling of G holds
( dom (L `1) c= dom ((DIJK:Step L) `1) & L `2 c= (DIJK:Step L) `2 )
let L be DIJK:Labeling of G; :: thesis: ( dom (L `1) c= dom ((DIJK:Step L) `1) & L `2 c= (DIJK:Step L) `2 )
set nL = DIJK:Step L;
set BestEdges = DIJK:NextBestEdges L;
set e = the Element of DIJK:NextBestEdges L;
set NextEG = (L `2) \/ { 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);

now :: thesis: ( dom (L `1) c= dom ((DIJK:Step L) `1) & L `2 c= (DIJK:Step L) `2 )

per cases ( DIJK:NextBestEdges L = {} or DIJK:NextBestEdges L <> {} ) ;

suppose DIJK:NextBestEdges L = {} ; :: thesis: ( dom (L `1) c= dom ((DIJK:Step L) `1) & L `2 c= (DIJK:Step L) `2 )

hence ( dom (L `1) c= dom ((DIJK:Step L) `1) & L `2 c= (DIJK:Step L) `2 ) by Def8; :: thesis: verum

end;

suppose DIJK:NextBestEdges L <> {} ; :: thesis: ( dom (L `1) c= dom ((DIJK:Step L) `1) & L `2 c= (DIJK:Step L) `2 )

then A1: 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 A2: dom ((DIJK:Step L) `1) = (dom (L `1)) \/ {((the_Target_of G) . the Element of DIJK:NextBestEdges L)} by Lm1;

now :: thesis: for x being object st x in dom (L `1) holds
x in dom ((DIJK:Step L) `1)

let x be object ; :: thesis: ( x in dom (L `1) implies x in dom ((DIJK:Step L) `1) )
assume A3: x in dom (L `1) ; :: thesis: x in dom ((DIJK:Step L) `1)
dom (L `1) c= dom ((DIJK:Step L) `1) by A2, XBOOLE_1:7;
hence x in dom ((DIJK:Step L) `1) by A3; :: thesis: verum

end;

hence dom (L `1) c= dom ((DIJK:Step L) `1) ; :: thesis: L `2 c= (DIJK:Step L) `2

now :: thesis: for x being object st x in L `2 holds
x in (DIJK:Step L) `2

let x be object ; :: thesis: ( x in L `2 implies x in (DIJK:Step L) `2 )
assume A4: x in L `2 ; :: thesis: x in (DIJK:Step L) `2
( L `2 c= (L `2) \/ { the Element of DIJK:NextBestEdges L} & (L `2) \/ { the Element of DIJK:NextBestEdges L} = (DIJK:Step L) `2 ) by A1, XBOOLE_1:7;
hence x in (DIJK:Step L) `2 by A4; :: thesis: verum

end;

hence L `2 c= (DIJK:Step L) `2 ; :: thesis: verum

end;

end;

end;

hence ( dom (L `1) c= dom ((DIJK:Step L) `1) & L `2 c= (DIJK:Step L) `2 ) ; :: thesis: verum