theorem :: FINSEQ_1:103

for f being natural-valued FinSequence holds f is FinSequence of NAT