:: deftheorem Def3 defines in_doms NOMIN_2:def 3 :
for F being Function-yielding Function
for d being object holds
( d in_doms F iff for x being object st x in dom F holds
d in dom (F . x) );