:: deftheorem defines is_vertex_seq_at GRAPHSP:def 17 :
for p being FinSequence of NAT
for f being Element of REAL *
for i, n being Nat holds
( p is_vertex_seq_at f,i,n iff ( p . (len p) = i & ( for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = f . (n + (p /. (((len p) - k) + 1))) ) ) );