theorem Th40: :: GRAPH_2:40

for n being Nat
for G being Graph
for vs, vs1 being FinSequence of the carrier of G
for c, c1 being Chain of G st vs is_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds
vs1 is_vertex_seq_of c1