theorem Th11: :: NUMERAL2:11

for F being XFinSequence holds F = SubXFinS (F,NAT)