( rng (s ^\ k) c= X & dom (s ^\ k) = NAT ) by PARTFUN1:def 2, RELAT_1:def 19;
hence s ^\ k is sequence of X by RELSET_1:4; :: thesis: verum