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 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 :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len q holds
not q . n = q . m

let n, m be Nat; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: contradiction
then vs . m = vs . n by A4, A10, A9, FINSEQ_1:def 7;
hence contradiction by A2, A6, A7, A11; :: thesis: 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; :: thesis: verum