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