theorem :: PARTFUN1:42

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