theorem :: FUNCT_2:45

for P, Y being set
for f being Function of {},Y holds f .: P = {} ;