take M = I --> X; :: thesis: M is bool X -valued
for a being object st a in rng M holds
a in bool X

proof

let a be object ; :: thesis: ( a in rng M implies a in bool X )
assume a in rng M ; :: thesis: a in bool X
then ex x being object st
( x in dom M & a = M . x ) by FUNCT_1:def 3;
then a = X by FUNCOP_1:7;
hence a in bool X by ZFMISC_1:def 1; :: thesis: verum

end;

hence M is bool X -valued by RELAT_1:def 19, TARSKI:def 3; :: thesis: verum