id X is Function of X,X ;
hence id X is Element of Funcs (X,X) by FUNCT_2:9; :: thesis: verum