X --> c is PartFunc of D,C ;
hence X --> c is Element of PFuncs (D,C) by PARTFUN1:45; :: thesis: verum