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 Def13; :: according to FUNCT_1:def 13 :: thesis: verum