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