theorem :: PARTFUN1:41

for X, Y being set st <:{},X,Y:> is total holds
X = {}