theorem :: FUNCT_1:54

for Y being set
for x being object
for f being Function holds
( x in dom (Y |` f) iff ( x in dom f & f . x in Y ) ) by Th52;