now :: thesis: for r being Real st r in rng (min (f,g)) holds
0 < r

let r be Real; :: thesis: ( r in rng (min (f,g)) implies 0 < r )
assume r in rng (min (f,g)) ; :: thesis: 0 < r
then consider x being object such that
A1: x in X and
A2: (min (f,g)) . x = r by FUNCT_2:11;
reconsider y = x as Element of X by A1;
r = min ((f . y),(g . y)) by A2, DEFM1;
then ( r = f . y or r = g . y ) by XXREAL_0:15;
then ( r in rng f or r in rng g ) by FUNCT_2:4;
hence 0 < r by PARTFUN3:def 1; :: thesis: verum

end;

hence min (f,g) is positive-yielding by PARTFUN3:def 1; :: thesis: verum