theorem Th2: :: FINSEQ_8:2

for f being FinSequence
for i being Nat st i >= len f holds
f /^ i = {}