let G be finite Graph; for ps being oriented Simple Chain of G holds len ps <= VerticesCount G
let ps be oriented Simple Chain of G; len ps <= VerticesCount G
set VV = the carrier of G;
consider vs being FinSequence of the carrier of G such that
A1:
vs is_oriented_vertex_seq_of ps
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;
reconsider V = the carrier of G as finite set ;
A3:
len vs = (len ps) + 1
by A1, GRAPH_4:def 5;
then
vs <> {}
;
then consider q being FinSequence, x being object such that
A4:
vs = q ^ <*x*>
by FINSEQ_1:46;
A5: (len ps) + 1 =
(len q) + (len <*x*>)
by A3, A4, FINSEQ_1:22
.=
(len q) + 1
by FINSEQ_1:39
;
now for n, m being Nat st 1 <= n & n < m & m <= len q holds
not q . n = q . mlet n,
m be
Nat;
( 1 <= n & n < m & m <= len q implies not q . n = q . m )assume that A6:
1
<= n
and A7:
n < m
and A8:
m <= len q
;
not q . n = q . m
1
<= m
by A6, A7, XXREAL_0:2;
then A9:
m in dom q
by A8, FINSEQ_3:25;
n <= len q
by A7, A8, XXREAL_0:2;
then
n in dom q
by A6, FINSEQ_3:25;
then A10:
vs . n = q . n
by A4, FINSEQ_1:def 7;
len q < len vs
by A3, A5, XREAL_1:29;
then A11:
m < len vs
by A8, XXREAL_0:2;
assume
q . n = q . m
;
contradictionthen
vs . m = vs . n
by A4, A10, A9, FINSEQ_1:def 7;
hence
contradiction
by A2, A6, A7, A11;
verum end;
then A12:
card (rng q) = len q
by Th5;
( rng vs c= the carrier of G & rng q c= rng vs )
by A4, FINSEQ_1:29, FINSEQ_1:def 4;
then
card (rng q) <= card V
by NAT_1:43, XBOOLE_1:1;
hence
len ps <= VerticesCount G
by A5, A12, GRAPH_1:def 19; verum