theorem Th32: :: FINSEQ_5:32

for i being Nat
for D being set
for f being FinSequence of D st len f <= i holds
f /^ i is empty