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