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

let x be object ; :: 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 A1: 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 x in Big_Oh 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 ) ) ) ;
x in Big_Omega f by A1, XBOOLE_0:def 4;
then 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 ) ) ) ;
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 :: thesis: ex a being Element of NAT st
for n being Element of NAT st n >= a 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 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 Nat such that
A16: for n being Nat st n >= N1 holds
f . n >= 0 by Def2;
reconsider a = max (N,N1) as Element of NAT by ORDINAL1:def 12;
A17: a >= N1 by XXREAL_0:25;
A18: a >= N by XXREAL_0:25;

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

take a = a; :: 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 A19: n >= a ; :: thesis: ( d * (f . n) <= t . n & t . n >= 0 )
then A20: n >= N by A18, XXREAL_0:2;
hence d * (f . n) <= t . n by A15; :: thesis: t . n >= 0
n >= N1 by A17, A19, XXREAL_0:2;
then f . n >= 0 by A16;
then d * (f . n) >= d * 0 by A14;
hence t . n >= 0 by A15, A20; :: thesis: verum

end;

then A21: x in Big_Omega f by A11, A14;

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

take a = a; :: 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 A22: n >= a ; :: thesis: ( t . n <= c * (f . n) & t . n >= 0 )
then A23: n >= N by A18, XXREAL_0:2;
hence t . n <= c * (f . n) by A15; :: thesis: t . n >= 0
n >= N1 by A17, A22, XXREAL_0:2;
then f . n >= 0 by A16;
then d * (f . n) >= d * 0 by A14;
hence t . n >= 0 by A15, A23; :: thesis: verum

end;

then x in Big_Oh f by A11, A13;
hence x in Big_Theta f by A21, 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