theorem Th29: :: PARTFUN2:29

for C, D being non empty set
for SC being Subset of C
for c being Element of C
for d being Element of D st c in SC holds
(SC --> d) /. c = d