let G be finite nonnegative-weighted WGraph; :: thesis: for s being Vertex of G
for n being Nat
for G2 being inducedWSubgraph of G, dom (((DIJK:CompSeq s) . n) `1),((DIJK:CompSeq s) . n) `2 holds
( G2 is_mincost_DTree_rooted_at s & ( for v being Vertex of G st v in dom (((DIJK:CompSeq s) . n) `1) holds
G .min_DPath_cost (s,v) = (((DIJK:CompSeq s) . n) `1) . v ) )
let src be Vertex of G; :: thesis: 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 ) )
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 ) );
A1: (DIJK:CompSeq src) . 0 = DIJK:Init src by Def11;
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:13;

now

let n be Nat; :: thesis: ( S₁[n] implies for Dn1W being inducedWSubgraph of G, dom (((DIJK:CompSeq src) . (n + 1)) `1),((DIJK:CompSeq src) . (n + 1)) `2 holds
( 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 ) ) )
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)));
set DnW = the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ;
A4: (DIJK:CompSeq src) . (n + 1) = DIJK:Step ((DIJK:CompSeq src) . n) by Def11;
assume A5: S₁[n] ; :: thesis: for Dn1W being inducedWSubgraph of G, dom (((DIJK:CompSeq src) . (n + 1)) `1),((DIJK:CompSeq src) . (n + 1)) `2 holds
( 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 ) )
then A6: the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 is_mincost_DTree_rooted_at src ;
then A7: the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 is Tree-like by Def1;
let Dn1W be inducedWSubgraph of G, dom (((DIJK:CompSeq src) . (n + 1)) `1),((DIJK:CompSeq src) . (n + 1)) `2 ; :: thesis: ( 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 ) )
A8: ( src in dom (((DIJK:CompSeq src) . 0) `1) & dom (((DIJK:CompSeq src) . 0) `1) c= dom (((DIJK:CompSeq src) . n) `1) ) by A3, Th18, TARSKI:def 1;
A9: ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1)) by Th22;
then A10: card (((DIJK:CompSeq src) . n) `2) = the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 .size() by A8, GLIB_000:def 37;
A11: ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1)) by Th22;
then A12: the_Vertices_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 = dom (((DIJK:CompSeq src) . n) `1) by A8, GLIB_000:def 37;
A13: the_Edges_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 = ((DIJK:CompSeq src) . n) `2 by A8, A11, GLIB_000:def 37;
A14: card (dom (((DIJK:CompSeq src) . n) `1)) = the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 .order() by A8, A9, GLIB_000:def 37;

now

per cases ( DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} or DIJK:NextBestEdges ((DIJK:CompSeq src) . n) <> {} ) ;

suppose DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} ; :: thesis: ( 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 ) )

then (DIJK:CompSeq src) . (n + 1) = (DIJK:CompSeq src) . n by A4, Def8;
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 A5; :: thesis: verum

end;

suppose A15: DIJK:NextBestEdges ((DIJK:CompSeq src) . n) <> {} ; :: thesis: ( 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 ) )

set mc = G .min_DPath_cost (src,((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))));
A16: the_Weight_of Dn1W = (the_Weight_of G) | (the_Edges_of Dn1W) by GLIB_003:def 10;
A17: choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) DSJoins dom (((DIJK:CompSeq src) . n) `1),(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)),G by A15, Def7;
then A18: (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) in (the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)) by GLIB_000:def 16;
then A19: src <> (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A8, XBOOLE_0:def 5;
A20: not (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) in dom (((DIJK:CompSeq src) . n) `1) by A18, XBOOLE_0:def 5;
then A21: card ((dom (((DIJK:CompSeq src) . n) `1)) \/ {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))}) = (card (dom (((DIJK:CompSeq src) . n) `1))) + 1 by CARD_2:41;
A22: (the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) in dom (((DIJK:CompSeq src) . n) `1) by A17, GLIB_000:def 16;
A23: (DIJK:CompSeq src) . (n + 1) = [((((DIJK:CompSeq src) . n) `1) +* (((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))))))),((((DIJK:CompSeq src) . n) `2) \/ {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))})] by A4, A15, Def8;
then ((DIJK:CompSeq src) . (n + 1)) `1 = (((DIJK:CompSeq src) . n) `1) +* (((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 MCART_1:7;
then A24: dom (((DIJK:CompSeq src) . (n + 1)) `1) = (dom (((DIJK:CompSeq src) . n) `1)) \/ {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} by Lm1;
A25: ((DIJK:CompSeq src) . (n + 1)) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1)) by Th22;
then A26: the_Vertices_of Dn1W = (dom (((DIJK:CompSeq src) . n) `1)) \/ {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} by A24, GLIB_000:def 37;
((DIJK:CompSeq src) . (n + 1)) `2 = (((DIJK:CompSeq src) . n) `2) \/ {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))} by A23, MCART_1:7;
then A27: the_Edges_of Dn1W = (((DIJK:CompSeq src) . n) `2) \/ {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))} by A24, A25, GLIB_000:def 37;

A28: now

thus ( the_Vertices_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 c= the_Vertices_of Dn1W & the_Edges_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 c= the_Edges_of Dn1W ) by A12, A13, A26, A27, XBOOLE_1:7; :: thesis: for e being set st e in the_Edges_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 holds
( (the_Source_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ) . e = (the_Source_of Dn1W) . e & (the_Target_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ) . e = (the_Target_of Dn1W) . e )
let e be set ; :: thesis: ( e in the_Edges_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 implies ( (the_Source_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ) . e = (the_Source_of Dn1W) . e & (the_Target_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ) . e = (the_Target_of Dn1W) . e ) )
assume A29: e in the_Edges_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ; :: thesis: ( (the_Source_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ) . e = (the_Source_of Dn1W) . e & (the_Target_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ) . e = (the_Target_of Dn1W) . e )
then A30: (the_Target_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ) . e = (the_Target_of G) . e by GLIB_000:def 32;
( e in the_Edges_of Dn1W & (the_Source_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ) . e = (the_Source_of G) . e ) by A13, A27, A29, GLIB_000:def 32, XBOOLE_0:def 3;
hence ( (the_Source_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ) . e = (the_Source_of Dn1W) . e & (the_Target_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ) . e = (the_Target_of Dn1W) . e ) by A30, GLIB_000:def 32; :: thesis: verum

end;

then reconsider DnW9 = the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 as [Weighted] Subgraph of Dn1W by GLIB_000:def 32;
choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) in {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))} by TARSKI:def 1;
then A31: choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) in the_Edges_of Dn1W by A27, XBOOLE_0:def 3;
choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) in DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A15;
then choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) DJoins (the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))),(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))),G by GLIB_000:def 14;
then A32: choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) DJoins (the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))),(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))),Dn1W by A31, GLIB_000:73;
then A33: choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) Joins (the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))),(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))),Dn1W by GLIB_000:16;
A34: the_Weight_of DnW9 = (the_Weight_of G) | (the_Edges_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ) by GLIB_003:def 10;

A35: now

let y be set ; :: thesis: ( y in dom (the_Weight_of DnW9) implies (the_Weight_of DnW9) . y = (the_Weight_of Dn1W) . y )
assume y in dom (the_Weight_of DnW9) ; :: thesis: (the_Weight_of DnW9) . y = (the_Weight_of Dn1W) . y
then A36: y in the_Edges_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 by PARTFUN1:def 2;
hence (the_Weight_of DnW9) . y = (the_Weight_of G) . y by A34, FUNCT_1:49
.= (the_Weight_of Dn1W) . y by A28, A16, A36, FUNCT_1:49 ;
:: thesis: verum

end;

dom (the_Weight_of Dn1W) = the_Edges_of Dn1W by PARTFUN1:def 2;
then (dom (the_Weight_of Dn1W)) /\ (the_Edges_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ) = the_Edges_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 by A28, XBOOLE_1:28;
then dom (the_Weight_of DnW9) = (dom (the_Weight_of Dn1W)) /\ (the_Edges_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ) by PARTFUN1:def 2;
then the_Weight_of DnW9 = (the_Weight_of Dn1W) | (the_Edges_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 ) by A35, FUNCT_1:46;
then A37: the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 is WSubgraph of Dn1W by GLIB_003:def 10;
A38: the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 is Subgraph of Dn1W by A28, GLIB_000:def 32;

now

let u, v be Vertex of Dn1W; :: thesis: ex W being Walk of Dn1W st W is_Walk_from u,v

A39: now

let u, v be set ; :: thesis: ( u in dom (((DIJK:CompSeq src) . n) `1) & v in dom (((DIJK:CompSeq src) . n) `1) implies ex W being Walk of Dn1W st W is_Walk_from u,v )
assume ( u in dom (((DIJK:CompSeq src) . n) `1) & v in dom (((DIJK:CompSeq src) . n) `1) ) ; :: thesis: ex W being Walk of Dn1W st W is_Walk_from u,v
then reconsider u9 = u, v9 = v as Vertex of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 by A11, GLIB_000:def 37;
consider W1 being Walk of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 such that
A40: W1 is_Walk_from u9,v9 by A7, GLIB_002:def 1;
reconsider W2 = W1 as Walk of Dn1W by A38, GLIB_001:167;
W2 is_Walk_from u,v by A40, GLIB_001:19;
hence ex W being Walk of Dn1W st W is_Walk_from u,v ; :: thesis: verum

end;

now

per cases ( ( u in dom (((DIJK:CompSeq src) . n) `1) & v in dom (((DIJK:CompSeq src) . n) `1) ) or ( u in dom (((DIJK:CompSeq src) . n) `1) & v in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} ) or ( u in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} & v in dom (((DIJK:CompSeq src) . n) `1) ) or ( 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))))} ) ) by A26, XBOOLE_0:def 3;

suppose ( u in dom (((DIJK:CompSeq src) . n) `1) & v in dom (((DIJK:CompSeq src) . n) `1) ) ; :: thesis: ex W being Walk of Dn1W st W is_Walk_from u,v

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

end;

suppose A41: ( u in dom (((DIJK:CompSeq src) . n) `1) & v in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} ) ; :: thesis: ex W being Walk of Dn1W st W is_Walk_from u,v

then A42: v = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by TARSKI:def 1;
consider W being Walk of Dn1W such that
A43: W is_Walk_from u,(the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A22, A39, A41;
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 A33, A43, GLIB_001:66;
hence ex W being Walk of Dn1W st W is_Walk_from u,v by A42; :: thesis: verum

end;

suppose A44: ( u in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} & v in dom (((DIJK:CompSeq src) . n) `1) ) ; :: thesis: ex W being Walk of Dn1W st W is_Walk_from u,v

then consider W being Walk of Dn1W such that
A45: W is_Walk_from v,(the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A22, A39;
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 A33, A45, GLIB_001:66;
then W .addEdge (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) is_Walk_from v,u by A44, TARSKI:def 1;
then (W .addEdge (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) .reverse() is_Walk_from u,v by GLIB_001:23;
hence ex W being Walk of Dn1W st W is_Walk_from u,v ; :: thesis: verum

end;

suppose A46: ( 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: ex W being Walk of Dn1W st W is_Walk_from u,v

take W = Dn1W .walkOf u; :: thesis: W is_Walk_from u,v
( 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 A46, TARSKI:def 1;
hence W is_Walk_from u,v by GLIB_001:13; :: thesis: verum

end;

end;

end;

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

end;

then A47: Dn1W is connected by GLIB_002:def 1;
A48: not choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) in ((DIJK:CompSeq src) . n) `2 by A9, A20, GLIB_000:31;
then Dn1W .size() = ( the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 .size()) + 1 by A10, A27, CARD_2:41;
then Dn1W .order() = (Dn1W .size()) + 1 by A14, A7, A26, A21, GLIB_002:47;
then A49: Dn1W is Tree-like by A47, GLIB_002:47;

now

consider WT being DPath of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 such that
A50: WT is_Walk_from src,(the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) and
A51: 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 A12, A6, A22, Def1;
reconsider WT9 = WT as DPath of Dn1W by A38, GLIB_001:175;
set W2 = WT9 .addEdge (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)));
A52: WT9 is_Walk_from src,(the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A50, GLIB_001:19;
then reconsider W2 = WT9 .addEdge (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) as DWalk of Dn1W by A32, GLIB_001:123;

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 A26, XBOOLE_0:def 3; :: thesis: ( choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) Joins WT9 .last() ,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))),Dn1W & not choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) in WT9 .edges() & ( WT9 is trivial or not WT9 is closed ) & ( for n being odd Element of NAT st 1 < n & n <= len WT9 holds
WT9 . n <> (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) ) )
thus choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) Joins WT9 .last() ,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))),Dn1W by A33, A52, GLIB_001:def 23; :: thesis: ( not choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) in WT9 .edges() & ( WT9 is trivial or not WT9 is closed ) & ( for n being odd Element of NAT st 1 < n & n <= len WT9 holds
WT9 . n <> (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) ) )
( not choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) in the_Edges_of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 & WT .edges() = WT9 .edges() ) by A8, A9, A48, GLIB_000:def 37, GLIB_001:110;
hence not choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) in WT9 .edges() ; :: thesis: ( ( WT9 is trivial or not WT9 is closed ) & ( for n being odd Element of NAT st 1 < n & n <= len WT9 holds
WT9 . n <> (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) ) )

now

assume A53: not WT9 is trivial ; :: thesis: not WT9 is closed

now

assume WT9 is closed ; :: thesis: contradiction
then WT9 is Cycle-like by A53, GLIB_001:def 31;
hence contradiction by A49, GLIB_002:def 2; :: thesis: verum

end;

hence not WT9 is closed ; :: thesis: verum

end;

hence ( WT9 is trivial or not WT9 is closed ) ; :: thesis: for n being odd Element of NAT st 1 < n & n <= len WT9 holds
WT9 . n <> (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))
let n be odd Element of NAT ; :: thesis: ( 1 < n & n <= len WT9 implies WT9 . n <> (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) )
assume that
1 < n and
A54: n <= len WT9 ; :: thesis: WT9 . n <> (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))
WT9 .vertices() = WT .vertices() by GLIB_001:98;
then not (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) in WT9 .vertices() by A12, A18, XBOOLE_0:def 5;
hence WT9 . n <> (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A54, GLIB_001:87; :: thesis: verum

end;

then reconsider W2 = W2 as DPath of Dn1W by GLIB_001:150;
take W2 = W2; :: thesis: ( W2 is_Walk_from src,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) & 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)))) )
thus W2 is_Walk_from src,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A33, A52, GLIB_001:66; :: thesis: 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))))

now

( WT9 .last() = (the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) & (the_Source_of Dn1W) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) = (the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) ) by A32, A52, GLIB_000:def 14, GLIB_001:def 23;
hence choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) in (WT9 .last()) .edgesInOut() by A31, GLIB_000:61; :: thesis: ( (the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) = (the_Weight_of Dn1W) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) & WT9 .cost() = (((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) )
reconsider WTG = WT as DPath of G by GLIB_001:175;
A55: WTG is_Walk_from src,(the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A50, GLIB_001:19;
(the_Weight_of Dn1W) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) = ((the_Weight_of G) | (the_Edges_of Dn1W)) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by GLIB_003:def 10;
hence (the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) = (the_Weight_of Dn1W) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A31, FUNCT_1:49; :: thesis: WT9 .cost() = (((DIJK:CompSeq src) . n) `1) . ((the_Source_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)))) = G .min_DPath_cost (src,((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) by A5, A22;
then consider WX being DPath of G such that
A56: WX is_mincost_DPath_from src,(the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) and
A57: (((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) = WX .cost() by A55, Def3;
WX is_Walk_from src,(the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A56, Def2;
then WT .cost() <= (((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) by A51, A57;
then A58: WT9 .cost() <= (((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) by A37, GLIB_003:27;
(((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) <= WTG .cost() by A55, A56, A57, Def2;
then (((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) <= WT9 .cost() by GLIB_003:27;
hence WT9 .cost() = (((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) by A58, XXREAL_0:1; :: thesis: verum

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:25; :: thesis: verum

end;

then consider W2 being DPath of Dn1W such that
A59: W2 is_Walk_from src,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) and
A60: 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)))) ;
reconsider W2G = W2 as DPath of G by GLIB_001:175;
A61: W2G is_Walk_from src,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A59, GLIB_001:19;
A62: W2G .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 A60, GLIB_003:27;

now

consider WB being DPath of G such that
A63: WB is_mincost_DPath_from src,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) and
A64: G .min_DPath_cost (src,((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) = WB .cost() by A61, Def3;
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 A61, A62, A63, A64, Def2; :: thesis: 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))))
A65: WB is_Walk_from src,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A63, Def2;
then reconsider target9 = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) as Vertex of G by GLIB_001:18;
( WB .first() = src & WB .last() = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) ) by A65, GLIB_001:def 23;
then consider lenWB2h being odd Element of NAT such that
A66: lenWB2h = (len WB) - 2 and
A67: (WB .cut (1,lenWB2h)) .addEdge (WB . (lenWB2h + 1)) = WB by A19, GLIB_001:127, GLIB_001:133;
A68: lenWB2h < (len WB) - 0 by A66, XREAL_1:15;
set sa = WB . lenWB2h;
set ea = WB . (lenWB2h + 1);
set WA = WB .cut (1,lenWB2h);
A69: 1 <= lenWB2h by ABIAN:12;
A70: WB . 1 = WB .first() by GLIB_001:def 6
.= src by A65, GLIB_001:def 23 ;
then WB .cut (1,lenWB2h) is_Walk_from src,WB . lenWB2h by A69, A68, GLIB_001:37, JORDAN12:2;
then reconsider sa = WB . lenWB2h as Vertex of G by GLIB_001:18;
A71: WB . (lenWB2h + 1) DJoins sa,WB . (lenWB2h + 2),G by A68, GLIB_001:122;
then A72: WB . (lenWB2h + 1) DJoins sa,WB .last() ,G by A66, GLIB_001:def 7;
then WB . (lenWB2h + 1) DJoins sa,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))),G by A65, GLIB_001:def 23;
then WB . (lenWB2h + 1) Joins sa,target9,G by GLIB_000:16;
then WB . (lenWB2h + 1) in sa .edgesInOut() by GLIB_000:62;
then A73: WB . (lenWB2h + 1) in ((WB .cut (1,lenWB2h)) .last()) .edgesInOut() by A69, A68, GLIB_001:37, JORDAN12:2;
then A74: 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 A64, A67, GLIB_003:25;
reconsider WA = WB .cut (1,lenWB2h) as DPath of G ;
A75: WA .first() = src by A69, A68, A70, GLIB_001:37, JORDAN12:2;
A76: WA .last() = sa by A69, A68, GLIB_001:37, JORDAN12:2;
then A77: WA is_mincost_DPath_from src,sa by A63, A75, Th12;
A78: WB . (lenWB2h + 1) DJoins sa,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))),G by A65, A72, GLIB_001:def 23;
A79: WA .cost() = G .min_DPath_cost (src,sa) by A63, A75, A76, Th12, Th14;

now

defpred S₂[ Nat] means ( not $1 is even & $1 <= len WA & not WA . $1 in dom (((DIJK:CompSeq src) . n) `1) );
A80: (the_Source_of G) . (WB . (lenWB2h + 1)) = sa by A71, GLIB_000:def 14;
assume A81: 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: contradiction

A82: now

assume A83: not sa in dom (((DIJK:CompSeq src) . n) `1) ; :: thesis: contradiction
sa = WA .last() by A69, A68, GLIB_001:37, JORDAN12:2
.= WA . (len WA) by GLIB_001:def 7 ;
then A84: ex k being Nat st S<sub>2</sub>[k] by A83;
consider k being Nat such that
A85: ( S<sub>2</sub>[k] & ( for m being Nat st S<sub>2</sub>[m] holds
k <= m ) ) from NAT_1:sch 5(A84);
reconsider k = k as odd Element of NAT by A85, ORDINAL1:def 12;
A86: 1 <= k by ABIAN:12;
WA . 1 = WA .first() by GLIB_001:def 6
.= src by A69, A68, A70, GLIB_001:37, JORDAN12:2 ;
then k <> 1 by A8, A85;
then 1 < k by A86, XXREAL_0:1;
then 1 + 1 < k + 1 by XREAL_1:8;
then 2 <= k by NAT_1:13;
then reconsider k2a = k - (2 * 1) as odd Element of NAT by INT_1:5;
set sk = WA . k2a;
set ek = WA . (k2a + 1);
set tk = WA . k;
A87: k2a < (len WA) - 0 by A85, XREAL_1:15;
set WKA = WA .cut (1,k);
set WKB = WA .cut (k,(len WA));
set WK1 = WA .cut (1,k2a);
reconsider WK1 = WA .cut (1,k2a), WKA = WA .cut (1,k), WKB = WA .cut (k,(len WA)) as DPath of G ;
A88: 1 <= k by ABIAN:12;
then A89: WKA .append WKB = WA .cut (1,(len WA)) by A85, GLIB_001:38, JORDAN12:2
.= WA by GLIB_001:39 ;
A90: k2a < k - 0 by XREAL_1:15;
then A91: WA . k2a in dom (((DIJK:CompSeq src) . n) `1) by A85, A87;
then reconsider sk = WA . k2a as Vertex of G ;
A92: 1 <= k2a by ABIAN:12;
then A93: WK1 .last() = sk by A87, GLIB_001:37, JORDAN12:2;
WK1 .first() = WA . 1 by A92, A87, GLIB_001:37, JORDAN12:2;
then WK1 is_mincost_DPath_from WA . 1,sk by A77, A93, Th12;
then WK1 is_mincost_DPath_from WA .first() ,sk by GLIB_001:def 6;
then G .min_DPath_cost (src,sk) = WK1 .cost() by A75, Th14;
then A94: (((DIJK:CompSeq src) . n) `1) . sk = WK1 .cost() by A5, A85, A87, A90;
reconsider tk = WA . k as Vertex of G by A85, GLIB_001:7;
A95: tk in (the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)) by A85, XBOOLE_0:def 5;
tk = WA . (k2a + 2) ;
then A96: WA . (k2a + 1) DJoins sk,tk,G by A87, GLIB_001:122;
then A97: (the_Source_of G) . (WA . (k2a + 1)) = sk by GLIB_000:def 14;
WKB .first() = WA . k by A85, GLIB_001:37
.= WKA .last() by A85, A88, GLIB_001:37, JORDAN12:2 ;
then A98: WA .cost() = (WKA .cost()) + (WKB .cost()) by A89, GLIB_003:24;
0 <= WKB .cost() by GLIB_003:29;
then A99: 0 + (WKA .cost()) <= WA .cost() by A98, XREAL_1:7;
WB . (lenWB2h + 1) in the_Edges_of G by A71, GLIB_000:def 14;
then A100: 0 <= (the_Weight_of G) . (WB . (lenWB2h + 1)) by GLIB_003:31;
( WA . (k2a + 1) in the_Edges_of G & (the_Target_of G) . (WA . (k2a + 1)) = tk ) by A96, GLIB_000:def 14;
then WA . (k2a + 1) DSJoins dom (((DIJK:CompSeq src) . n) `1),(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)),G by A91, A97, A95, GLIB_000:def 16;
then A101: ((((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 A15, A97, A94, Def7;
( WA . (k2a + 1) in the_Edges_of G & (the_Source_of G) . (WA . (k2a + 1)) = sk ) by A96, GLIB_000:def 14;
then A102: WA . (k2a + 1) in sk .edgesInOut() by GLIB_000:61;
k2a + 2 = k ;
then WK1 .addEdge (WA . (k2a + 1)) = WKA by A87, ABIAN:12, GLIB_001:41, JORDAN12:2;
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)))) <= WKA .cost() by A93, A101, A102, GLIB_003:25;
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)))) <= WA .cost() by A99, XXREAL_0:2;
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 A100, XREAL_1:7;
hence contradiction by A64, A67, A73, A81, GLIB_003:25; :: thesis: verum

end;

then A103: WA .cost() = (((DIJK:CompSeq src) . n) `1) . sa by A5, A79;
( WB . (lenWB2h + 1) in the_Edges_of G & (the_Target_of G) . (WB . (lenWB2h + 1)) = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) ) by A78, GLIB_000:def 14;
then WB . (lenWB2h + 1) DSJoins dom (((DIJK:CompSeq src) . n) `1),(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)),G by A18, A82, A80, GLIB_000:def 16;
hence contradiction by A15, A74, A81, A103, A80, Def7; :: thesis: verum

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: verum

end;

then A104: 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: 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() ) )

now

per cases ( x in dom (((DIJK:CompSeq src) . n) `1) or x in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} ) by A26, XBOOLE_0:def 3;

suppose x in dom (((DIJK:CompSeq src) . n) `1) ; :: thesis: ex W29 being DPath of Dn1W st
( W29 is_Walk_from src,x & ( for W1 being DPath of G st W1 is_Walk_from src,x holds
W29 .cost() <= W1 .cost() ) )

then reconsider x9 = x as Vertex of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 by A11, GLIB_000:def 37;
the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 is_mincost_DTree_rooted_at src by A5;
then consider W2 being DPath of the inducedWSubgraph of G, dom (((DIJK:CompSeq src) . n) `1),((DIJK:CompSeq src) . n) `2 such that
A105: W2 is_Walk_from src,x9 and
A106: for W1 being DPath of G st W1 is_Walk_from src,x9 holds
W2 .cost() <= W1 .cost() by Def1;
reconsider W29 = W2 as DPath of Dn1W by A38, GLIB_001:175;
take W29 = W29; :: thesis: ( W29 is_Walk_from src,x & ( for W1 being DPath of G st W1 is_Walk_from src,x holds
W29 .cost() <= W1 .cost() ) )
thus W29 is_Walk_from src,x by A105, GLIB_001:19; :: thesis: for W1 being DPath of G st W1 is_Walk_from src,x holds
W29 .cost() <= W1 .cost()
let W1 be DPath of G; :: thesis: ( W1 is_Walk_from src,x implies W29 .cost() <= W1 .cost() )
assume W1 is_Walk_from src,x ; :: thesis: W29 .cost() <= W1 .cost()
then W2 .cost() <= W1 .cost() by A106;
hence W29 .cost() <= W1 .cost() by A37, GLIB_003:27; :: thesis: verum

end;

suppose A107: x in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} ; :: thesis: 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() ) )

take W2 = W2; :: thesis: ( W2 is_Walk_from src,x & ( for W1 being DPath of G st W1 is_Walk_from src,x holds
W2 .cost() <= W1 .cost() ) )
thus W2 is_Walk_from src,x by A59, A107, TARSKI:def 1; :: thesis: for W1 being DPath of G st W1 is_Walk_from src,x holds
W2 .cost() <= W1 .cost()
let W1 be DPath of G; :: thesis: ( W1 is_Walk_from src,x implies W2 .cost() <= W1 .cost() )
assume A108: W1 is_Walk_from src,x ; :: thesis: W2 .cost() <= W1 .cost()
A109: x = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A107, TARSKI:def 1;
ex WX being DPath of G st
( WX is_mincost_DPath_from src,(the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) & WX .cost() = W2 .cost() ) by A60, A61, A104, Def3;
hence W2 .cost() <= W1 .cost() by A109, A108, Def2; :: thesis: verum

end;

end;

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: verum

end;

hence Dn1W is_mincost_DTree_rooted_at src by A49, Def1; :: thesis: 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
let v be Vertex of G; :: thesis: ( v in dom (((DIJK:CompSeq src) . (n + 1)) `1) implies G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . (n + 1)) `1) . v )
assume A110: v in dom (((DIJK:CompSeq src) . (n + 1)) `1) ; :: thesis: G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . (n + 1)) `1) . v

now

per cases ( v in dom (((DIJK:CompSeq src) . n) `1) or v in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} ) by A24, A110, XBOOLE_0:def 3;

suppose A111: v in dom (((DIJK:CompSeq src) . n) `1) ; :: thesis: G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . (n + 1)) `1) . v

then A112: G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . n) `1) . v by A5;
A113: ((DIJK:CompSeq src) . (n + 1)) `1 = (((DIJK:CompSeq src) . n) `1) +* (((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 A23, MCART_1:7;
A114: dom (((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)))))) = {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} by FUNCOP_1:13;
then not v in dom (((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 A20, A111, TARSKI:def 1;
hence G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . (n + 1)) `1) . v by A24, A110, A112, A113, A114, FUNCT_4:def 1; :: thesis: verum

end;

suppose A115: v in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} ; :: thesis: G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . (n + 1)) `1) . v

( ((DIJK:CompSeq src) . (n + 1)) `1 = (((DIJK:CompSeq src) . n) `1) +* (((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)))))) & dom (((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)))))) = {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} ) by A23, FUNCOP_1:13, MCART_1:7;
then A116: (((DIJK:CompSeq src) . (n + 1)) `1) . v = (((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)))))) . v by A115, FUNCT_4:13;
v = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) by A115, TARSKI:def 1;
hence G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . (n + 1)) `1) . v by A104, A116, FUNCOP_1:72; :: thesis: verum

end;

end;

end;

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

end;

end;

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: verum

end;

then A117: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A118: ((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: ( D0W is_mincost_DTree_rooted_at src & ( for v being Vertex of G st v in dom (((DIJK:CompSeq src) . 0) `1) holds
G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . 0) `1) . v ) )
A119: {} c= G .edgesBetween (dom (((DIJK:CompSeq src) . 0) `1)) by XBOOLE_1:2;
then A120: the_Vertices_of D0W = {src} by A3, A118, GLIB_000:def 37;
then card (the_Vertices_of D0W) = 1 by CARD_1:30;
then A121: D0W is trivial by GLIB_000:def 19;

A122: now

let x be Vertex of D0W; :: thesis: ex W2 being Walk of D0W 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() ) )
set W2 = D0W .walkOf x;
take W2 = D0W .walkOf x; :: thesis: ( W2 is_Walk_from src,x & ( for W1 being DPath of G st W1 is_Walk_from src,x holds
W2 .cost() <= W1 .cost() ) )
x = src by A120, TARSKI:def 1;
hence W2 is_Walk_from src,x by GLIB_001:13; :: thesis: for W1 being DPath of G st W1 is_Walk_from src,x holds
W2 .cost() <= W1 .cost()
let W1 be DPath of G; :: thesis: ( W1 is_Walk_from src,x implies W2 .cost() <= W1 .cost() )
assume W1 is_Walk_from src,x ; :: thesis: W2 .cost() <= W1 .cost()
0 <= W1 .cost() by GLIB_003:29;
hence W2 .cost() <= W1 .cost() by GLIB_003:21; :: thesis: verum

end;

the_Edges_of D0W = {} by A2, A118, A119, GLIB_000:def 37;
then D0W .order() = (D0W .size()) + 1 by A120, CARD_1:27, CARD_1:30;
then D0W is Tree-like by A121, GLIB_002:47;
hence D0W is_mincost_DTree_rooted_at src by A122, Def1; :: thesis: for v being Vertex of G st v in dom (((DIJK:CompSeq src) . 0) `1) holds
G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . 0) `1) . v
let v be Vertex of G; :: thesis: ( v in dom (((DIJK:CompSeq src) . 0) `1) implies G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . 0) `1) . v )
assume A123: v in dom (((DIJK:CompSeq src) . 0) `1) ; :: thesis: G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . 0) `1) . v
then A124: v = src by A3, TARSKI:def 1;

A125: now

set W1 = G .walkOf v;
A126: G .walkOf v is_Walk_from src,v by A124, GLIB_001:13;
then consider W being DPath of G such that
A127: W is_mincost_DPath_from src,v and
A128: G .min_DPath_cost (src,v) = W .cost() by Def3;
(G .walkOf v) .cost() = 0 by GLIB_003:21;
then W .cost() <= 0 by A126, A127, Def2;
hence G .min_DPath_cost (src,v) = 0 by A128, GLIB_003:29; :: thesis: verum

end;

(((DIJK:CompSeq src) . 0) `1) . src = 0 by A2, FUNCOP_1:72;
hence G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . 0) `1) . v by A3, A123, A125, TARSKI:def 1; :: thesis: verum

end;

then A129: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A129, A117);
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: verum