let f be eventually-nonnegative Real_Sequence; :: thesis: Big_Theta f = { t where t 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) <= t . n & t . n <= c * (f . n) ) ) ) }
set BT = { t where t 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) <= t . n & t . n <= c * (f . n) ) ) ) } ;

now

let x be set ; :: thesis: ( ( x in Big_Theta f implies x in { t where t 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) <= t . n & t . n <= c * (f . n) ) ) ) } ) & ( x in { t where t 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) <= t . n & t . n <= c * (f . n) ) ) ) } implies x in Big_Theta f ) )

hereby :: thesis: ( x in { t where t 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) <= t . n & t . n <= c * (f . n) ) ) ) } implies x in Big_Theta f )

assume x in Big_Theta f ; :: thesis: x in { t where t 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) <= t . n & t . n <= c * (f . n) ) ) ) }
then A1: ( x in Big_Oh f & x in Big_Omega f ) by XBOOLE_0:def 4;
then consider t being Element of Funcs NAT ,REAL such that
A2: x = t and
A3: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) ;
consider s being Element of Funcs NAT ,REAL such that
A4: x = s and
A5: 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 ) ) ) by A1;
consider c being Real, N being Element of NAT such that
A6: c > 0 and
A7: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A3;
consider d being Real, N1 being Element of NAT such that
A8: d > 0 and
A9: for n being Element of NAT st n >= N1 holds
( s . n >= d * (f . n) & s . n >= 0 ) by A5;
set a = max N,N1;
A10: ( max N,N1 >= N & max N,N1 >= N1 ) by XXREAL_0:25;

now

take a = max N,N1; :: thesis: for n being Element of NAT st n >= a holds
( d * (f . n) <= t . n & t . n <= c * (f . n) )
let n be Element of NAT ; :: thesis: ( n >= a implies ( d * (f . n) <= t . n & t . n <= c * (f . n) ) )
assume n >= a ; :: thesis: ( d * (f . n) <= t . n & t . n <= c * (f . n) )
then ( n >= N & n >= N1 ) by A10, XXREAL_0:2;
hence ( d * (f . n) <= t . n & t . n <= c * (f . n) ) by A2, A4, A7, A9; :: thesis: verum

end;

hence x in { t where t 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) <= t . n & t . n <= c * (f . n) ) ) ) } by A2, A6, A8; :: thesis: verum

end;

assume x in { t where t 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) <= t . n & t . n <= c * (f . n) ) ) ) } ; :: thesis: x in Big_Theta f
then consider t being Element of Funcs NAT ,REAL such that
A11: x = t and
A12: 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) <= t . n & t . n <= c * (f . n) ) ) ) ;
consider c, d being Real, N being Element of NAT such that
A13: c > 0 and
A14: d > 0 and
A15: for n being Element of NAT st n >= N holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) by A12;
consider N1 being Element of NAT such that
A16: for n being Element of NAT st n >= N1 holds
f . n >= 0 by Def4;
set a = max N,N1;
A17: ( max N,N1 >= N & max N,N1 >= N1 ) by XXREAL_0:25;

now

take a = max N,N1; :: thesis: for n being Element of NAT st n >= a holds
( t . n <= c * (f . n) & t . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= a implies ( t . n <= c * (f . n) & t . n >= 0 ) )
assume n >= a ; :: thesis: ( t . n <= c * (f . n) & t . n >= 0 )
then A18: ( n >= N & n >= N1 ) by A17, XXREAL_0:2;
hence t . n <= c * (f . n) by A15; :: thesis: t . n >= 0
f . n >= 0 by A16, A18;
then d * (f . n) >= d * 0 by A14;
hence t . n >= 0 by A15, A18; :: thesis: verum

end;

then A19: x in Big_Oh f by A11, A13;

now

take a = max N,N1; :: thesis: for n being Element of NAT st n >= a holds
( d * (f . n) <= t . n & t . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= a implies ( d * (f . n) <= t . n & t . n >= 0 ) )
assume n >= a ; :: thesis: ( d * (f . n) <= t . n & t . n >= 0 )
then A20: ( n >= N & n >= N1 ) by A17, XXREAL_0:2;
hence d * (f . n) <= t . n by A15; :: thesis: t . n >= 0
f . n >= 0 by A16, A20;
then d * (f . n) >= d * 0 by A14;
hence t . n >= 0 by A15, A20; :: thesis: verum

end;

then x in Big_Omega f by A11, A14;
hence x in Big_Theta f by A19, XBOOLE_0:def 4; :: thesis: verum

end;

hence Big_Theta f = { t where t 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) <= t . n & t . n <= c * (f . n) ) ) ) } by TARSKI:2; :: thesis: verum