let ss be subsequence of s; :: thesis: ss is sequence of X
( rng ss c= X & dom ss = NAT ) by PARTFUN1:def 2;
hence ss is sequence of X by RELSET_1:4; :: thesis: verum