theorem :: FUNCT_2:91

for X, Y being set
for f, g being PartFunc of X,Y st ( for y being object holds Y <> {y} ) & TotFuncs f = TotFuncs g holds
f = g by Th89;