take f = seq_const 1; :: 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 Nat st n >= 0 holds
f . n >= 0
let n be Nat; :: thesis: ( n >= 0 implies f . n >= 0 )
assume n >= 0 ; :: thesis: f . n >= 0
thus f . n >= 0 by SEQ_1:57; :: 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 Nat st n >= 0 holds
f . n <> 0
let n be Nat; :: thesis: ( n >= 0 implies f . n <> 0 )
thus ( n >= 0 implies f . n <> 0 ) by SEQ_1:57; :: thesis: verum
end;
thus f is positive by SEQ_1:57; :: thesis: ( f is eventually-positive & f is eventually-nondecreasing )
thus f is eventually-positive :: thesis: f is eventually-nondecreasing
proof
take 0 ; :: according to ASYMPT_0:def 4 :: thesis: for n being Nat st n >= 0 holds
f . n > 0
let n be Nat; :: thesis: ( n >= 0 implies f . n > 0 )
assume n >= 0 ; :: thesis: f . n > 0
thus f . n > 0 by SEQ_1:57; :: thesis: verum
end;
thus f is eventually-nondecreasing :: thesis: verum
proof
take 0 ; :: according to ASYMPT_0:def 6 :: thesis: for n being Nat st n >= 0 holds
f . n <= f . (n + 1)
let n be Nat; :: thesis: ( n >= 0 implies f . n <= f . (n + 1) )
assume n >= 0 ; :: thesis: f . n <= f . (n + 1)
f . n = 1 by SEQ_1:57;
hence f . n <= f . (n + 1) by SEQ_1:57; :: thesis: verum
end;