rng (f | X) c= rng f by RELAT_1:70;
hence f | X is uniq-surreal-valued ; :: thesis: verum