consider C being Coherence_Space;
consider f being union-distributive cap-distributive ManySortedSet of C;
take f ; :: thesis: f is U-linear
thus f is U-linear ; :: thesis: verum