theorem :: FUNCT_2:84

for X, Y being set holds TotFuncs <:{},X,Y:> = Funcs (X,Y)