set C = the Coherence_Space;
set f = the union-distributive cap-distributive ManySortedSet of the Coherence_Space;
take the union-distributive cap-distributive ManySortedSet of the Coherence_Space ; :: thesis: the union-distributive cap-distributive ManySortedSet of the Coherence_Space is U-linear
thus the union-distributive cap-distributive ManySortedSet of the Coherence_Space is U-linear ; :: thesis: verum