theorem :: FUNCT_2:83

for X, Y being set
for f being PartFunc of X,Y holds TotFuncs f c= Funcs (X,Y)