set f = the union-distributive cap-distributive Function of C,C;
dom the union-distributive cap-distributive Function of C,C = C by FUNCT_2:52;
then reconsider f = the union-distributive cap-distributive Function of C,C as ManySortedSet of C by PARTFUN1:def 2;
take f ; :: thesis: ( f is union-distributive & f is cap-distributive )
thus ( f is union-distributive & f is cap-distributive ) ; :: thesis: verum