theorem Th47: :: FINSEQ_3:49

for p being FinSequence
for n being Nat holds
( p | (Seg n) = p iff len p <= n )