for p, q being FinSequence of NAT
for f being Element of REAL *
for i, n being Element of NAT st p is_simple_vertex_seq_at f,i,n & q is_simple_vertex_seq_at f,i,n holds
p = q