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