let G be finite Graph; :: thesis: for ps being oriented Simple Chain of G holds len ps <= VerticesCount G
let ps be oriented Simple Chain of G; :: thesis: 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 & ( 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 ps) + 1 by A1, GRAPH_4:def 5;
then vs <> {} ;
then consider q being FinSequence, x being set such that
A3: vs = q ^ <*x*> by FINSEQ_1:63;
A4: (len ps) + 1 = (len q) + (len <*x*>) by A2, A3, FINSEQ_1:35
.= (len q) + 1 by FINSEQ_1:56 ;

now

let n, m be Element of NAT ; :: thesis: ( 1 <= n & n < m & m <= len q implies not q . n = q . m )
assume A5: ( 1 <= n & n < m & m <= len q ) ; :: thesis: not q . n = q . m
assume A6: q . n = q . m ; :: thesis: contradiction
len q < len vs by A2, A4, XREAL_1:31;
then A7: m < len vs by A5, XXREAL_0:2;
A8: n <= len q by A5, XXREAL_0:2;
A9: 1 <= m by A5, XXREAL_0:2;
n in dom q by A5, A8, FINSEQ_3:27;
then A10: vs . n = q . n by A3, FINSEQ_1:def 7;
m in dom q by A5, A9, FINSEQ_3:27;
then vs . m = vs . n by A3, A6, A10, FINSEQ_1:def 7;
hence contradiction by A1, A5, A7; :: thesis: verum

end;

then A11: card (rng q) = len q by Th10;
A12: rng vs c= the carrier of G by FINSEQ_1:def 4;
reconsider V = the carrier of G as finite set ;
rng q c= rng vs by A3, FINSEQ_1:42;
then card (rng q) <= card V by A12, NAT_1:44, XBOOLE_1:1;
hence len ps <= VerticesCount G by A4, A11, GRAPH_1:def 19; :: thesis: verum