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 & ( for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) ) )
by GRAPH_4:def 7;
A2:
( len vs = (len p) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds
p . n orientedly_joins vs /. n,vs /. (n + 1) ) )
by A1, GRAPH_4:def 5;
now let n,
m be
Element of
NAT ;
:: thesis: ( 1 <= n & n < m & m <= len p implies not p . n = p . m )assume A3:
( 1
<= n &
n < m &
m <= len p )
;
:: thesis: not p . n = p . massume A4:
p . n = p . m
;
:: thesis: contradictionA5:
n <= len p
by A3, XXREAL_0:2;
A6:
1
<= m
by A3, XXREAL_0:2;
then A7:
p . m orientedly_joins vs /. m,
vs /. (m + 1)
by A1, A3, GRAPH_4:def 5;
p . n orientedly_joins vs /. n,
vs /. (n + 1)
by A1, A3, A5, GRAPH_4:def 5;
then A8:
vs /. n =
the
Source of
G . (p . m)
by A4, GRAPH_4:def 1
.=
vs /. m
by A7, GRAPH_4:def 1
;
A9:
len p < len vs
by A2, XREAL_1:31;
then
n <= len vs
by A5, XXREAL_0:2;
then
n in dom vs
by A3, FINSEQ_3:27;
then A10:
vs . n = vs /. n
by PARTFUN1:def 8;
A11:
m <= len vs
by A3, A9, XXREAL_0:2;
then
m in dom vs
by A6, FINSEQ_3:27;
then
vs . m = vs . n
by A8, A10, PARTFUN1:def 8;
then
m = len vs
by A1, A3, A11;
hence
contradiction
by A2, A3, XREAL_1:31;
:: thesis: verum end;
hence
p is one-to-one
by Th9; :: thesis: verum