theorem :: FUNCT_2:49

for P, Y being set
for x being object
for f being Function of {x},Y st Y <> {} holds
f .: P c= {(f . x)}