let e, V be set ; :: thesis:
let W be Function; :: thesis:
let G be oriented finite Graph; :: thesis:
let P, Q, R be oriented Chain of G; :: thesis:
let v1, v2, v3 be Element of G; :: thesis:
assume that
A1: e in the carrier' of G and
A2: W is_weight>=0of G and
A3: len P >= 1 and
A4: P is_shortestpath_of v1,v2,V,W and
A5: v1 <> v2 and
A6: v1 <> v3 and
A7: R = P ^ <*e*> and
A8: Q is_shortestpath_of v1,v3,V,W and
A9: e orientedly_joins v2,v3 and
A10: P islongestInShortestpath V,v1,W ; :: thesis:
A11: P is_orientedpath_of v1,v2,V by A4, Def18;
then A12: v1 in V by A5, Th35;
set Eg = the carrier' of G;
reconsider pe = <*e*> as FinSequence of the carrier' of G by A1, FINSEQ_1:95;
set V9 = V \/ {v2};
Q is_orientedpath_of v1,v3,V by A8, Def18;
then A13: Q is_orientedpath_of v1,v3,V \/ {v2} by Th36, XBOOLE_1:7;
A14: ( len pe = 1 & pe . 1 = e ) by FINSEQ_1:57;
then consider s being oriented Simple Chain of G such that
A15: s is_shortestpath_of v1,v3,V \/ {v2},W by A2, A3, A7, A9, A11, Th38, Th66;
A16: R is_orientedpath_of v1,v3,V \/ {v2} by A3, A7, A9, A11, A14, Th38;

A17: now

assume A18: cost Q,W <= cost s,W ; :: thesis:

hereby :: thesis:

assume cost Q,W <= cost R,W ; :: thesis:

now

let u be oriented Chain of G; :: thesis:
assume u is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis:
then cost s,W <= cost u,W by A15, Def18;
hence cost Q,W <= cost u,W by A18, XXREAL_0:2; :: thesis:

end;

hence Q is_shortestpath_of v1,v3,V \/ {v2},W by A13, Def18; :: thesis:

end;

hereby :: thesis:

assume A19: cost Q,W >= cost R,W ; :: thesis:

now

let u be oriented Chain of G; :: thesis:
assume u is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis:
then cost s,W <= cost u,W by A15, Def18;
then cost Q,W <= cost u,W by A18, XXREAL_0:2;
hence cost R,W <= cost u,W by A19, XXREAL_0:2; :: thesis:

end;

hence R is_shortestpath_of v1,v3,V \/ {v2},W by A16, Def18; :: thesis:

end;

set FT = the Target of G;
set FS = the Source of G;
A20: ( the Source of G . e = v2 & the Target of G . e = v3 ) by A9, GRAPH_4:def 1;
A21: s is_orientedpath_of v1,v3,V \/ {v2} by A15, Def18;
then A22: s is_orientedpath_of v1,v3 by Def4;
then A23: the Target of G . (s . (len s)) = v3 by Def3;
s <> {} by A22, Def3;
then A24: len s >= 1 by FINSEQ_1:28;

per cases ;

suppose len s >= 2 ; :: thesis:

then consider k being Nat such that
A25: len s = (1 + 1) + k by NAT_1:10;
A26: (V \/ {v2}) \ {v2} = V \ {v2} by XBOOLE_1:40;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A27: len s = 1 + (1 + k) by A25;
then consider s1, s2 being FinSequence such that
A28: len s1 = 1 + k and
A29: len s2 = 1 and
A30: s = s1 ^ s2 by FINSEQ_2:25;
reconsider s1 = s1, s2 = s2 as oriented Simple Chain of G by A30, Th17;
A31: len s1 >= 1 by A28, NAT_1:12;
A32: the Source of G . (s . 1) = v1 by A22, Def3;
then A33: the Source of G . (s1 . 1) = v1 by A30, A31, Lm1;
len s2 = 1 by A29;
then A34: not v3 in vertices s1 by A6, A23, A30, A31, A32, Th21;
A35: s2 . 1 = s . (len s) by A27, A28, A29, A30, Lm2;
then A36: (vertices s) \ {v3} = ((vertices s1) \/ {v3}) \ {v3} by A23, A28, A29, A30, Th31, NAT_1:12
.= (vertices s1) \ {v3} by XBOOLE_1:40
.= vertices s1 by A34, ZFMISC_1:65 ;
then vertices s1 c= V \/ {v2} by A21, Def4;
then (vertices s1) \ {v2} c= (V \/ {v2}) \ {v2} by XBOOLE_1:33;
then A37: (vertices s1) \ {v2} c= V by A26, XBOOLE_1:1;
A38: len s1 < len s by A27, A28, NAT_1:13;
then A39: the Source of G . (s . ((len s1) + 1)) = the Target of G . (s . (len s1)) by A31, GRAPH_1:def 13;
A40: s1 . (len s1) = s . (len s1) by A30, A31, Lm1;
then A41: the Source of G . (s2 . 1) = the Target of G . (s1 . (len s1)) by A27, A28, A35, A31, A38, GRAPH_1:def 13;
A42: cost s,W = (cost s1,W) + (cost s2,W) by A2, A30, Th50, Th58;
A43: not v1 in vertices s2 by A6, A23, A29, A30, A31, A32, Th21;

hereby :: thesis:

per cases ;

suppose v2 in vertices s1 ; :: thesis:

then consider i being Element of NAT such that
A44: 1 <= i and
A45: i <= len s1 and
A46: v2 = the Target of G . (s1 . i) by A5, A33, Th32;
s2 /. 1 in the carrier' of G by A1;
then A47: s2 . 1 in the carrier' of G by A29, FINSEQ_4:24;

hereby :: thesis:

per cases ;

suppose A48: the Source of G . (s2 . 1) = v2 ; :: thesis:

s1 <> {} by A28;
then s1 is_orientedpath_of v1,v2 by A33, A41, A48, Def3;
then s1 is_orientedpath_of v1,v2,V by A37, Def4;
then A49: cost P,W <= cost s1,W by A4, Def18;
s2 . 1 = e by A1, A23, A20, A35, A47, A48, GRAPH_1:def 5;
then s2 = pe by A29, FINSEQ_1:57;
then cost R,W = (cost P,W) + (cost s2,W) by A2, A7, Th50, Th58;
then A50: cost R,W <= cost s,W by A42, A49, XREAL_1:9;

hereby :: thesis:

assume cost Q,W <= cost R,W ; :: thesis:
then A51: cost Q,W <= cost s,W by A50, XXREAL_0:2;

now

let u be oriented Chain of G; :: thesis:
assume u is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis:
then cost s,W <= cost u,W by A15, Def18;
hence cost Q,W <= cost u,W by A51, XXREAL_0:2; :: thesis:

end;

hence Q is_shortestpath_of v1,v3,V \/ {v2},W by A13, Def18; :: thesis:

end;

hereby :: thesis:

assume cost Q,W >= cost R,W ; :: thesis:

now

let u be oriented Chain of G; :: thesis:
assume u is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis:
then cost s,W <= cost u,W by A15, Def18;
hence cost R,W <= cost u,W by A50, XXREAL_0:2; :: thesis:

end;

hence R is_shortestpath_of v1,v3,V \/ {v2},W by A16, Def18; :: thesis:

end;

suppose A52: the Source of G . (s2 . 1) <> v2 ; :: thesis:

len s1 in dom s1 by A31, FINSEQ_3:27;
then reconsider vx = the Target of G . (s1 . (len s1)) as Vertex of G by FINSEQ_2:13, FUNCT_2:7;
A53: not vx in {v2} by A41, A52, TARSKI:def 1;
len s1 in dom s1 by A31, FINSEQ_3:27;
then A54: vx in vertices s1 by Th28;
vertices s1 c= V \/ {v2} by A21, A36, Def4;
then A55: vx in V by A54, A53, XBOOLE_0:def 3;
{vx} c= V

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {vx} ; :: thesis:
hence x in V by A55, TARSKI:def 1; :: thesis:

end;

then A56: V \/ {vx} c= V by XBOOLE_1:8;
1 in dom s2 by A29, FINSEQ_3:27;
then vx <> v1 by A25, A28, A35, A40, A43, A39, Th28;
then consider q9 being oriented Chain of G such that
A57: q9 is_shortestpath_of v1,vx,V,W and
A58: cost q9,W <= cost P,W by A10, A55, Def19;
consider j being Nat such that
A59: len s1 = i + j by A45, NAT_1:10;
A60: q9 is_orientedpath_of v1,vx,V by A57, Def18;
then A61: q9 is_orientedpath_of v1,vx by Def4;
then q9 <> {} by Def3;
then A62: len q9 >= 1 by FINSEQ_1:28;
the Target of G . (q9 . (len q9)) = vx by A61, Def3;
then reconsider qx = q9 ^ s2 as oriented Chain of G by A25, A28, A35, A40, A39, Th15;
len qx = (len q9) + 1 by A29, FINSEQ_1:35;
then A63: ( qx <> {} & the Target of G . (qx . (len qx)) = v3 ) by A23, A29, A35, Lm2;
the Source of G . (q9 . 1) = v1 by A61, Def3;
then the Source of G . (qx . 1) = v1 by A62, Lm1;
then A64: qx is_orientedpath_of v1,v3 by A63, Def3;
(vertices q9) \ {vx} c= V by A60, Def4;
then vertices q9 c= V \/ {vx} by XBOOLE_1:44;
then vertices q9 c= V by A56, XBOOLE_1:1;
then A65: (vertices q9) \ {v3} c= V \ {v3} by XBOOLE_1:33;
vertices qx = (vertices q9) \/ {v3} by A23, A29, A35, A62, Th31;
then (vertices qx) \ {v3} = (vertices q9) \ {v3} by XBOOLE_1:40;
then (vertices qx) \ {v3} c= V by A65, XBOOLE_1:1;
then qx is_orientedpath_of v1,v3,V by A64, Def4;
then A66: cost Q,W <= cost qx,W by A8, Def18;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
consider t1, t2 being FinSequence such that
A67: len t1 = i and
len t2 = j and
A68: s1 = t1 ^ t2 by A59, FINSEQ_2:25;
reconsider t1 = t1, t2 = t2 as oriented Simple Chain of G by A68, Th17;
A69: the Target of G . (t1 . (len t1)) = v2 by A44, A46, A67, A68, Lm1;
vertices t1 c= vertices (t1 ^ t2) by Th30;
then (vertices t1) \ {v2} c= (vertices s1) \ {v2} by A68, XBOOLE_1:33;
then A70: (vertices t1) \ {v2} c= V by A37, XBOOLE_1:1;
( t1 <> {} & the Source of G . (t1 . 1) = v1 ) by A33, A44, A67, A68, Lm1;
then t1 is_orientedpath_of v1,v2 by A69, Def3;
then t1 is_orientedpath_of v1,v2,V by A70, Def4;
then A71: cost P,W <= cost t1,W by A4, Def18;
A72: cost t2,W >= 0 by A2, Th54;
cost s1,W = (cost t1,W) + (cost t2,W) by A2, A68, Th50, Th58;
then (cost t1,W) + 0 <= cost s1,W by A72, XREAL_1:9;
then cost P,W <= cost s1,W by A71, XXREAL_0:2;
then A73: cost q9,W <= cost s1,W by A58, XXREAL_0:2;
cost qx,W = (cost q9,W) + (cost s2,W) by A2, Th50, Th58;
then cost qx,W <= cost s,W by A42, A73, XREAL_1:9;
then A74: cost Q,W <= cost s,W by A66, XXREAL_0:2;

hereby :: thesis:

assume cost Q,W <= cost R,W ; :: thesis:

now

let u be oriented Chain of G; :: thesis:
assume u is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis:
then cost s,W <= cost u,W by A15, Def18;
hence cost Q,W <= cost u,W by A74, XXREAL_0:2; :: thesis:

end;

hence Q is_shortestpath_of v1,v3,V \/ {v2},W by A13, Def18; :: thesis:

end;

hereby :: thesis:

assume cost Q,W >= cost R,W ; :: thesis:
then A75: cost R,W <= cost s,W by A74, XXREAL_0:2;

now

let u be oriented Chain of G; :: thesis:
assume u is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis:
then cost s,W <= cost u,W by A15, Def18;
hence cost R,W <= cost u,W by A75, XXREAL_0:2; :: thesis:

end;

hence R is_shortestpath_of v1,v3,V \/ {v2},W by A16, Def18; :: thesis:

end;

suppose not v2 in vertices s1 ; :: thesis:

then A76: (vertices s1) \ {v2} = vertices s1 by ZFMISC_1:65;
then (vertices s1) \ {v2} c= V \/ {v2} by A21, A36, Def4;
then (vertices s) \ {v3} c= V by A36, A76, XBOOLE_1:43;
then s is_orientedpath_of v1,v3,V by A22, Def4;
hence ( ( cost Q,W <= cost R,W implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost Q,W >= cost R,W implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) by A8, A17, Def18; :: thesis:

end;

suppose len s < 1 + 1 ; :: thesis:

then A77: len s <= 1 by NAT_1:13;
then A78: len s = 1 by A24, XXREAL_0:1;
A79: vertices s = vertices (s /. 1) by A24, A77, Th29, XXREAL_0:1;
(vertices s) \ {v3} c= V

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A80: x in (vertices s) \ {v3} ; :: thesis:
then A81: not x in {v3} by XBOOLE_0:def 5;
x in vertices (s /. 1) by A79, A80, XBOOLE_0:def 5;
then A82: ( x = the Source of G . (s /. 1) or x = the Target of G . (s /. 1) ) by TARSKI:def 2;
A83: s /. 1 = s . 1 by A24, FINSEQ_4:24;
v3 = the Target of G . (s . (len s)) by A22, Def3
.= the Target of G . (s /. 1) by A78, FINSEQ_4:24 ;
hence x in V by A22, A12, A81, A82, A83, Def3, TARSKI:def 1; :: thesis:

end;

then s is_orientedpath_of v1,v3,V by A22, Def4;
hence ( ( cost Q,W <= cost R,W implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost Q,W >= cost R,W implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) by A8, A17, Def18; :: thesis:

end;