let f, g be Function of [.0,1.],REAL; :: thesis: rng (min (f,g)) c= (rng f) \/ (rng g)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (min (f,g)) or y in (rng f) \/ (rng g) )
assume y in rng (min (f,g)) ; :: thesis: y in (rng f) \/ (rng g)
then consider x being object such that
A1: ( x in dom (min (f,g)) & y = (min (f,g)) . x ) by FUNCT_1:def 3;
A3: dom (min (f,g)) = [.0,1.] by FUNCT_2:def 1;
( dom f = [.0,1.] & dom g = [.0,1.] ) by FUNCT_2:def 1;
then A2: ( x in dom f & x in dom g ) by A1, FUNCT_2:def 1;
(min (f,g)) . x = min ((f . x),(g . x)) by A1, A3, COUSIN2:def 1;
then ( (min (f,g)) . x = f . x or (min (f,g)) . x = g . x ) by XXREAL_0:15;
then ( y in rng f or y in rng g ) by A1, A2, FUNCT_1:def 3;
hence y in (rng f) \/ (rng g) by XBOOLE_0:def 3; :: thesis: verum