theorem :: FUNCT_2:87

for X being set
for y being object
for f being PartFunc of X,{y}
for g being Function of X,{y} holds TotFuncs f = {g}