x in {x} by TARSKI:def 1;
then x in dom ({x} --> y) ;
then A1: x in dom (x .--> y) by FUNCOP_1:def 9;
( x is set & y is set ) by TARSKI:1;
hence proj ((x .--> y),x) is one-to-one by A1, Th19; :: thesis: verum