let f be Function; :: thesis: ( f is union-distributive implies f is d.union-distributive )
assume A5: 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 is d.union-distributive
let A be Subset of (dom f); :: according to COHSP_1:def 11 :: thesis: ( A is c=directed & union A in dom f implies f . (union A) = union (f .: A) )
thus ( A is c=directed & union A in dom f implies f . (union A) = union (f .: A) ) by A5; :: thesis: verum