let f, g be eventually-nonnegative Real_Sequence; :: thesis: ( f in Big_Theta g iff Big_Theta f = Big_Theta g )
A1: 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 N2 being Element of NAT such that
A2: for n being Element of NAT st n >= N2 holds
g . n >= 0 by ASYMPT_0:def 2;
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 2;
A4: 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;

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 ) )
A6: g in Big_Theta f by A5, ASYMPT_0:29;

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
A7: s = x and
A8: 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 A4;
consider c, d being Real, N3 being Element of NAT such that
c > 0 and
A9: d > 0 and
A10: for n being Element of NAT st n >= N3 holds
( d * (f . n) <= s . n & s . n <= c * (f . n) ) by A8;
set N = max (N1,N3);
A11: max (N1,N3) >= N3 by XXREAL_0:25;
A12: max (N1,N3) >= N1 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 A13: n >= N ; :: thesis: s . n >= 0
then n >= N1 by A12, XXREAL_0:2;
then f . n >= 0 by A3;
then A14: d * (f . n) >= d * 0 by A9;
n >= N3 by A11, A13, XXREAL_0:2;
hence s . n >= 0 by A10, A14; :: thesis: verum

end;

then A15: s is eventually-nonnegative by ASYMPT_0:def 2;
s in Big_Theta f by A4, A8;
hence x in Big_Theta g by A5, A7, A15, 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
A16: s = x and
A17: 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 A1;
consider c, d being Real, N3 being Element of NAT such that
c > 0 and
A18: d > 0 and
A19: for n being Element of NAT st n >= N3 holds
( d * (g . n) <= s . n & s . n <= c * (g . n) ) by A17;
set N = max (N2,N3);
A20: max (N2,N3) >= N3 by XXREAL_0:25;
A21: max (N2,N3) >= N2 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 A22: n >= N ; :: thesis: s . n >= 0
then n >= N2 by A21, XXREAL_0:2;
then g . n >= 0 by A2;
then A23: d * (g . n) >= d * 0 by A18;
n >= N3 by A20, A22, XXREAL_0:2;
hence s . n >= 0 by A19, A23; :: thesis: verum

end;

then A24: s is eventually-nonnegative by ASYMPT_0:def 2;
s in Big_Theta g by A1, A17;
hence x in Big_Theta f by A16, A24, A6, ASYMPT_0:30; :: thesis: verum

end;

hence Big_Theta f = Big_Theta g by TARSKI:1; :: 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