theorem :: PARTFUN2:49

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