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