theorem :: PARTFUN2:45

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