consider f being union-distributive cap-distributive Function of C,C;
dom f = C by FUNCT_2:67;
then reconsider f = f as ManySortedSet of C by PARTFUN1:def 4;
take f ; :: thesis: ( f is union-distributive & f is cap-distributive )
thus ( f is union-distributive & f is cap-distributive ) ; :: thesis: verum