theorem :: FUNCT_2:67

for X, Y being set
for f being PartFunc of X,Y st dom f = X holds
f is Function of X,Y