rng (f ^ g) = (rng f) \/ (rng g) by ORDINAL4:2;
hence f ^ g is uniq-surreal-valued ; :: thesis: verum