theorem Th22: :: PARTFUN2:22

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