for p being FinSequence
for n being Nat
for G being Graph st p is OrientedPath of G holds
p | (Seg n) is OrientedPath of G