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