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 ;
then A3: dom (((DIJK:CompSeq src) . 0) `1) = {src} ;

now :: thesis: for n being Nat st S₁[n] holds
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 ) )

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 = the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n);
set source = (the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n);
set target = (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n);
set DnE = (((DIJK:CompSeq src) . n) `2) \/ { the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)};
set pc = (((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n));
set ec = (the_Weight_of G) . the Element of 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 ;
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 :: 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 ) )

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) . the Element of 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: the Element of 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) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) in (the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)) ;
then A19: src <> (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A8, XBOOLE_0:def 5;
A20: not (the_Target_of G) . the Element of 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) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))}) = (card (dom (((DIJK:CompSeq src) . n) `1))) + 1 by CARD_2:41;
A22: (the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) in dom (((DIJK:CompSeq src) . n) `1) by A17;
A23: (DIJK:CompSeq src) . (n + 1) = [((((DIJK:CompSeq src) . n) `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) .--> (((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))),((((DIJK:CompSeq src) . n) `2) \/ { the Element of 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) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) .--> (((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) ;
then A24: dom (((DIJK:CompSeq src) . (n + 1)) `1) = (dom (((DIJK:CompSeq src) . n) `1)) \/ {((the_Target_of G) . the Element of 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) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))} by A24, GLIB_000:def 37;
((DIJK:CompSeq src) . (n + 1)) `2 = (((DIJK:CompSeq src) . n) `2) \/ { the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)} by A23;
then A27: the_Edges_of Dn1W = (((DIJK:CompSeq src) . n) `2) \/ { the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)} by A24, A25, GLIB_000:def 37;

A28: now :: thesis: ( 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 & ( 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 ) ) )

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;
the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) in { the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)} by TARSKI:def 1;
then A31: the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) in the_Edges_of Dn1W by A27, XBOOLE_0:def 3;
the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) in DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A15;
then the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) DJoins (the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n),(the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n),G ;
then A32: the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) DJoins (the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n),(the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n),Dn1W by A31, GLIB_000:73;
then A33: the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) Joins (the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n),(the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n),Dn1W ;
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 :: thesis: for y being object st y in dom (the_Weight_of DnW9) holds
(the_Weight_of DnW9) . y = (the_Weight_of Dn1W) . y

let y be object ; :: 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 ;
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 :: thesis: for u, v being Vertex of Dn1W ex W being Walk of Dn1W st W is_Walk_from u,v

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

A39: now :: thesis: for u, v being set st u in dom (((DIJK:CompSeq src) . n) `1) & v in dom (((DIJK:CompSeq src) . n) `1) holds
ex W being Walk of Dn1W st W is_Walk_from u,v

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

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) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))} ) or ( u in {((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))} & v in dom (((DIJK:CompSeq src) . n) `1) ) or ( u in {((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))} & v in {((the_Target_of G) . the Element of 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) . the Element of 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) . the Element of 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) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A22, A39, A41;
W .addEdge the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) is_Walk_from u,(the_Target_of G) . the Element of 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) . the Element of 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) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A22, A39;
W .addEdge the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) is_Walk_from v,(the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A33, A45, GLIB_001:66;
then W .addEdge the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) is_Walk_from v,u by A44, TARSKI:def 1;
then (W .addEdge the Element of 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) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))} & v in {((the_Target_of G) . the Element of 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) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) & v = (the_Target_of G) . the Element of 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 the Element of 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 :: thesis: ex W2 being DPath of Dn1W st
( W2 is_Walk_from src,(the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) & W2 .cost() = ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) )

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) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) and
A51: for W1 being DPath of G st W1 is_Walk_from src,(the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) holds
WT .cost() <= W1 .cost() by A12, A6, A22;
reconsider WT9 = WT as DPath of Dn1W by A38, GLIB_001:175;
set W2 = WT9 .addEdge the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n);
A52: WT9 is_Walk_from src,(the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A50, GLIB_001:19;
then reconsider W2 = WT9 .addEdge the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) as DWalk of Dn1W by A32, GLIB_001:123;

now :: thesis: ( (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) is Vertex of Dn1W & the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) Joins WT9 .last() ,(the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n),Dn1W & not the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) in WT9 .edges() & ( not WT9 is trivial or WT9 is open ) & ( for n being odd Element of NAT st 1 < n & n <= len WT9 holds
WT9 . n <> (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) ) )

(the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) in {((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))} by TARSKI:def 1;
hence (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) is Vertex of Dn1W by A26, XBOOLE_0:def 3; :: thesis: ( the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) Joins WT9 .last() ,(the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n),Dn1W & not the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) in WT9 .edges() & ( not WT9 is trivial or WT9 is open ) & ( for n being odd Element of NAT st 1 < n & n <= len WT9 holds
WT9 . n <> (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) ) )
thus the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) Joins WT9 .last() ,(the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n),Dn1W by A33, A52, GLIB_001:def 23; :: thesis: ( not the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) in WT9 .edges() & ( not WT9 is trivial or WT9 is open ) & ( for n being odd Element of NAT st 1 < n & n <= len WT9 holds
WT9 . n <> (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) ) )
( not the Element of 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 the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) in WT9 .edges() ; :: thesis: ( ( not WT9 is trivial or WT9 is open ) & ( for n being odd Element of NAT st 1 < n & n <= len WT9 holds
WT9 . n <> (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) ) )
thus ( not WT9 is trivial or WT9 is open ) by GLIB_001:def 31, A49, GLIB_002:def 2; :: thesis: for n being odd Element of NAT st 1 < n & n <= len WT9 holds
WT9 . n <> (the_Target_of G) . the Element of 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) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) )
assume that
1 < n and
A53: n <= len WT9 ; :: thesis: WT9 . n <> (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)
WT9 .vertices() = WT .vertices() by GLIB_001:98;
then not (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) in WT9 .vertices() by A12, A18, XBOOLE_0:def 5;
hence WT9 . n <> (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A53, 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) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) & W2 .cost() = ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) )
thus W2 is_Walk_from src,(the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A33, A52, GLIB_001:66; :: thesis: W2 .cost() = ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))

now :: thesis: ( the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) in (WT9 .last()) .edgesInOut() & (the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = (the_Weight_of Dn1W) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) & WT9 .cost() = (((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) )

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

end;

hence W2 .cost() = ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) by GLIB_003:25; :: thesis: verum

end;

then consider W2 being DPath of Dn1W such that
A58: W2 is_Walk_from src,(the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) and
A59: W2 .cost() = ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) ;
reconsider W2G = W2 as DPath of G by GLIB_001:175;
A60: W2G is_Walk_from src,(the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A58, GLIB_001:19;
A61: W2G .cost() = ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) by A59, GLIB_003:27;

now :: thesis: ( G .min_DPath_cost (src,((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) <= ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) & G .min_DPath_cost (src,((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) >= ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) )

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

now :: thesis: not G .min_DPath_cost (src,((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) < ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))

defpred S₂[ Nat] means ( $1 is odd & $1 <= len WA & not WA . $1 in dom (((DIJK:CompSeq src) . n) `1) );
A79: (the_Source_of G) . (WB . (lenWB2h + 1)) = sa by A70;
assume A80: G .min_DPath_cost (src,((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) < ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) ; :: thesis: contradiction

A81: now :: thesis: sa in dom (((DIJK:CompSeq src) . n) `1)

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

end;

then A102: WA .cost() = (((DIJK:CompSeq src) . n) `1) . sa by A5, A78;
( WB . (lenWB2h + 1) in the_Edges_of G & (the_Target_of G) . (WB . (lenWB2h + 1)) = (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) ) by A77;
then WB . (lenWB2h + 1) DSJoins dom (((DIJK:CompSeq src) . n) `1),(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)),G by A18, A81, A79;
hence contradiction by A15, A73, A80, A102, A79, Def7; :: thesis: verum

end;

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

end;

then A103: G .min_DPath_cost (src,((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) = ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) by XXREAL_0:1;

now :: thesis: for x being Vertex of Dn1W 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() ) )

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

per cases ( x in dom (((DIJK:CompSeq src) . n) `1) or x in {((the_Target_of G) . the Element of 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
A104: W2 is_Walk_from src,x9 and
A105: for W1 being DPath of G st W1 is_Walk_from src,x9 holds
W2 .cost() <= W1 .cost() ;
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 A104, 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 A105;
hence W29 .cost() <= W1 .cost() by A37, GLIB_003:27; :: thesis: verum

end;

suppose A106: x in {((the_Target_of G) . the Element of 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 A58, A106, 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 A107: W1 is_Walk_from src,x ; :: thesis: W2 .cost() <= W1 .cost()
A108: x = (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A106, TARSKI:def 1;
ex WX being DPath of G st
( WX is_mincost_DPath_from src,(the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) & WX .cost() = W2 .cost() ) by A59, A60, A103, Def3;
hence W2 .cost() <= W1 .cost() by A108, A107; :: 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; :: 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 A109: v in dom (((DIJK:CompSeq src) . (n + 1)) `1) ; :: thesis: G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . (n + 1)) `1) . v

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

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

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

then A111: G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . n) `1) . v by A5;
A112: ((DIJK:CompSeq src) . (n + 1)) `1 = (((DIJK:CompSeq src) . n) `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) .--> (((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) by A23;
not v in dom (((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) .--> (((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) by A20, A110, TARSKI:def 1;
hence G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . (n + 1)) `1) . v by A24, A109, A111, A112, FUNCT_4:def 1; :: thesis: verum

end;

suppose A114: v in {((the_Target_of G) . the Element of 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) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) .--> (((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) & dom (((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) .--> (((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) = {((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))} ) by A23;
then A115: (((DIJK:CompSeq src) . (n + 1)) `1) . v = (((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) .--> (((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) . v by A114, FUNCT_4:13;
v = (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A114, TARSKI:def 1;
hence G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . (n + 1)) `1) . v by A103, A115, 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 A116: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A117: ((DIJK:CompSeq src) . 0) `2 = {} by A1;

now :: thesis: for D0W being inducedWSubgraph of G, dom (((DIJK:CompSeq src) . 0) `1),((DIJK:CompSeq src) . 0) `2 holds
( 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 ) )

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 ) )
A118: {} c= G .edgesBetween (dom (((DIJK:CompSeq src) . 0) `1)) ;
then A119: the_Vertices_of D0W = {src} by A3, A117, GLIB_000:def 37;
then card (the_Vertices_of D0W) = 1 by CARD_1:30;
then A120: D0W is _trivial ;

A121: now :: thesis: for x being Vertex of D0W 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() ) )

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 A119, 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, A117, A118, GLIB_000:def 37;
then D0W .order() = (D0W .size()) + 1 by A119, CARD_1:30;
then D0W is Tree-like by A120, GLIB_002:47;
hence D0W is_mincost_DTree_rooted_at src by A121; :: 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 A122: v in dom (((DIJK:CompSeq src) . 0) `1) ; :: thesis: G .min_DPath_cost (src,v) = (((DIJK:CompSeq src) . 0) `1) . v
then A123: v = src by A3, TARSKI:def 1;

A124: now :: thesis: G .min_DPath_cost (src,v) = 0

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

end;

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

end;

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