theorem :: FUNCT_4:44

for f being Function ex X, Y being set st dom (~ f) c= [:X,Y:]