let e, V be set ; :: thesis:
let G be oriented finite Graph; :: thesis:
let P, Q be oriented Chain of G; :: thesis:
let W be Function of the carrier' of G,Real>=0 ; :: thesis:
let v1, v2, v3 be Vertex of G; :: thesis:
assume A1: ( e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds
for ee being set holds
( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) ) ; :: thesis:
set V' = V \/ {v2};
set FS = the Source of G;
set FT = the Target of G;
A2: W is_weight>=0of G by GRAPH_5:def 13;
then A3: W is_weight_of G by GRAPH_5:50;
set Eg = the carrier' of G;

A4: now

let S be oriented Chain of G; :: thesis:
assume A5: S is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis:
then consider s being oriented Simple Chain of G such that
A6: s is_shortestpath_of v1,v3,V \/ {v2},W by A2, GRAPH_5:66;
A7: s is_orientedpath_of v1,v3,V \/ {v2} by A6, GRAPH_5:def 18;
then A8: s is_orientedpath_of v1,v3 by GRAPH_5:def 4;
then s <> {} by GRAPH_5:def 3;
then A9: len s >= 1 by FINSEQ_1:28;
then consider i being Nat such that
A10: len s = 1 + i by NAT_1:10;
consider s1, s2 being FinSequence such that
A11: ( len s1 = i & len s2 = 1 & s = s1 ^ s2 ) by A10, FINSEQ_2:25;
reconsider s1 = s1, s2 = s2 as oriented Simple Chain of G by A11, GRAPH_5:17;
A12: s2 . 1 = s . (len s) by A10, A11, Lm2;
A13: ( the Source of G . (s . 1) = v1 & the Target of G . (s . (len s)) = v3 ) by A8, GRAPH_5:def 3;
reconsider vx = the Source of G . (s2 . 1) as Vertex of G by A11, Lm3;
A14: s1 <> {}

proof

assume s1 = {} ; :: thesis:
then A15: len s = 1 + 0 by A10, A11;
then s . 1 orientedly_joins v1,v3 by A13, GRAPH_4:def 1;
hence contradiction by A1, A15, Th2; :: thesis:

end;

then A16: len s1 >= 1 by FINSEQ_1:28;
len s1 < len s by A10, A11, NAT_1:13;
then A17: the Source of G . (s . (len s)) = the Target of G . (s . (len s1)) by A10, A11, A16, GRAPH_1:def 13
.= the Target of G . (s1 . (len s1)) by A11, A16, Lm1 ;
set Vs = vertices s;
A18: (vertices s) \ {v3} c= V \/ {v2} by A7, GRAPH_5:def 4;

A19: now

assume A20: vx <> v2 ; :: thesis:
A21: vx in vertices s by A9, A12, Lm4;
vx <> the Target of G . (s . (len s)) by A11, A12, A16, A17, Th6;
then not vx in {v3} by A13, TARSKI:def 1;
then vx in (vertices s) \ {v3} by A21, XBOOLE_0:def 5;
then A22: ( vx in V or vx in {v2} ) by A18, XBOOLE_0:def 3;
A23: s2 . 1 orientedly_joins vx,v3 by A12, A13, GRAPH_4:def 1;
s2 . 1 in the carrier' of G by A11, Th2;
hence contradiction by A1, A20, A22, A23, TARSKI:def 1; :: thesis:

end;

the Source of G . (s1 . 1) = v1 by A11, A13, A16, Lm1;
then A24: s1 is_orientedpath_of v1,v2 by A12, A14, A17, A19, GRAPH_5:def 3;
len s2 = 1 by A11;
then not the Target of G . (s . (len s)) in vertices s1 by A1, A11, A13, A16, GRAPH_5:21;
then A25: (vertices s1) \ {v3} = vertices s1 by A13, ZFMISC_1:65;
vertices s1 c= vertices (s1 ^ s2) by GRAPH_5:30;
then vertices s1 c= (vertices s) \ {v3} by A11, A25, XBOOLE_1:33;
then vertices s1 c= V \/ {v2} by A18, XBOOLE_1:1;
then (vertices s1) \ {v2} c= (V \/ {v2}) \ {v2} by XBOOLE_1:33;
then (vertices s1) \ {v2} c= V \ {v2} by XBOOLE_1:40;
then (vertices s1) \ {v2} c= V by XBOOLE_1:1;
then s1 is_orientedpath_of v1,v2,V by A24, GRAPH_5:def 4;
then A26: cost P,W <= cost s1,W by A1, GRAPH_5:def 18;
s2 /. 1 in the carrier' of G by A1;
then A27: s2 . 1 in the carrier' of G by A11, FINSEQ_4:24;
( the Source of G . e = v2 & the Target of G . e = v3 ) by A1, GRAPH_4:def 1;
then e = s2 . 1 by A1, A12, A13, A19, A27, GRAPH_1:def 5;
then A28: s2 = <*e*> by A11, FINSEQ_1:57;
A29: cost s,W = (cost s1,W) + (cost s2,W) by A2, A11, GRAPH_5:50, GRAPH_5:58;
cost Q,W = (cost P,W) + (cost s2,W) by A1, A3, A28, GRAPH_5:58;
then A30: cost Q,W <= cost s,W by A26, A29, XREAL_1:9;
cost s,W <= cost S,W by A5, A6, GRAPH_5:def 18;
hence cost Q,W <= cost S,W by A30, XXREAL_0:2; :: thesis:

end;

A31: P is_orientedpath_of v1,v2,V by A1, GRAPH_5:def 18;
then P is_orientedpath_of v1,v2 by GRAPH_5:def 4;
then P <> {} by GRAPH_5:def 3;
then A32: len P >= 1 by FINSEQ_1:28;
reconsider pe = <*e*> as FinSequence of the carrier' of G by A1, FINSEQ_1:95;
( len pe = 1 & pe . 1 = e ) by FINSEQ_1:57;
then Q is_orientedpath_of v1,v3,V \/ {v2} by A1, A31, A32, GRAPH_5:38;
hence Q is_shortestpath_of v1,v3,V \/ {v2},W by A4, GRAPH_5:def 18; :: thesis: