reconsider a = {} as Element of C2 by COH_SP:1;
take f = C1 --> a; :: thesis: ( f is union-distributive & f is cap-distributive )
A1: dom f = C1 by FUNCOP_1:19;
thus f is union-distributive :: thesis: f is cap-distributive

proof

let A be Subset of (dom f); :: according to COHSP_1:def 10 :: thesis: ( union A in dom f implies f . (union A) = union (f .: A) )
assume union A in dom f ; :: thesis: f . (union A) = union (f .: A)
then A2: f . (union A) = {} by A1, FUNCOP_1:13;
f .: A c= {{} }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: A or x in {{} } )
assume x in f .: A ; :: thesis: x in {{} }
then ex y being set st
( y in dom f & y in A & x = f . y ) by FUNCT_1:def 12;
then x = {} by A1, FUNCOP_1:13;
hence x in {{} } by TARSKI:def 1; :: thesis: verum

end;

then ( union (f .: A) c= union {{} } & union {{} } = {} ) by ZFMISC_1:31, ZFMISC_1:95;
hence f . (union A) = union (f .: A) by A2; :: thesis: verum

end;

let a, b be set ; :: according to COHSP_1:def 13 :: thesis: ( dom f includes_lattice_of a,b implies f . (a /\ b) = (f . a) /\ (f . b) )
assume dom f includes_lattice_of a,b ; :: thesis: f . (a /\ b) = (f . a) /\ (f . b)
then ( a in dom f & b in dom f & a /\ b in dom f ) by Th17;
then ( f . a = {} & f . b = {} & f . (a /\ b) = {} ) by A1, FUNCOP_1:13;
hence f . (a /\ b) = (f . a) /\ (f . b) ; :: thesis: verum