id X is Function of X,X ;
hence id X is Element of Funcs X,X by FUNCT_2:12; :: thesis: verum