theorem :: PARTFUN2:31

for C, D, E being non empty set
for SE being Subset of E
for c being Element of C
for f being PartFunc of C,D st c in dom f holds
f * (SE --> c) = SE --> (f /. c)