let ss be subsequence of s; :: thesis: ss is X -valued
rng ss c= rng s by Lm1;
hence rng ss c= X by XBOOLE_1:1; :: according to RELAT_1:def 19 :: thesis: verum