theorem :: PARTFUN2:23

for X being set
for C, D being non empty set
for d being Element of D
for f being PartFunc of C,D holds
( d in f .: X iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) by Th22;