theorem Th32: :: FINSEQ_5:32

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