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 :: thesis: for x being object holds
( ( 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) ) )

let x be object ; :: 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 Nat such that
A1: for n being Nat st n >= N1 holds
f . n >= 0 by Def2;
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;
reconsider a = max (N,N1) as Element of NAT by ORDINAL1:def 12;
A7: a >= N1 by XXREAL_0:25;
A8: a >= N by XXREAL_0:25;

now :: thesis: ex a being Element of NAT st
for n being Element of NAT st n >= a & n in X holds
( d * (f . n) <= t . n & t . n >= 0 )

take a = a; :: 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 :: thesis: ex a being Element of NAT st
for n being Element of NAT st n >= a & n in X holds
( t . n <= c * (f . n) & t . n >= 0 )

take a = a; :: 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 :: thesis: ex a being Element of NAT st
for n being Element of NAT st n >= a & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) )

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