let i, n be Nat; :: thesis: for V being set

for f, g being Element of REAL *

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 f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) holds

g . (n + i) <> - 1

let V be set ; :: thesis: for f, g being Element of REAL *

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 f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) holds

g . (n + i) <> - 1

let f, g be Element of REAL * ; :: 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 f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) holds

g . (n + i) <> - 1

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 f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) holds

g . (n + i) <> - 1

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 f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) holds

g . (n + i) <> - 1

let W be Function of the carrier' of G,Real>=0; :: thesis: for v1, v2 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) holds

g . (n + i) <> - 1

let v1, v2 be Vertex of G; :: thesis: ( f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) implies g . (n + i) <> - 1 )

assume that

A1: f is_Input_of_Dijkstra_Alg G,n,W and

A2: W is_weight>=0of G and

A3: v2 = i and

A4: v1 <> v2 and

A5: ( 1 <= i & i <= n ) and

A6: P is_shortestpath_of v1,v2,V,W and

A7: for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ; :: thesis: g . (n + i) <> - 1

P is_orientedpath_of v1,v2,V by A6, GRAPH_5:def 18;

then consider q being oriented Simple Chain of G such that

A8: q is_shortestpath_of v1,v2,V,W by A2, GRAPH_5:62;

set FT = the Target of G;

assume A9: g . (n + i) = - 1 ; :: thesis: contradiction

set e = q . (len q);

consider vs being FinSequence of the carrier of G such that

A10: vs is_oriented_vertex_seq_of q and

A11: for n1, m1 being Nat st 1 <= n1 & n1 < m1 & m1 <= len vs & vs . n1 = vs . m1 holds

( n1 = 1 & m1 = len vs ) by GRAPH_4:def 7;

A12: q is_orientedpath_of v1,v2,V by A8, GRAPH_5:def 18;

then A13: q is_orientedpath_of v1,v2 by GRAPH_5:def 4;

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

then A14: len q >= 1 by FINSEQ_1:20;

then A15: q . (len q) orientedly_joins vs /. (len q),vs /. ((len q) + 1) by A10, GRAPH_4:def 5;

len q in dom q by A14, FINSEQ_3:25;

then A16: q . (len q) in the carrier' of G by FINSEQ_2:11;

A17: len vs = (len q) + 1 by A10, GRAPH_4:def 5;

then A18: len q < len vs by NAT_1:13;

then A19: len q in dom vs by A14, FINSEQ_3:25;

A20: vs /. (len q) = vs . (len q) by A14, A18, FINSEQ_4:15;

then reconsider v3 = vs . (len q) as Vertex of G ;

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

then A21: v2 = vs /. ((len q) + 1) by A15, GRAPH_4:def 1;

A22: 1 < (len q) + 1 by A14, NAT_1:13;

then A23: v2 = vs . (len vs) by A17, A21, FINSEQ_4:15;

Seg n = the carrier of G by A1;

then v3 in Seg n by A19, FINSEQ_2:11;

then reconsider m = v3 as Element of NAT ;

A27: f . (((2 * n) + (n * m)) + i) = Weight (v3,v2,W) by A1, A3;

v3 = the Source of G . (q . (len q)) by A15, A20, GRAPH_4:def 1;

then v3 in vertices q by A14, Lm4;

then A28: m in (vertices q) \ {v2} by A26, XBOOLE_0:def 5;

(vertices q) \ {v2} c= V by A12, GRAPH_5:def 4;

then f . (((2 * n) + (n * m)) + i) = - 1 by A5, A7, A9, A28;

hence contradiction by A15, A16, A20, A21, A27, Th23; :: thesis: verum

for f, g being Element of REAL *

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 f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) holds

g . (n + i) <> - 1

let V be set ; :: thesis: for f, g being Element of REAL *

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 f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) holds

g . (n + i) <> - 1

let f, g be Element of REAL * ; :: 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 f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) holds

g . (n + i) <> - 1

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 f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) holds

g . (n + i) <> - 1

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 f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) holds

g . (n + i) <> - 1

let W be Function of the carrier' of G,Real>=0; :: thesis: for v1, v2 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) holds

g . (n + i) <> - 1

let v1, v2 be Vertex of G; :: thesis: ( f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) implies g . (n + i) <> - 1 )

assume that

A1: f is_Input_of_Dijkstra_Alg G,n,W and

A2: W is_weight>=0of G and

A3: v2 = i and

A4: v1 <> v2 and

A5: ( 1 <= i & i <= n ) and

A6: P is_shortestpath_of v1,v2,V,W and

A7: for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ; :: thesis: g . (n + i) <> - 1

P is_orientedpath_of v1,v2,V by A6, GRAPH_5:def 18;

then consider q being oriented Simple Chain of G such that

A8: q is_shortestpath_of v1,v2,V,W by A2, GRAPH_5:62;

set FT = the Target of G;

assume A9: g . (n + i) = - 1 ; :: thesis: contradiction

set e = q . (len q);

consider vs being FinSequence of the carrier of G such that

A10: vs is_oriented_vertex_seq_of q and

A11: for n1, m1 being Nat st 1 <= n1 & n1 < m1 & m1 <= len vs & vs . n1 = vs . m1 holds

( n1 = 1 & m1 = len vs ) by GRAPH_4:def 7;

A12: q is_orientedpath_of v1,v2,V by A8, GRAPH_5:def 18;

then A13: q is_orientedpath_of v1,v2 by GRAPH_5:def 4;

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

then A14: len q >= 1 by FINSEQ_1:20;

then A15: q . (len q) orientedly_joins vs /. (len q),vs /. ((len q) + 1) by A10, GRAPH_4:def 5;

len q in dom q by A14, FINSEQ_3:25;

then A16: q . (len q) in the carrier' of G by FINSEQ_2:11;

A17: len vs = (len q) + 1 by A10, GRAPH_4:def 5;

then A18: len q < len vs by NAT_1:13;

then A19: len q in dom vs by A14, FINSEQ_3:25;

A20: vs /. (len q) = vs . (len q) by A14, A18, FINSEQ_4:15;

then reconsider v3 = vs . (len q) as Vertex of G ;

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

then A21: v2 = vs /. ((len q) + 1) by A15, GRAPH_4:def 1;

A22: 1 < (len q) + 1 by A14, NAT_1:13;

then A23: v2 = vs . (len vs) by A17, A21, FINSEQ_4:15;

now :: thesis: not v3 = v2

then A26:
not v3 in {v2}
by TARSKI:def 1;A24:
q . 1 orientedly_joins vs /. 1,vs /. (1 + 1)
by A10, A14, GRAPH_4:def 5;

assume A25: v3 = v2 ; :: thesis: contradiction

v1 = the Source of G . (q . 1) by A13, GRAPH_5:def 3

.= vs /. 1 by A24, GRAPH_4:def 1

.= vs . 1 by A17, A22, FINSEQ_4:15

.= v3 by A11, A14, A18, A23, A25 ;

hence contradiction by A4, A25; :: thesis: verum

end;assume A25: v3 = v2 ; :: thesis: contradiction

v1 = the Source of G . (q . 1) by A13, GRAPH_5:def 3

.= vs /. 1 by A24, GRAPH_4:def 1

.= vs . 1 by A17, A22, FINSEQ_4:15

.= v3 by A11, A14, A18, A23, A25 ;

hence contradiction by A4, A25; :: thesis: verum

Seg n = the carrier of G by A1;

then v3 in Seg n by A19, FINSEQ_2:11;

then reconsider m = v3 as Element of NAT ;

A27: f . (((2 * n) + (n * m)) + i) = Weight (v3,v2,W) by A1, A3;

v3 = the Source of G . (q . (len q)) by A15, A20, GRAPH_4:def 1;

then v3 in vertices q by A14, Lm4;

then A28: m in (vertices q) \ {v2} by A26, XBOOLE_0:def 5;

(vertices q) \ {v2} c= V by A12, GRAPH_5:def 4;

then f . (((2 * n) + (n * m)) + i) = - 1 by A5, A7, A9, A28;

hence contradiction by A15, A16, A20, A21, A27, Th23; :: thesis: verum