thus ( f is positive implies for n being Nat st n in dom f holds
f . n > 0 ) by FUNCT_1:3; :: thesis: ( ( for n being Nat st n in dom f holds
f . n > 0 ) implies f is positive )
assume A3: for n being Nat st n in dom f holds
f . n > 0 ; :: thesis: f is positive
for r being Real st r in rng f holds
0 < r
proof
let r be Real; :: thesis: ( r in rng f implies 0 < r )
assume r in rng f ; :: thesis: 0 < r
then consider x being object such that
A2: ( x in dom f & r = f . x ) by FUNCT_1:def 3;
reconsider n = x as Nat by A2;
thus 0 < r by A2, A3; :: thesis: verum
end;
hence f is positive ; :: thesis: verum