:: deftheorem defines is_oriented_edge_seq_of GRAPHSP:def 19 :
for G being Graph
for p being FinSequence of the carrier' of G
for vs being FinSequence holds
( p is_oriented_edge_seq_of vs iff ( len vs = (len p) + 1 & ( for n being Nat st 1 <= n & n <= len p holds
( the Source of G . (p . n) = vs . n & the Target of G . (p . n) = vs . (n + 1) ) ) ) );