let f, g be eventually-nonnegative Real_Sequence; :: thesis: ( f in Big_Theta g iff Big_Theta f = Big_Theta g )
A1: Big_Theta f = { s where s is Element of Funcs NAT ,REAL : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * (f . n) <= s . n & s . n <= c * (f . n) ) ) ) } by ASYMPT_0:27;
A2: Big_Theta g = { s where s is Element of Funcs NAT ,REAL : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * (g . n) <= s . n & s . n <= c * (g . n) ) ) ) } by ASYMPT_0:27;
consider N1 being Element of NAT such that
A3: for n being Element of NAT st n >= N1 holds
f . n >= 0 by ASYMPT_0:def 4;
consider N2 being Element of NAT such that
A4: for n being Element of NAT st n >= N2 holds
g . n >= 0 by ASYMPT_0:def 4;

hereby :: thesis: ( Big_Theta f = Big_Theta g implies f in Big_Theta g )

assume A5: f in Big_Theta g ; :: thesis: Big_Theta f = Big_Theta g

now

let x be set ; :: thesis: ( ( x in Big_Theta f implies x in Big_Theta g ) & ( x in Big_Theta g implies x in Big_Theta f ) )

hereby :: thesis: ( x in Big_Theta g implies x in Big_Theta f )

assume x in Big_Theta f ; :: thesis: x in Big_Theta g
then consider s being Element of Funcs NAT ,REAL such that
A6: s = x and
A7: ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * (f . n) <= s . n & s . n <= c * (f . n) ) ) ) by A1;
consider c, d being Real, N3 being Element of NAT such that
c > 0 and
A8: d > 0 and
A9: for n being Element of NAT st n >= N3 holds
( d * (f . n) <= s . n & s . n <= c * (f . n) ) by A7;
set N = max N1,N3;
A10: ( max N1,N3 >= N1 & max N1,N3 >= N3 ) by XXREAL_0:25;

now

take N = max N1,N3; :: thesis: for n being Element of NAT st n >= N holds
s . n >= 0
let n be Element of NAT ; :: thesis: ( n >= N implies s . n >= 0 )
assume n >= N ; :: thesis: s . n >= 0
then A11: ( n >= N1 & n >= N3 ) by A10, XXREAL_0:2;
then f . n >= 0 by A3;
then d * (f . n) >= d * 0 by A8;
hence s . n >= 0 by A9, A11; :: thesis: verum

end;

then A12: s is eventually-nonnegative by ASYMPT_0:def 4;
s in Big_Theta f by A1, A7;
hence x in Big_Theta g by A5, A6, A12, ASYMPT_0:30; :: thesis: verum

end;

assume x in Big_Theta g ; :: thesis: x in Big_Theta f
then consider s being Element of Funcs NAT ,REAL such that
A13: s = x and
A14: ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * (g . n) <= s . n & s . n <= c * (g . n) ) ) ) by A2;
consider c, d being Real, N3 being Element of NAT such that
c > 0 and
A15: d > 0 and
A16: for n being Element of NAT st n >= N3 holds
( d * (g . n) <= s . n & s . n <= c * (g . n) ) by A14;
set N = max N2,N3;
A17: ( max N2,N3 >= N2 & max N2,N3 >= N3 ) by XXREAL_0:25;

now

take N = max N2,N3; :: thesis: for n being Element of NAT st n >= N holds
s . n >= 0
let n be Element of NAT ; :: thesis: ( n >= N implies s . n >= 0 )
assume n >= N ; :: thesis: s . n >= 0
then A18: ( n >= N2 & n >= N3 ) by A17, XXREAL_0:2;
then g . n >= 0 by A4;
then d * (g . n) >= d * 0 by A15;
hence s . n >= 0 by A16, A18; :: thesis: verum

end;

then A19: s is eventually-nonnegative by ASYMPT_0:def 4;
A20: s in Big_Theta g by A2, A14;
g in Big_Theta f by A5, ASYMPT_0:29;
hence x in Big_Theta f by A13, A19, A20, ASYMPT_0:30; :: thesis: verum

end;

hence Big_Theta f = Big_Theta g by TARSKI:2; :: thesis: verum

end;

assume Big_Theta f = Big_Theta g ; :: thesis: f in Big_Theta g
hence f in Big_Theta g by ASYMPT_0:28; :: thesis: verum