:: deftheorem Def12 defines FUNCTION_DOMAIN FUNCT_2:def 12 :
for A, B being set
for b₃ being non empty set holds
( b₃ is FUNCTION_DOMAIN of A,B iff for x being Element of b₃ holds x is Function of A,B );