theorem :: PARTFUN2:24

for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in dom f holds
Im (f,c) = {(f /. c)}