theorem Th79: :: FINSEQ_1:79

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