theorem Th2: :: GRAPH_2:2

for p, q being FinSequence
for n being Nat st q = p | (Seg n) holds
( len q <= len p & ( for i being Nat st 1 <= i & i <= len q holds
p . i = q . i ) )