now :: thesis: for r being Real st r in rng (n + X) holds
r > 0

let r be Real; :: thesis: ( r in rng (n + X) implies r > 0 )
assume r in rng (n + X) ; :: thesis: r > 0
then consider x being object such that
A1: ( x in dom (n + X) & (n + X) . x = r ) by FUNCT_1:def 3;
(n + X) . x = n + (X . x) by A1, VALUED_1:def 2;
hence r > 0 by A1; :: thesis: verum

end;

hence n + X is positive-yielding by PARTFUN3:def 1; :: thesis: verum