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