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