take M = Y --> the Element of X; :: thesis: M is X -valued
A: { the Element of X} c= X by ZFMISC_1:37;
rng M c= { the Element of X} by FUNCOP_1:19;
hence rng M c= X by A, XBOOLE_1:1; :: according to RELAT_1:def 19 :: thesis: verum