thus F . (c,d) is PartFunc of X,ExtREAL by PARTFUN1:47; :: thesis: verum