theorem :: FUNCT_2:36

for P, X, Y being set
for f being Function of X,Y holds f .: P c= Y ;