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 )

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

end;

then A12: x in Big_Omega f,X by A2, A5;

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
A13: n >= a and
A14: n in X ; :: thesis: ( t . n <= c * (f . n) & t . n >= 0 )
A15: n >= N by A8, A13, XXREAL_0:2;
hence t . n <= c * (f . n) by A6, A14; :: thesis: t . n >= 0
n >= N1 by A7, A13, XXREAL_0:2;
then f . n >= 0 by A1;
then d * (f . n) >= d * 0 by A5;
hence t . n >= 0 by A6, A14, A15; :: thesis: verum

end;

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

end;

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

end;

hence x in Big_Theta f,X by A17, A21, A23; :: thesis: verum

end;

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