:: deftheorem defines is_simple_vertex_seq_at GRAPHSP:def 18 :
for p being FinSequence of NAT
for f being Element of REAL *
for i, n being Nat holds
( p is_simple_vertex_seq_at f,i,n iff ( p . 1 = 1 & len p > 1 & p is_vertex_seq_at f,i,n & p is one-to-one ) );