theorem :: GRFUNC_1:22

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