theorem :: PARTFUN1:73

for Y being set
for f being PartFunc of {},Y holds TotFuncs f = {f} by Th72;