theorem :: PARTFUN2:48

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