for G being _Graph
for p being FinSequence of the_Vertices_of G
for q being FinSequence of the_Edges_of G st len p = 1 + (len q) & ( for n being Element of NAT st 1 <= n & n + 1 <= len p holds
q . n Joins p . n,p . (n + 1),G ) holds
ex W being Walk of G st
( W .vertexSeq() = p & W .edgeSeq() = q )