take <*> X ; :: thesis: <*> X is X -valued
rng (<*> X) c= X by XBOOLE_1:2;
hence <*> X is X -valued by RELAT_1:def 19; :: thesis: verum