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