set f = the union-distributive cap-distributive Function of B,C;
take the union-distributive cap-distributive Function of B,C ; :: thesis: the union-distributive cap-distributive Function of B,C is U-linear
dom the union-distributive cap-distributive Function of B,C = B by FUNCT_2:def 1;
then reconsider f = the union-distributive cap-distributive Function of B,C as union-distributive cap-distributive ManySortedSet of B by PARTFUN1:def 2;
f is U-linear ;
hence the union-distributive cap-distributive Function of B,C is U-linear ; :: thesis: verum