let X, Y be set ; :: thesis: Y misses rng <:(X --> Y),(id X):>
set h = <:(X --> Y),(id X):>;

now :: thesis: for y being object holds
( not y in Y or not y in rng <:(X --> Y),(id X):> )

given y being object such that A1: ( y in Y & y in rng <:(X --> Y),(id X):> ) ; :: thesis: contradiction
consider x being object such that
A2: ( x in dom <:(X --> Y),(id X):> & y = <:(X --> Y),(id X):> . x ) by A1, FUNCT_1:def 3;
x in X by A2, Lm8;
then A3: y = [Y,x] by A2, Lm9
.= {{Y,x},{Y}} by TARSKI:def 5 ;
A4: {Y} in {{Y,x},{Y}} by TARSKI:def 2;
Y in {Y} by TARSKI:def 1;
hence contradiction by A1, A3, A4, XREGULAR:7; :: thesis: verum

end;

hence Y misses rng <:(X --> Y),(id X):> by XBOOLE_0:3; :: thesis: verum