let V, e 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 that
A1: e in the carrier' of G and
A2: P is_shortestpath_of v1,v2,V,W and
A3: v1 <> v3 and
A4: Q = P ^ <*e*> and
A5: e orientedly_joins v2,v3 and
A6: v1 in V and
A7: 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 Eg = the carrier' of G;
reconsider pe = <*e*> as FinSequence of the carrier' of G by A1, FINSEQ_1:74;
A8: P is_orientedpath_of v1,v2,V by A2, GRAPH_5:def 18;
then P is_orientedpath_of v1,v2 by GRAPH_5:def 4;
then P <> {} by GRAPH_5:def 3;
then A9: len P >= 1 by FINSEQ_1:20;
set V9 = V \/ {v2};
set FS = the Source of G;
set FT = the Target of G;
A10: W is_weight>=0of G by GRAPH_5:def 13;

A11: now :: thesis:

let S be oriented Chain of G; :: thesis:
assume A12: S is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis:
then consider s being oriented Simple Chain of G such that
A13: s is_shortestpath_of v1,v3,V \/ {v2},W by A10, GRAPH_5:62;
set Vs = vertices s;
A14: s is_orientedpath_of v1,v3,V \/ {v2} by A13, GRAPH_5:def 18;
then A15: s is_orientedpath_of v1,v3 by GRAPH_5:def 4;
then A16: the Target of G . (s . (len s)) = v3 by GRAPH_5:def 3;
A17: (vertices s) \ {v3} c= V \/ {v2} by A14, GRAPH_5:def 4;
s <> {} by A15, GRAPH_5:def 3;
then A18: len s >= 1 by FINSEQ_1:20;
then consider i being Nat such that
A19: len s = 1 + i by NAT_1:10;
consider s1, s2 being FinSequence such that
A20: len s1 = i and
A21: len s2 = 1 and
A22: s = s1 ^ s2 by A19, FINSEQ_2:22;
reconsider s1 = s1, s2 = s2 as oriented Simple Chain of G by A22, GRAPH_5:14;
reconsider vx = the Source of G . (s2 . 1) as Vertex of G by A21, Lm3;
A23: s2 . 1 = s . (len s) by A19, A20, A21, A22, Lm2;
A24: the Source of G . (s . 1) = v1 by A15, GRAPH_5:def 3;
A25: s1 <> {}

assume s1 = {} ; :: thesis:
then A26: len s = 1 + 0 by A19, A20;
then s . 1 orientedly_joins v1,v3 by A24, A16, GRAPH_4:def 1;
hence contradiction by A6, A7, A26, Th2; :: thesis:

end;

then A27: len s1 >= 1 by FINSEQ_1:20;
len s1 < len s by A19, A20, NAT_1:13;
then A28: the Source of G . (s . (len s)) = the Target of G . (s . (len s1)) by A19, A20, A27, GRAPH_1:def 15
.= the Target of G . (s1 . (len s1)) by A22, A27, Lm1 ;

A29: now :: thesis:

vx <> the Target of G . (s . (len s)) by A21, A22, A23, A27, A28, Th6;
then A30: not vx in {v3} by A16, TARSKI:def 1;
vx in vertices s by A18, A23, Lm4;
then vx in (vertices s) \ {v3} by A30, XBOOLE_0:def 5;
then A31: ( vx in V or vx in {v2} ) by A17, XBOOLE_0:def 3;
assume A32: vx <> v2 ; :: thesis:
( s2 . 1 orientedly_joins vx,v3 & s2 . 1 in the carrier' of G ) by A21, A23, A16, Th2, GRAPH_4:def 1;
hence contradiction by A7, A32, A31, TARSKI:def 1; :: thesis:

end;

len s2 = 1 by A21;
then not the Target of G . (s . (len s)) in vertices s1 by A3, A22, A24, A16, A27, GRAPH_5:18;
then A33: (vertices s1) \ {v3} = vertices s1 by A16, ZFMISC_1:57;
vertices s1 c= vertices (s1 ^ s2) by GRAPH_5:26;
then vertices s1 c= (vertices s) \ {v3} by A22, A33, XBOOLE_1:33;
then vertices s1 c= V \/ {v2} by A17;
then (vertices s1) \ {v2} c= (V \/ {v2}) \ {v2} by XBOOLE_1:33;
then (vertices s1) \ {v2} c= V \ {v2} by XBOOLE_1:40;
then A34: (vertices s1) \ {v2} c= V by XBOOLE_1:1;
s2 /. 1 in the carrier' of G by A1;
then A35: s2 . 1 in the carrier' of G by A21, FINSEQ_4:15;
( the Source of G . e = v2 & the Target of G . e = v3 ) by A5, GRAPH_4:def 1;
then e = s2 . 1 by A1, A23, A16, A29, A35, GRAPH_1:def 7;
then s2 = <*e*> by A21, FINSEQ_1:40;
then A36: cost (Q,W) = (cost (P,W)) + (cost (s2,W)) by A4, A10, GRAPH_5:46, GRAPH_5:54;
the Source of G . (s1 . 1) = v1 by A22, A24, A27, Lm1;
then s1 is_orientedpath_of v1,v2 by A23, A25, A28, A29, GRAPH_5:def 3;
then s1 is_orientedpath_of v1,v2,V by A34, GRAPH_5:def 4;
then A37: cost (P,W) <= cost (s1,W) by A2, GRAPH_5:def 18;
A38: cost (s,W) <= cost (S,W) by A12, A13, GRAPH_5:def 18;
cost (s,W) = (cost (s1,W)) + (cost (s2,W)) by A10, A22, GRAPH_5:46, GRAPH_5:54;
then cost (Q,W) <= cost (s,W) by A37, A36, XREAL_1:7;
hence cost (Q,W) <= cost (S,W) by A38, XXREAL_0:2; :: thesis:

end;

( len pe = 1 & pe . 1 = e ) by FINSEQ_1:40;
then Q is_orientedpath_of v1,v3,V \/ {v2} by A4, A5, A8, A9, GRAPH_5:34;
hence Q is_shortestpath_of v1,v3,V \/ {v2},W by A11, GRAPH_5:def 18; :: thesis: