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