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:13;
thus f is union-distributive :: thesis: f is cap-distributive
proof
let A be Subset of (dom f); :: according to COHSP_1:def 9 :: 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:7;
f .: A c= {{}}
proof
let x be object ; :: 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 object st
( y in dom f & y in A & x = f . y ) by FUNCT_1:def 6;
then x = {} by A1, FUNCOP_1:7;
hence x in {{}} by TARSKI:def 1; :: thesis: verum
end;
then A3: union (f .: A) c= union {{}} by ZFMISC_1:77;
union {{}} = {} by ZFMISC_1:25;
hence f . (union A) = union (f .: A) by A2, A3; :: thesis: verum
end;
let a, b be set ; :: according to COHSP_1:def 12 :: thesis: ( dom f includes_lattice_of a,b implies f . (a /\ b) = (f . a) /\ (f . b) )
assume A4: dom f includes_lattice_of a,b ; :: thesis: f . (a /\ b) = (f . a) /\ (f . b)
then a in dom f by Th16;
then A5: f . a = {} by A1, FUNCOP_1:7;
a /\ b in dom f by A4, Th16;
hence f . (a /\ b) = (f . a) /\ (f . b) by A1, A5, FUNCOP_1:7; :: thesis: verum