let G be finite nonnegative-weighted WGraph; :: thesis:
let src be Vertex of G; :: thesis:
set DCS = DIJK:CompSeq src;
set D0 = (DIJK:CompSeq src) . 0 ;
defpred S₁[ Nat] means for G2 being inducedWSubgraph of G, dom (((DIJK:CompSeq src) . $1) `1 ),((DIJK:CompSeq src) . $1) `2 holds
( G2 is_mincost_DTree_rooted_at src & ( for v being Vertex of G st v in dom (((DIJK:CompSeq src) . $1) `1 ) holds
G .min_DPath_cost src,v = (((DIJK:CompSeq src) . $1) `1 ) . v ) );
reconsider EL = {} as PartFunc of (the_Edges_of G),REAL by RELSET_1:25;
A1: (DIJK:CompSeq src) . 0 = DIJK:Init src by Def7;
then A2: ((DIJK:CompSeq src) . 0 ) `1 = src .--> 0 by MCART_1:7;
then A3: dom (((DIJK:CompSeq src) . 0 ) `1 ) = {src} by FUNCOP_1:19;
A4: ((DIJK:CompSeq src) . 0 ) `2 = {} by A1, MCART_1:7;

now

let D0W be inducedWSubgraph of G, dom (((DIJK:CompSeq src) . 0 ) `1 ),((DIJK:CompSeq src) . 0 ) `2 ; :: thesis:
{} c= G .edgesBetween (dom (((DIJK:CompSeq src) . 0 ) `1 )) by XBOOLE_1:2;
then A5: ( the_Vertices_of D0W = {src} & the_Edges_of D0W = {} ) by A3, A4, GLIB_000:def 39;
then A6: ( card (the_Vertices_of D0W) = 1 & card (the_Edges_of D0W) = 0 ) by CARD_1:50;
A7: D0W .order() = (D0W .size() ) + 1 by A5, CARD_1:47, CARD_1:50;
D0W is trivial by A6, GLIB_000:def 21;
then A8: D0W is Tree-like by A7, GLIB_002:47;

now

let x be Vertex of D0W; :: thesis:
A9: x = src by A5, TARSKI:def 1;
set W2 = D0W .walkOf x;
take W2 = D0W .walkOf x; :: thesis:
thus W2 is_Walk_from src,x by A9, GLIB_001:14; :: thesis:
let W1 be DPath of G; :: thesis:
assume W1 is_Walk_from src,x ; :: thesis:
0 <= W1 .cost() by GLIB_003:36;
hence W2 .cost() <= W1 .cost() by GLIB_003:28; :: thesis:

end;

hence D0W is_mincost_DTree_rooted_at src by A8, Def1; :: thesis:
let v be Vertex of G; :: thesis:
assume A10: v in dom (((DIJK:CompSeq src) . 0 ) `1 ) ; :: thesis:
then A11: v = src by A3, TARSKI:def 1;
A12: (((DIJK:CompSeq src) . 0 ) `1 ) . src = 0 by A2, FUNCOP_1:87;

now

set W1 = G .walkOf v;
A13: G .walkOf v is_Walk_from src,v by A11, GLIB_001:14;
then consider W being DPath of G such that
A14: ( W is_mincost_DPath_from src,v & G .min_DPath_cost src,v = W .cost() ) by Def3;
(G .walkOf v) .cost() = 0 by GLIB_003:28;
then W .cost() <= 0 by A13, A14, Def2;
hence G .min_DPath_cost src,v = 0 by A14, GLIB_003:36; :: thesis:

end;

hence G .min_DPath_cost src,v = (((DIJK:CompSeq src) . 0 ) `1 ) . v by A3, A10, A12, TARSKI:def 1; :: thesis:

end;

then A15: S₁[ 0 ] ;

now

let n be Nat; :: thesis:
set Dn = (DIJK:CompSeq src) . n;
set Dn1 = (DIJK:CompSeq src) . (n + 1);
set BE = DIJK:NextBestEdges ((DIJK:CompSeq src) . n);
set e = choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n));
set source = (the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)));
set target = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)));
set DnE = (((DIJK:CompSeq src) . n) `2 ) \/ {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))};
set pc = (((DIJK:CompSeq src) . n) `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))));
set ec = (the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)));
consider DnW being inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1 ),((DIJK:CompSeq src) . n) `2 ;
assume A16: S₁[n] ; :: thesis:
let Dn1W be inducedWSubgraph of G, dom (((DIJK:CompSeq src) . (n + 1)) `1 ),((DIJK:CompSeq src) . (n + 1)) `2 ; :: thesis:
A17: (DIJK:CompSeq src) . (n + 1) = DIJK:Step ((DIJK:CompSeq src) . n) by Def7;
A21: src in dom (((DIJK:CompSeq src) . 0 ) `1 ) by A3, TARSKI:def 1;
A23: dom (((DIJK:CompSeq src) . 0 ) `1 ) c= dom (((DIJK:CompSeq src) . n) `1 ) by Th16;
A25: ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1 )) by Th21;
A26: ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1 )) by Th21;
then A27: ( the_Vertices_of DnW = dom (((DIJK:CompSeq src) . n) `1 ) & the_Edges_of DnW = ((DIJK:CompSeq src) . n) `2 ) by A21, A23, GLIB_000:def 39;
A28: ( card (dom (((DIJK:CompSeq src) . n) `1 )) = DnW .order() & card (((DIJK:CompSeq src) . n) `2 ) = DnW .size() ) by A21, A23, A25, GLIB_000:def 39;
A29: DnW is_mincost_DTree_rooted_at src by A16;
then A30: DnW is Tree-like by Def1;

now

per cases ;

suppose DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} ; :: thesis:

then (DIJK:CompSeq src) . (n + 1) = (DIJK:CompSeq src) . n by A17, Def5;
hence ( Dn1W is_mincost_DTree_rooted_at src & ( for v being Vertex of G st v in dom (((DIJK:CompSeq src) . (n + 1)) `1 ) holds
G .min_DPath_cost src,v = (((DIJK:CompSeq src) . (n + 1)) `1 ) . v ) ) by A16; :: thesis:

end;

suppose A32: DIJK:NextBestEdges ((DIJK:CompSeq src) . n) <> {} ; :: thesis:

A48: now

thus ( the_Vertices_of DnW c= the_Vertices_of Dn1W & the_Edges_of DnW c= the_Edges_of Dn1W ) by A27, A40, XBOOLE_1:7; :: thesis:
let e be set ; :: thesis:
assume A49: e in the_Edges_of DnW ; :: thesis:
then A50: e in the_Edges_of Dn1W by A27, A40, XBOOLE_0:def 3;
( (the_Source_of DnW) . e = (the_Source_of G) . e & (the_Target_of DnW) . e = (the_Target_of G) . e ) by A49, GLIB_000:def 34;
hence ( (the_Source_of DnW) . e = (the_Source_of Dn1W) . e & (the_Target_of DnW) . e = (the_Target_of Dn1W) . e ) by A50, GLIB_000:def 34; :: thesis:

end;

then A52: DnW is Subgraph of Dn1W by GLIB_000:def 34;
reconsider DnW' = DnW as [Weighted] Subgraph of Dn1W by A48, GLIB_000:def 34;
A53: the_Weight_of DnW' = (the_Weight_of G) | (the_Edges_of DnW) by GLIB_003:def 10;
A54: the_Weight_of Dn1W = (the_Weight_of G) | (the_Edges_of Dn1W) by GLIB_003:def 10;
dom (the_Weight_of Dn1W) = the_Edges_of Dn1W by PARTFUN1:def 4;
then (dom (the_Weight_of Dn1W)) /\ (the_Edges_of DnW) = the_Edges_of DnW by A48, XBOOLE_1:28;
then A55: dom (the_Weight_of DnW') = (dom (the_Weight_of Dn1W)) /\ (the_Edges_of DnW) by PARTFUN1:def 4;

now

let y be set ; :: thesis:
assume y in dom (the_Weight_of DnW') ; :: thesis:
then A56: y in the_Edges_of DnW by PARTFUN1:def 4;
hence (the_Weight_of DnW') . y = (the_Weight_of G) . y by A53, FUNCT_1:72
.= (the_Weight_of Dn1W) . y by A48, A54, A56, FUNCT_1:72 ;
:: thesis:

end;

now

let u, v be Vertex of Dn1W; :: thesis:

A62: now

let u, v be set ; :: thesis:
assume ( u in dom (((DIJK:CompSeq src) . n) `1 ) & v in dom (((DIJK:CompSeq src) . n) `1 ) ) ; :: thesis:
then reconsider u' = u, v' = v as Vertex of DnW by A26, GLIB_000:def 39;
consider W1 being Walk of DnW such that
A63: W1 is_Walk_from u',v' by A30, GLIB_002:def 1;
reconsider W2 = W1 as Walk of Dn1W by A52, GLIB_001:168;
W2 is_Walk_from u,v by A63, GLIB_001:20;
hence ex W being Walk of Dn1W st W is_Walk_from u,v ; :: thesis:

end;

now

per cases by A40, XBOOLE_0:def 3;

suppose ( u in dom (((DIJK:CompSeq src) . n) `1 ) & v in dom (((DIJK:CompSeq src) . n) `1 ) ) ; :: thesis:

hence ex W being Walk of Dn1W st W is_Walk_from u,v by A62; :: thesis:

end;

suppose A64: ( u in dom (((DIJK:CompSeq src) . n) `1 ) & v in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} ) ; :: thesis:

then consider W being Walk of Dn1W such that
A65: W is_Walk_from u,(the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A58, A62;
A66: W .addEdge (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) is_Walk_from u,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A61, A65, GLIB_001:67;
v = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A64, TARSKI:def 1;
hence ex W being Walk of Dn1W st W is_Walk_from u,v by A66; :: thesis:

end;

suppose A67: ( u in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} & v in dom (((DIJK:CompSeq src) . n) `1 ) ) ; :: thesis:

then consider W being Walk of Dn1W such that
A68: W is_Walk_from v,(the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A58, A62;
W .addEdge (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) is_Walk_from v,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A61, A68, GLIB_001:67;
then W .addEdge (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) is_Walk_from v,u by A67, TARSKI:def 1;
then (W .addEdge (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) .reverse() is_Walk_from u,v by GLIB_001:24;
hence ex W being Walk of Dn1W st W is_Walk_from u,v ; :: thesis:

end;

suppose ( u in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} & v in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} ) ; :: thesis:

then A69: ( u = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) & v = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) ) by TARSKI:def 1;
take W = Dn1W .walkOf u; :: thesis:
thus W is_Walk_from u,v by A69, GLIB_001:14; :: thesis:

end;

hence ex W being Walk of Dn1W st W is_Walk_from u,v ; :: thesis:

end;

then Dn1W is connected by GLIB_002:def 1;
then A70: Dn1W is Tree-like by A46, GLIB_002:47;

now

consider WT being DPath of DnW such that
A71: ( WT is_Walk_from src,(the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) & ( for W1 being DPath of G st W1 is_Walk_from src,(the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) holds
WT .cost() <= W1 .cost() ) ) by A27, A29, A58, Def1;
reconsider WT' = WT as DPath of Dn1W by A52, GLIB_001:176;
set W2 = WT' .addEdge (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)));
A72: WT' is_Walk_from src,(the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A71, GLIB_001:20;
then reconsider W2 = WT' .addEdge (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) as DWalk of Dn1W by A60, GLIB_001:124;

now

(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} by TARSKI:def 1;
hence (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) is Vertex of Dn1W by A40, XBOOLE_0:def 3; :: thesis:
thus choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) Joins WT' .last() ,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))),Dn1W by A61, A72, GLIB_001:def 23; :: thesis:
A73: not choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) in the_Edges_of DnW by A21, A23, A25, A45, GLIB_000:def 39;
WT .edges() = WT' .edges() by GLIB_001:111;
hence not choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) in WT' .edges() by A73; :: thesis:

now

assume A74: not WT' is trivial ; :: thesis:

now

assume WT' is closed ; :: thesis:
then WT' is Cycle-like by A74, GLIB_001:def 31;
hence contradiction by A70, GLIB_002:def 2; :: thesis:

end;

hence not WT' is closed ; :: thesis:

end;

hence ( WT' is trivial or not WT' is closed ) ; :: thesis:
WT' .vertices() = WT .vertices() by GLIB_001:99;
then A76: not (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) in WT' .vertices() by A27, A42, XBOOLE_0:def 5;
let n be odd Element of NAT ; :: thesis:
assume ( 1 < n & n <= len WT' ) ; :: thesis:
hence WT' . n <> (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A76, GLIB_001:88; :: thesis:

end;

then reconsider W2 = W2 as DPath of Dn1W by GLIB_001:151;
take W2 = W2; :: thesis:
thus W2 is_Walk_from src,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A61, A72, GLIB_001:67; :: thesis:

now

end;

hence W2 .cost() = ((((DIJK:CompSeq src) . n) `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) by GLIB_003:32; :: thesis:

end;

now

consider WB being DPath of G such that
A87: ( WB is_mincost_DPath_from src,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) & G .min_DPath_cost src,((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) = WB .cost() ) by A84, Def3;
A88: ( WB is_Walk_from src,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) & ( for WA being DPath of G st WA is_Walk_from src,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) holds
WB .cost() <= WA .cost() ) ) by A87, Def2;
thus G .min_DPath_cost src,((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) <= ((((DIJK:CompSeq src) . n) `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) by A84, A85, A87, Def2; :: thesis:
( WB .first() = src & WB .last() = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) ) by A88, GLIB_001:def 23;
then consider lenWB2h being odd Element of NAT such that
A89: ( lenWB2h = (len WB) - 2 & (WB .cut 1,lenWB2h) .addEdge (WB . (lenWB2h + 1)) = WB ) by A86, GLIB_001:128, GLIB_001:134;
set WA = WB .cut 1,lenWB2h;
set sa = WB . lenWB2h;
set ea = WB . (lenWB2h + 1);
A90: ( 1 <= lenWB2h & not 1 is even ) by HEYTING3:1, JORDAN12:3;
A91: lenWB2h < (len WB) - 0 by A89, XREAL_1:17;
A92: WB . 1 = WB .first() by GLIB_001:def 6
.= src by A88, GLIB_001:def 23 ;
then WB .cut 1,lenWB2h is_Walk_from src,WB . lenWB2h by A90, A91, GLIB_001:38;
then reconsider sa = WB . lenWB2h as Vertex of G by GLIB_001:19;
reconsider target' = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) as Vertex of G by A88, GLIB_001:19;
A93: WB . (lenWB2h + 1) DJoins sa,WB . (lenWB2h + 2),G by A91, GLIB_001:123;
then A94a: WB . (lenWB2h + 1) DJoins sa,WB .last() ,G by A89, GLIB_001:def 7;
then WB . (lenWB2h + 1) DJoins sa,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))),G by A88, GLIB_001:def 23;
then WB . (lenWB2h + 1) Joins sa,target',G by GLIB_000:19;
then WB . (lenWB2h + 1) in sa .edgesInOut() by GLIB_000:65;
then A95: WB . (lenWB2h + 1) in ((WB .cut 1,lenWB2h) .last() ) .edgesInOut() by A90, A91, GLIB_001:38;
then A96: G .min_DPath_cost src,((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) = ((WB .cut 1,lenWB2h) .cost() ) + ((the_Weight_of G) . (WB . (lenWB2h + 1))) by A87, A89, GLIB_003:32;
reconsider WA = WB .cut 1,lenWB2h as DPath of G ;
A97: ( WA .first() = src & WA .last() = sa ) by A90, A91, A92, GLIB_001:38;
then A98: WA is_mincost_DPath_from src,sa by A87, Th10;
A99: WA .cost() = G .min_DPath_cost src,sa by A87, A97, Th10, Th12;
A100: WB . (lenWB2h + 1) DJoins sa,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))),G by A88, A94a, GLIB_001:def 23;

now

assume A101: G .min_DPath_cost src,((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) < ((((DIJK:CompSeq src) . n) `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) ; :: thesis:
defpred S₂[ Nat] means ( not $1 is even & $1 <= len WA & not WA . $1 in dom (((DIJK:CompSeq src) . n) `1 ) );

A102: now

assume A103: not sa in dom (((DIJK:CompSeq src) . n) `1 ) ; :: thesis:
sa = WA .last() by A90, A91, GLIB_001:38
.= WA . (len WA) by GLIB_001:def 7 ;
then A104: ex k being Nat st S₂[k] by A103;
consider k being Nat such that
A105: ( S₂[k] & ( for m being Nat st S₂[m] holds
k <= m ) ) from NAT_1:sch 5(A104);
reconsider k = k as odd Element of NAT by A105, ORDINAL1:def 13;
WA . 1 = WA .first() by GLIB_001:def 6
.= src by A90, A91, A92, GLIB_001:38 ;
then A106: k <> 1 by A21, A23, A105;
1 <= k by HEYTING3:1;
then 1 < k by A106, XXREAL_0:1;
then 1 + 1 < k + 1 by XREAL_1:10;
then 2 <= k by NAT_1:13;
then reconsider k2a = k - (2 * 1) as odd Element of NAT by INT_1:18;
set sk = WA . k2a;
set ek = WA . (k2a + 1);
set tk = WA . k;
A107: ( not 1 is even & 1 <= k2a & k2a < (len WA) - 0 ) by A105, HEYTING3:1, JORDAN12:3, XREAL_1:17;
A108a: k2a < k - 0 by XREAL_1:17;
then A108: WA . k2a in dom (((DIJK:CompSeq src) . n) `1 ) by A105, A107;
then reconsider sk = WA . k2a as Vertex of G ;
reconsider tk = WA . k as Vertex of G by A105, GLIB_001:8;
set WK1 = WA .cut 1,k2a;
set WKA = WA .cut 1,k;
set WKB = WA .cut k,(len WA);
reconsider WK1 = WA .cut 1,k2a, WKA = WA .cut 1,k, WKB = WA .cut k,(len WA) as DPath of G ;
tk = WA . (k2a + 2) ;
then A109: WA . (k2a + 1) DJoins sk,tk,G by A107, GLIB_001:123;
then A110: ( WA . (k2a + 1) in the_Edges_of G & (the_Source_of G) . (WA . (k2a + 1)) = sk & (the_Target_of G) . (WA . (k2a + 1)) = tk ) by GLIB_000:def 16;
A111: ( WK1 .first() = WA . 1 & WK1 .last() = sk ) by A107, GLIB_001:38;
then WK1 is_mincost_DPath_from WA . 1,sk by A98, Th10;
then WK1 is_mincost_DPath_from WA .first() ,sk by GLIB_001:def 6;
then G .min_DPath_cost src,sk = WK1 .cost() by A97, Th12;
then A112: (((DIJK:CompSeq src) . n) `1 ) . sk = WK1 .cost() by A16, A108a, A105, A107;
tk in (the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1 )) by A105, XBOOLE_0:def 5;
then WA . (k2a + 1) DSJoins dom (((DIJK:CompSeq src) . n) `1 ),(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1 )),G by A108, A110, GLIB_000:def 18;
then A113: ((((DIJK:CompSeq src) . n) `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) <= (WK1 .cost() ) + ((the_Weight_of G) . (WA . (k2a + 1))) by A32, A110, A112, Def4;
k2a + 2 = k ;
then A114: WK1 .addEdge (WA . (k2a + 1)) = WKA by A107, GLIB_001:42;
( WA . (k2a + 1) in the_Edges_of G & (the_Source_of G) . (WA . (k2a + 1)) = sk & (the_Target_of G) . (WA . (k2a + 1)) = tk ) by A109, GLIB_000:def 16;
then WA . (k2a + 1) in sk .edgesInOut() by GLIB_000:64;
then A115: ((((DIJK:CompSeq src) . n) `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) <= WKA .cost() by A111, A113, A114, GLIB_003:32;
A116: ( 1 <= k & k <= len WA ) by A105, HEYTING3:1;
then A117: WKA .append WKB = WA .cut 1,(len WA) by GLIB_001:39, JORDAN12:3
.= WA by GLIB_001:40 ;
WKB .first() = WA . k by A105, GLIB_001:38
.= WKA .last() by A116, GLIB_001:38, JORDAN12:3 ;
then A118: WA .cost() = (WKA .cost() ) + (WKB .cost() ) by A117, GLIB_003:31;
0 <= WKB .cost() by GLIB_003:36;
then 0 + (WKA .cost() ) <= WA .cost() by A118, XREAL_1:9;
then A119: ((((DIJK:CompSeq src) . n) `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) <= WA .cost() by A115, XXREAL_0:2;
WB . (lenWB2h + 1) in the_Edges_of G by A93, GLIB_000:def 16;
then 0 <= (the_Weight_of G) . (WB . (lenWB2h + 1)) by GLIB_003:38;
then (((((DIJK:CompSeq src) . n) `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + 0 <= (WA .cost() ) + ((the_Weight_of G) . (WB . (lenWB2h + 1))) by A119, XREAL_1:9;
hence contradiction by A87, A89, A95, A101, GLIB_003:32; :: thesis:

end;

then A120: WA .cost() = (((DIJK:CompSeq src) . n) `1 ) . sa by A16, A99;
A121: ( WB . (lenWB2h + 1) in the_Edges_of G & (the_Source_of G) . (WB . (lenWB2h + 1)) = sa & (the_Target_of G) . (WB . (lenWB2h + 1)) = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) ) by A100, GLIB_000:def 16;
then WB . (lenWB2h + 1) DSJoins dom (((DIJK:CompSeq src) . n) `1 ),(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1 )),G by A42, A102, GLIB_000:def 18;
hence contradiction by A32, A96, A101, A120, A121, Def4; :: thesis:

end;

hence G .min_DPath_cost src,((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) >= ((((DIJK:CompSeq src) . n) `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) ; :: thesis:

end;

then A122: G .min_DPath_cost src,((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) = ((((DIJK:CompSeq src) . n) `1 ) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) by XXREAL_0:1;

now

let x be Vertex of Dn1W; :: thesis:

now

per cases by A40, XBOOLE_0:def 3;

suppose x in dom (((DIJK:CompSeq src) . n) `1 ) ; :: thesis:

then reconsider x' = x as Vertex of DnW by A26, GLIB_000:def 39;
DnW is_mincost_DTree_rooted_at src by A16;
then consider W2 being DPath of DnW such that
A123: ( W2 is_Walk_from src,x' & ( for W1 being DPath of G st W1 is_Walk_from src,x' holds
W2 .cost() <= W1 .cost() ) ) by Def1;
reconsider W2' = W2 as DPath of Dn1W by A52, GLIB_001:176;
take W2' = W2'; :: thesis:
thus W2' is_Walk_from src,x by A123, GLIB_001:20; :: thesis:
let W1 be DPath of G; :: thesis:
assume W1 is_Walk_from src,x ; :: thesis:
then W2 .cost() <= W1 .cost() by A123;
hence W2' .cost() <= W1 .cost() by A57, GLIB_003:34; :: thesis:

end;

suppose A124: x in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} ; :: thesis:

then A125: x = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by TARSKI:def 1;
take W2 = W2; :: thesis:
thus W2 is_Walk_from src,x by A83, A124, TARSKI:def 1; :: thesis:
let W1 be DPath of G; :: thesis:
assume A126: W1 is_Walk_from src,x ; :: thesis:
consider WX being DPath of G such that
A127: ( WX is_mincost_DPath_from src,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) & WX .cost() = W2 .cost() ) by A83, A84, A122, Def3;
thus W2 .cost() <= W1 .cost() by A125, A126, A127, Def2; :: thesis:

end;

hence ex W2 being DPath of Dn1W st
( W2 is_Walk_from src,x & ( for W1 being DPath of G st W1 is_Walk_from src,x holds
W2 .cost() <= W1 .cost() ) ) ; :: thesis:

end;

hence Dn1W is_mincost_DTree_rooted_at src by A70, Def1; :: thesis:
let v be Vertex of G; :: thesis:
assume A128: v in dom (((DIJK:CompSeq src) . (n + 1)) `1 ) ; :: thesis:

now

per cases by A35, A128, XBOOLE_0:def 3;

suppose A129: v in dom (((DIJK:CompSeq src) . n) `1 ) ; :: thesis:

end;

suppose A133: v in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} ; :: thesis:

end;

hence G .min_DPath_cost src,v = (((DIJK:CompSeq src) . (n + 1)) `1 ) . v ; :: thesis:

end;

hence ( Dn1W is_mincost_DTree_rooted_at src & ( for v being Vertex of G st v in dom (((DIJK:CompSeq src) . (n + 1)) `1 ) holds
G .min_DPath_cost src,v = (((DIJK:CompSeq src) . (n + 1)) `1 ) . v ) ) ; :: thesis:

end;

then A137: for k being Nat st S₁[k] holds
S₁[k + 1] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A15, A137);
hence for n being Nat
for G2 being inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1 ),((DIJK:CompSeq src) . n) `2 holds
( G2 is_mincost_DTree_rooted_at src & ( for v being Vertex of G st v in dom (((DIJK:CompSeq src) . n) `1 ) holds
G .min_DPath_cost src,v = (((DIJK:CompSeq src) . n) `1 ) . v ) ) ; :: thesis: