theorem Th24: :: PARTFUN1:24

for x being object
for X, Y being set
for f being Function holds
( x in dom <:f,X,Y:> iff ( x in dom f & x in X & f . x in Y ) )