let X, Y be set ; :: thesis: Y \/ {Y} misses rng <:(X --> Y),(id X):>
set h = <:(X --> Y),(id X):>;
A1: Y misses rng <:(X --> Y),(id X):> by Lm11;
{Y} misses rng <:(X --> Y),(id X):> by Lm20, ZFMISC_1:50;
hence Y \/ {Y} misses rng <:(X --> Y),(id X):> by A1, XBOOLE_1:70; :: thesis: verum