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 = choose (DIJK:NextBestEdges L);
set NextEG = (L `2) \/ {(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)));

now

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 A2: 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;

now

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

end;

hence dom (L `1) c= dom ((DIJK:Step L) `1) by TARSKI:def 3; :: thesis: L `2 c= (DIJK:Step L) `2

now

let x be set ; :: thesis: ( x in L `2 implies x in (DIJK:Step L) `2 )
assume A5: x in L `2 ; :: thesis: x in (DIJK:Step L) `2
( L `2 c= (L `2) \/ {(choose (DIJK:NextBestEdges L))} & (L `2) \/ {(choose (DIJK:NextBestEdges L))} = (DIJK:Step L) `2 ) by A2, MCART_1:7, XBOOLE_1:7;
hence x in (DIJK:Step L) `2 by A5; :: thesis: verum

end;

hence L `2 c= (DIJK:Step L) `2 by TARSKI:def 3; :: thesis: verum

end;

end;

end;

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