theorem :: PARTFUN2:55

for C, D being non empty set
for SD being Subset of D
for c being Element of C
for f being PartFunc of C,D holds
( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )