let f be eventually-nonnegative Real_Sequence; :: thesis: for X being set holds Big_Theta f,X = (Big_Oh f,X) /\ (Big_Omega f,X)
let X be set ; :: thesis: Big_Theta f,X = (Big_Oh f,X) /\ (Big_Omega f,X)

now

let x be set ; :: thesis: ( ( x in Big_Theta f,X implies x in (Big_Oh f,X) /\ (Big_Omega f,X) ) & ( x in (Big_Oh f,X) /\ (Big_Omega f,X) implies x in Big_Theta f,X ) )

hereby :: thesis: ( x in (Big_Oh f,X) /\ (Big_Omega f,X) implies x in Big_Theta f,X )

assume x in Big_Theta f,X ; :: thesis: x in (Big_Oh f,X) /\ (Big_Omega f,X)
then consider t being Element of Funcs NAT ,REAL such that
A1: x = t and
A2: 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 & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) ;
consider c, d being Real, N being Element of NAT such that
A3: c > 0 and
A4: d > 0 and
A5: for n being Element of NAT st n >= N & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) by A2;
consider N1 being Element of NAT such that
A6: for n being Element of NAT st n >= N1 holds
f . n >= 0 by Def4;
set a = max N,N1;
A7: ( 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 & n in X holds
( t . n <= c * (f . n) & t . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= a & n in X implies ( t . n <= c * (f . n) & t . n >= 0 ) )
assume that
A8: n >= a and
A9: n in X ; :: thesis: ( t . n <= c * (f . n) & t . n >= 0 )
A10: ( n >= N & n >= N1 ) by A7, A8, XXREAL_0:2;
hence t . n <= c * (f . n) by A5, A9; :: thesis: t . n >= 0
f . n >= 0 by A6, A10;
then d * (f . n) >= d * 0 by A4;
hence t . n >= 0 by A5, A9, A10; :: thesis: verum

end;

then A11: x in Big_Oh f,X by A1, A3;

now

take a = max N,N1; :: thesis: for n being Element of NAT st n >= a & n in X holds
( d * (f . n) <= t . n & t . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= a & n in X implies ( d * (f . n) <= t . n & t . n >= 0 ) )
assume that
A12: n >= a and
A13: n in X ; :: thesis: ( d * (f . n) <= t . n & t . n >= 0 )
A14: ( n >= N & n >= N1 ) by A7, A12, XXREAL_0:2;
hence d * (f . n) <= t . n by A5, A13; :: thesis: t . n >= 0
f . n >= 0 by A6, A14;
then d * (f . n) >= d * 0 by A4;
hence t . n >= 0 by A5, A13, A14; :: thesis: verum

end;

then x in Big_Omega f,X by A1, A4;
hence x in (Big_Oh f,X) /\ (Big_Omega f,X) by A11, XBOOLE_0:def 4; :: thesis: verum

end;

assume x in (Big_Oh f,X) /\ (Big_Omega f,X) ; :: thesis: x in Big_Theta f,X
then A15: ( x in Big_Oh f,X & x in Big_Omega f,X ) by XBOOLE_0:def 4;
then consider t being Element of Funcs NAT ,REAL such that
A16: x = t and
A17: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N & n in X holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) ;
consider s being Element of Funcs NAT ,REAL such that
A18: x = s and
A19: ex d being Real ex N being Element of NAT st
( d > 0 & ( for n being Element of NAT st n >= N & n in X holds
( s . n >= d * (f . n) & s . n >= 0 ) ) ) by A15;
consider c being Real, N being Element of NAT such that
A20: c > 0 and
A21: for n being Element of NAT st n >= N & n in X holds
( t . n <= c * (f . n) & t . n >= 0 ) by A17;
consider d being Real, N1 being Element of NAT such that
A22: d > 0 and
A23: for n being Element of NAT st n >= N1 & n in X holds
( s . n >= d * (f . n) & s . n >= 0 ) by A19;
set a = max N,N1;
A24: ( 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 & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) )
let n be Element of NAT ; :: thesis: ( n >= a & n in X implies ( d * (f . n) <= t . n & t . n <= c * (f . n) ) )
assume that
A25: n >= a and
A26: n in X ; :: thesis: ( d * (f . n) <= t . n & t . n <= c * (f . n) )
( n >= N & n >= N1 ) by A24, A25, XXREAL_0:2;
hence ( d * (f . n) <= t . n & t . n <= c * (f . n) ) by A16, A18, A21, A23, A26; :: thesis: verum

end;

hence x in Big_Theta f,X by A16, A20, A22; :: thesis: verum

end;

hence Big_Theta f,X = (Big_Oh f,X) /\ (Big_Omega f,X) by TARSKI:2; :: thesis: verum