let G be Graph; :: thesis: for p being oriented Simple Chain of G holds p is one-to-one
let p be oriented Simple Chain of G; :: thesis: p is one-to-one
set VV = the carrier of G;
consider vs being FinSequence of the carrier of G such that
A1: vs is_oriented_vertex_seq_of p and
A2: for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) by GRAPH_4:def 7;
A3: len vs = (len p) + 1 by A1, GRAPH_4:def 5;

now :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len p holds
not p . n = p . m

let n, m be Nat; :: thesis: ( 1 <= n & n < m & m <= len p implies not p . n = p . m )
assume that
A4: 1 <= n and
A5: n < m and
A6: m <= len p ; :: thesis: not p . n = p . m
A7: 1 <= m by A4, A5, XXREAL_0:2;
then A8: p . m orientedly_joins vs /. m,vs /. (m + 1) by A1, A6, GRAPH_4:def 5;
assume A9: p . n = p . m ; :: thesis: contradiction
A10: n <= len p by A5, A6, XXREAL_0:2;
then p . n orientedly_joins vs /. n,vs /. (n + 1) by A1, A4, GRAPH_4:def 5;
then A11: vs /. n = the Source of G . (p . m) by A9, GRAPH_4:def 1
.= vs /. m by A8, GRAPH_4:def 1 ;
A12: len p < len vs by A3, XREAL_1:29;
then n <= len vs by A10, XXREAL_0:2;
then n in dom vs by A4, FINSEQ_3:25;
then A13: vs . n = vs /. n by PARTFUN1:def 6;
A14: m <= len vs by A6, A12, XXREAL_0:2;
then m in dom vs by A7, FINSEQ_3:25;
then vs . m = vs . n by A11, A13, PARTFUN1:def 6;
then m = len vs by A2, A4, A5, A14;
hence contradiction by A3, A6, XREAL_1:29; :: thesis: verum

end;

hence p is one-to-one by Th4; :: thesis: verum