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

r > 0

hence
n + X is positive-yielding
by PARTFUN3:def 1; :: thesis: verumr > 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;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