:: deftheorem Def9 defines union-distributive COHSP_1:def 9 :
for f being Function holds
( f is union-distributive iff for A being Subset of (dom f) st union A in dom f holds
f . (union A) = union (f .: A) );