theorem :: PARTFUN1:43

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