theorem Th2: :: FILEREC1:2

for f being FinSequence holds f | (len f) = f