reconsider f = NAT --> 1 as Function of NAT,REAL by FUNCOP_1:45;
take f ; :: thesis: ( f is eventually-nonnegative & f is eventually-nonzero & f is positive & f is eventually-positive & f is eventually-nondecreasing )
thus f is eventually-nonnegative :: thesis: ( f is eventually-nonzero & f is positive & f is eventually-positive & f is eventually-nondecreasing )

proof

take 0 ; :: according to ASYMPT_0:def 2 :: thesis: for n being Element of NAT st n >= 0 holds
f . n >= 0
let n be Element of NAT ; :: thesis: ( n >= 0 implies f . n >= 0 )
assume n >= 0 ; :: thesis: f . n >= 0
thus f . n >= 0 ; :: thesis: verum

end;

thus f is eventually-nonzero :: thesis: ( f is positive & f is eventually-positive & f is eventually-nondecreasing )

proof

take 0 ; :: according to ASYMPT_0:def 5 :: thesis: for n being Element of NAT st n >= 0 holds
f . n <> 0
let n be Element of NAT ; :: thesis: ( n >= 0 implies f . n <> 0 )
thus ( n >= 0 implies f . n <> 0 ) by FUNCOP_1:7; :: thesis: verum

end;

thus f is positive :: thesis: ( f is eventually-positive & f is eventually-nondecreasing )

proof

let n be Element of NAT ; :: according to ASYMPT_0:def 3 :: thesis: f . n > 0
thus f . n > 0 by FUNCOP_1:7; :: thesis: verum

end;

thus f is eventually-positive :: thesis: f is eventually-nondecreasing

proof

take 0 ; :: according to ASYMPT_0:def 4 :: thesis: for n being Element of NAT st n >= 0 holds
f . n > 0
let n be Element of NAT ; :: thesis: ( n >= 0 implies f . n > 0 )
assume n >= 0 ; :: thesis: f . n > 0
thus f . n > 0 by FUNCOP_1:7; :: thesis: verum

end;

thus f is eventually-nondecreasing :: thesis: verum

proof

take 0 ; :: according to ASYMPT_0:def 6 :: thesis: for n being Element of NAT st n >= 0 holds
f . n <= f . (n + 1)
let n be Element of NAT ; :: thesis: ( n >= 0 implies f . n <= f . (n + 1) )
assume n >= 0 ; :: thesis: f . n <= f . (n + 1)
f . n = 1 by FUNCOP_1:7;
hence f . n <= f . (n + 1) by FUNCOP_1:7; :: thesis: verum

end;