theorem :: PARTFUN2:51

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 f & f1 = f \/ g holds
f1 /. c = f /. c