let F be FUNCTION_DOMAIN of A,B; :: thesis: F is functional
thus for x being set st x in F holds
x is Function by Def2; :: according to FUNCT_1:def 19 :: thesis: verum