theorem :: PARTFUN1:49

for X being set holds PFuncs (X,{}) = {{}}