theorem :: FINSEQ_1:11

for f being Function st ex k being Nat st dom f c= Seg k holds
ex p being FinSequence st f c= p