theorem :: GRFUNC_1:24

for Y being set
for x being object
for f being Function holds
( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f )