for X being non empty set
for f being FinSequence of X
for f1 being FinSequence of the carrier of (PGraph X) st len f >= 1 & f = f1 holds
f1 is_oriented_vertex_seq_of PairF f