for P, X, Y being set
for f being Function of X,Y
for y being object st y in f .: P holds
ex c being Element of X st
( c in P & y = f . c )