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