theorem Th3: :: NUMERAL2:3

for f being XFinSequence holds mid (f,2,(len f)) = f /^ 1