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