for P, X, Y being set
for f being Function of X,Y st Y <> {} holds
for y being object st ex x being object st
( x in X & x in P & y = f . x ) holds
y in f .: P