:: deftheorem defines DOMS VALUED_2:def 1 :
for Y being functional set holds DOMS Y = union { (dom f) where f is Element of Y : verum } ;