let e be set ; :: thesis: for G being oriented finite Graph

for P being oriented Chain of G

for W being Function of the carrier' of G,Real>=0

for v1, v2 being Vertex of G st e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 holds

P is_shortestpath_of v1,v2,{v1},W

let G be oriented finite Graph; :: thesis: for P being oriented Chain of G

for W being Function of the carrier' of G,Real>=0

for v1, v2 being Vertex of G st e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 holds

P is_shortestpath_of v1,v2,{v1},W

let P be oriented Chain of G; :: thesis: for W being Function of the carrier' of G,Real>=0

for v1, v2 being Vertex of G st e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 holds

P is_shortestpath_of v1,v2,{v1},W

let W be Function of the carrier' of G,Real>=0; :: thesis: for v1, v2 being Vertex of G st e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 holds

P is_shortestpath_of v1,v2,{v1},W

let v1, v2 be Vertex of G; :: thesis: ( e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 implies P is_shortestpath_of v1,v2,{v1},W )

assume that

A1: e in the carrier' of G and

A2: P = <*e*> and

A3: e orientedly_joins v1,v2 ; :: thesis: P is_shortestpath_of v1,v2,{v1},W

A4: len P = 1 by A2, FINSEQ_1:40;

then A5: vertices P = vertices (P /. 1) by GRAPH_5:25;

set FS = the Source of G;

set FT = the Target of G;

set Eg = the carrier' of G;

A6: ( the Source of G . e = v1 & the Target of G . e = v2 ) by A3, GRAPH_4:def 1;

then P /. 1 = e by A4, FINSEQ_4:15;

then vertices P = {v1,v2} by A6, A5, GRAPH_5:def 1;

then A27: (vertices P) \ {v2} = ({v1} \/ {v2}) \ {v2} by ENUMSET1:1

.= {v1} \ {v2} by XBOOLE_1:40 ;

P is_orientedpath_of v1,v2 by A2, A6, A4, A26, GRAPH_5:def 3;

then P is_orientedpath_of v1,v2,{v1} by A27, GRAPH_5:def 4;

hence P is_shortestpath_of v1,v2,{v1},W by A7, GRAPH_5:def 18; :: thesis: verum

for P being oriented Chain of G

for W being Function of the carrier' of G,Real>=0

for v1, v2 being Vertex of G st e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 holds

P is_shortestpath_of v1,v2,{v1},W

let G be oriented finite Graph; :: thesis: for P being oriented Chain of G

for W being Function of the carrier' of G,Real>=0

for v1, v2 being Vertex of G st e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 holds

P is_shortestpath_of v1,v2,{v1},W

let P be oriented Chain of G; :: thesis: for W being Function of the carrier' of G,Real>=0

for v1, v2 being Vertex of G st e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 holds

P is_shortestpath_of v1,v2,{v1},W

let W be Function of the carrier' of G,Real>=0; :: thesis: for v1, v2 being Vertex of G st e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 holds

P is_shortestpath_of v1,v2,{v1},W

let v1, v2 be Vertex of G; :: thesis: ( e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 implies P is_shortestpath_of v1,v2,{v1},W )

assume that

A1: e in the carrier' of G and

A2: P = <*e*> and

A3: e orientedly_joins v1,v2 ; :: thesis: P is_shortestpath_of v1,v2,{v1},W

A4: len P = 1 by A2, FINSEQ_1:40;

then A5: vertices P = vertices (P /. 1) by GRAPH_5:25;

set FS = the Source of G;

set FT = the Target of G;

set Eg = the carrier' of G;

A6: ( the Source of G . e = v1 & the Target of G . e = v2 ) by A3, GRAPH_4:def 1;

A7: now :: thesis: for S being oriented Chain of G st S is_orientedpath_of v1,v2,{v1} holds

cost (P,W) <= cost (S,W)

A26:
P . 1 = e
by A2, FINSEQ_1:40;cost (P,W) <= cost (S,W)

let S be oriented Chain of G; :: thesis: ( S is_orientedpath_of v1,v2,{v1} implies cost (P,W) <= cost (S,W) )

assume A8: S is_orientedpath_of v1,v2,{v1} ; :: thesis: cost (P,W) <= cost (S,W)

W is_weight>=0of G by GRAPH_5:def 13;

then consider s being oriented Simple Chain of G such that

A9: s is_shortestpath_of v1,v2,{v1},W by A8, GRAPH_5:62;

set Vs = vertices s;

A10: s is_orientedpath_of v1,v2,{v1} by A9, GRAPH_5:def 18;

then A11: s is_orientedpath_of v1,v2 by GRAPH_5:def 4;

then s <> {} by GRAPH_5:def 3;

then len s >= 1 by FINSEQ_1:20;

then consider i being Nat such that

A12: len s = 1 + i by NAT_1:10;

A13: the Target of G . (s . (len s)) = v2 by A11, GRAPH_5:def 3;

A14: the Source of G . (s . 1) = v1 by A11, GRAPH_5:def 3;

consider s1, s2 being FinSequence such that

A15: len s1 = i and

A16: len s2 = 1 and

A17: s = s1 ^ s2 by A12, FINSEQ_2:22;

reconsider s1 = s1, s2 = s2 as oriented Simple Chain of G by A17, GRAPH_5:14;

(vertices s) \ {v2} c= {v1} by A10, GRAPH_5:def 4;

then vertices s c= {v2} \/ {v1} by XBOOLE_1:44;

then A18: vertices s c= {v1,v2} by ENUMSET1:1;

s /. 1 in the carrier' of G by A1;

then s . 1 in the carrier' of G by A25, FINSEQ_4:15;

then e = s . 1 by A1, A6, A14, A13, A25, GRAPH_1:def 7;

then s = P by A2, A25, FINSEQ_1:40;

hence cost (P,W) <= cost (S,W) by A8, A9, GRAPH_5:def 18; :: thesis: verum

end;assume A8: S is_orientedpath_of v1,v2,{v1} ; :: thesis: cost (P,W) <= cost (S,W)

W is_weight>=0of G by GRAPH_5:def 13;

then consider s being oriented Simple Chain of G such that

A9: s is_shortestpath_of v1,v2,{v1},W by A8, GRAPH_5:62;

set Vs = vertices s;

A10: s is_orientedpath_of v1,v2,{v1} by A9, GRAPH_5:def 18;

then A11: s is_orientedpath_of v1,v2 by GRAPH_5:def 4;

then s <> {} by GRAPH_5:def 3;

then len s >= 1 by FINSEQ_1:20;

then consider i being Nat such that

A12: len s = 1 + i by NAT_1:10;

A13: the Target of G . (s . (len s)) = v2 by A11, GRAPH_5:def 3;

A14: the Source of G . (s . 1) = v1 by A11, GRAPH_5:def 3;

consider s1, s2 being FinSequence such that

A15: len s1 = i and

A16: len s2 = 1 and

A17: s = s1 ^ s2 by A12, FINSEQ_2:22;

reconsider s1 = s1, s2 = s2 as oriented Simple Chain of G by A17, GRAPH_5:14;

(vertices s) \ {v2} c= {v1} by A10, GRAPH_5:def 4;

then vertices s c= {v2} \/ {v1} by XBOOLE_1:44;

then A18: vertices s c= {v1,v2} by ENUMSET1:1;

now :: thesis: not s1 <> {}

then A25:
len s = 0 + 1
by A12, A15;reconsider vx = the Source of G . (s2 . 1) as Vertex of G by A16, Lm3;

A19: len s1 < len s by A12, A15, NAT_1:13;

A20: vx in vertices s2 by A16, Lm4;

vertices s2 c= vertices (s1 ^ s2) by GRAPH_5:26;

then A21: vertices s2 c= {v1,v2} by A18, A17;

assume s1 <> {} ; :: thesis: contradiction

then A22: len s1 >= 1 by FINSEQ_1:20;

then A23: the Source of G . (s . 1) <> the Source of G . (s2 . 1) by A16, A17, Th6;

len s2 = 1 by A16;

then A24: the Target of G . (s . (len s)) <> the Target of G . (s1 . (len s1)) by A17, A22, Th6;

the Source of G . (s2 . 1) = the Source of G . (s . ((len s1) + 1)) by A16, A17, Lm2

.= the Target of G . (s . (len s1)) by A22, A19, GRAPH_1:def 15

.= the Target of G . (s1 . (len s1)) by A17, A22, Lm1 ;

hence contradiction by A14, A13, A24, A23, A21, A20, TARSKI:def 2; :: thesis: verum

end;A19: len s1 < len s by A12, A15, NAT_1:13;

A20: vx in vertices s2 by A16, Lm4;

vertices s2 c= vertices (s1 ^ s2) by GRAPH_5:26;

then A21: vertices s2 c= {v1,v2} by A18, A17;

assume s1 <> {} ; :: thesis: contradiction

then A22: len s1 >= 1 by FINSEQ_1:20;

then A23: the Source of G . (s . 1) <> the Source of G . (s2 . 1) by A16, A17, Th6;

len s2 = 1 by A16;

then A24: the Target of G . (s . (len s)) <> the Target of G . (s1 . (len s1)) by A17, A22, Th6;

the Source of G . (s2 . 1) = the Source of G . (s . ((len s1) + 1)) by A16, A17, Lm2

.= the Target of G . (s . (len s1)) by A22, A19, GRAPH_1:def 15

.= the Target of G . (s1 . (len s1)) by A17, A22, Lm1 ;

hence contradiction by A14, A13, A24, A23, A21, A20, TARSKI:def 2; :: thesis: verum

s /. 1 in the carrier' of G by A1;

then s . 1 in the carrier' of G by A25, FINSEQ_4:15;

then e = s . 1 by A1, A6, A14, A13, A25, GRAPH_1:def 7;

then s = P by A2, A25, FINSEQ_1:40;

hence cost (P,W) <= cost (S,W) by A8, A9, GRAPH_5:def 18; :: thesis: verum

then P /. 1 = e by A4, FINSEQ_4:15;

then vertices P = {v1,v2} by A6, A5, GRAPH_5:def 1;

then A27: (vertices P) \ {v2} = ({v1} \/ {v2}) \ {v2} by ENUMSET1:1

.= {v1} \ {v2} by XBOOLE_1:40 ;

P is_orientedpath_of v1,v2 by A2, A6, A4, A26, GRAPH_5:def 3;

then P is_orientedpath_of v1,v2,{v1} by A27, GRAPH_5:def 4;

hence P is_shortestpath_of v1,v2,{v1},W by A7, GRAPH_5:def 18; :: thesis: verum