:: deftheorem defines is_oriented_vertex_seq_of GRAPH_4:def 5 :
for G being Graph
for vs being FinSequence of the carrier of G
for c being FinSequence holds
( vs is_oriented_vertex_seq_of c iff ( len vs = (len c) + 1 & ( for n being Nat st 1 <= n & n <= len c holds
c . n orientedly_joins vs /. n,vs /. (n + 1) ) ) );