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