let f be Function; :: thesis: ( f is union-distributive implies f . {} = {} )
assume A1: for A being Subset of (dom f) st union A in dom f holds
f . (union A) = union (f .: A) ; :: according to COHSP_1:def 10 :: thesis: f . {} = {}
( ( not {} in dom f implies f . {} = {} ) & {} c= dom f & ( {} in dom f or not {} in dom f ) & f .: {} = {} ) by FUNCT_1:def 4, RELAT_1:149, XBOOLE_1:2;
hence f . {} = {} by A1, ZFMISC_1:2; :: thesis: verum