theorem :: PARTFUN1:21

for y being object
for X being set
for f1, f2 being PartFunc of X,{y} st dom f1 = dom f2 holds
f1 = f2