ex f being Function st
( F . k = f & dom f = NAT & rng f c= X ) by FUNCT_2:def 2;
hence F . k is sequence of X by FUNCT_2:2; :: thesis: verum