theorem :: PARTFUN1:44

for X, Y being set
for f being Function st X c= dom f & f .: X c= Y holds
<:f,X,Y:> is total