let t be set ; :: thesis: for f being eventually-nonnegative Real_Sequence st t in Big_Omega f holds
t is eventually-nonnegative Real_Sequence
let f be eventually-nonnegative Real_Sequence; :: thesis: ( t in Big_Omega f implies t is eventually-nonnegative Real_Sequence )
assume t in Big_Omega f ; :: thesis: t is eventually-nonnegative Real_Sequence
then consider s being Element of Funcs (NAT,REAL) such that
A1: s = t and
A2: ex d being Real ex N being Element of NAT st
( d > 0 & ( for n being Element of NAT st n >= N holds
( s . n >= d * (f . n) & s . n >= 0 ) ) ) ;
reconsider t9 = t as Real_Sequence by A1;
consider d being Real, N being Element of NAT such that
d > 0 and
A3: for n being Element of NAT st n >= N holds
( s . n >= d * (f . n) & s . n >= 0 ) by A2;

now :: thesis: ex N being Nat st
for n being Nat st n >= N holds
t9 . n >= 0

reconsider N = N as Nat ;
take N = N; :: thesis: for n being Nat st n >= N holds
t9 . n >= 0
let n be Nat; :: thesis: ( n >= N implies t9 . n >= 0 )
A4: n in NAT by ORDINAL1:def 12;
assume n >= N ; :: thesis: t9 . n >= 0
hence t9 . n >= 0 by A1, A3, A4; :: thesis: verum

end;

hence t is eventually-nonnegative Real_Sequence by Def2; :: thesis: verum