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 9 :: thesis: f . {} = {}
A2: ( {} c= dom f & f .: {} = {} ) ;
( not {} in dom f implies f . {} = {} ) by FUNCT_1:def 2;
hence f . {} = {} by A1, A2, ZFMISC_1:2; :: thesis: verum