theorem :: FUNCT_2:68

for X, Y being set
for f being PartFunc of X,Y st f is total holds
f is Function of X,Y ;