:: deftheorem Def10 defines d.union-distributive COHSP_1:def 10 :
for f being Function holds
( f is d.union-distributive iff for A being Subset of (dom f) st A is c=directed & union A in dom f holds
f . (union A) = union (f .: A) );