theorem :: PARTFUN2:20

for X being set
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D holds
( c in dom (X |` f) iff ( c in dom f & f /. c in X ) ) by Th19;