let X, Y be set ; :: thesis: not Y in rng <:(X --> Y),(id X):>
set h = <:(X --> Y),(id X):>;
assume Y in rng <:(X --> Y),(id X):> ; :: thesis: contradiction
then consider x being object such that
A1: ( x in dom <:(X --> Y),(id X):> & <:(X --> Y),(id X):> . x = Y ) by FUNCT_1:def 3;
x in X by A1, Lm8;
then Y = [Y,x] by A1, Lm9
.= {{Y,x},{Y}} by TARSKI:def 5 ;
then ( {Y} in Y & Y in {Y} ) by TARSKI:def 1, TARSKI:def 2;
hence contradiction ; :: thesis: verum