theorem :: PARTFUN2:52

for C, D being non empty set
for c being Element of C
for f, f1, g being PartFunc of C,D st c in dom g & f1 = f \/ g holds
f1 /. c = g /. c