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 A1: 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
choose (DIJK:NextBestEdges L) in DIJK:NextBestEdges L by A1;
then reconsider target = (the_Target_of G) . (choose (DIJK:NextBestEdges L)) as Vertex of G by FUNCT_2:7;

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