take M = Y --> the Element of X; :: thesis: M is X -valued
A1: { the Element of X} c= X by ZFMISC_1:31;
rng M c= { the Element of X} by FUNCOP_1:13;
hence rng M c= X by A1; :: according to RELAT_1:def 19 :: thesis: verum