let G be Graph; for p being oriented Simple Chain of G holds p is V18()
let p be oriented Simple Chain of G; p is V18()
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 for n, m being Nat st 1 <= n & n < m & m <= len p holds
not p . n = p . mlet n,
m be
Nat;
( 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
;
not p . n = p . mA7:
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
;
contradictionA10:
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;
verum end;
hence
p is V18()
by Th4; verum