theorem :: FUNCT_3:8

for f being Function holds (.: f) . {} = {}