( dom (id X) = X & rng (id X) = X ) ;
then id X is Function of X,X by FUNCT_2:1;
hence id X is Element of Funcs (X,X) by FUNCT_2:9; :: thesis: verum