let f, t be positive Real_Sequence; :: thesis: ( t in Big_Theta f iff ex c, d being Real st
( c > 0 & d > 0 & ( for n being Element of NAT holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) )
A1: Big_Theta f = { s where s 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) <= s . n & s . n <= c * (f . n) ) ) ) } by Th27;

hereby :: thesis: ( ex c, d being Real st
( c > 0 & d > 0 & ( for n being Element of NAT holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) implies t in Big_Theta f )

assume t in Big_Theta f ; :: thesis: ex c, d being Real st
( c > 0 & d > 0 & ( for n being Element of NAT holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) )
then consider s being Element of Funcs (NAT,REAL) such that
A2: s = 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 holds
( d * (f . n) <= s . n & s . n <= c * (f . n) ) ) ) by A1;
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 holds
( d * (f . n) <= s . n & s . n <= c * (f . n) ) by A3;

per cases ( N = 0 or N > 0 ) ;

suppose A7: N = 0 ; :: thesis: ex c, d being Real st
( c > 0 & d > 0 & ( for n being Element of NAT holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) )

take c = c; :: thesis: ex d being Real st
( c > 0 & d > 0 & ( for n being Element of NAT holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) )
take d = d; :: thesis: ( c > 0 & d > 0 & ( for n being Element of NAT holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) )
thus c > 0 by A4; :: thesis: ( d > 0 & ( for n being Element of NAT holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) )
thus d > 0 by A5; :: thesis: for n being Element of NAT holds
( d * (f . n) <= t . n & t . n <= c * (f . n) )
let n be Element of NAT ; :: thesis: ( d * (f . n) <= t . n & t . n <= c * (f . n) )
thus ( d * (f . n) <= t . n & t . n <= c * (f . n) ) by A2, A6, A7; :: thesis: verum

end;

suppose A8: N > 0 ; :: thesis: ex c, d being Real st
( c > 0 & d > 0 & ( for n being Element of NAT holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) )

deffunc H₁( Element of NAT ) -> Element of REAL = (t . $1) / (f . $1);
reconsider B = { H₁(n) where n is Element of NAT : n < N } as non empty finite Subset of REAL from ASYMPT_0:sch 3(A8);
set b = max B;
set a = min B;
A9: for n being Element of NAT st n < N holds
t . n >= (min B) * (f . n)

proof

let n be Element of NAT ; :: thesis: ( n < N implies t . n >= (min B) * (f . n) )
A10: f . n > 0 by Def3;
assume n < N ; :: thesis: t . n >= (min B) * (f . n)
then (t . n) / (f . n) in B ;
then (t . n) / (f . n) >= min B by XXREAL_2:def 7;
then ((t . n) / (f . n)) * (f . n) >= (min B) * (f . n) by A10, XREAL_1:64;
hence t . n >= (min B) * (f . n) by A10, XCMPLX_1:87; :: thesis: verum

end;

A11: for n being Element of NAT st n < N holds
t . n <= (max B) * (f . n)

proof

let n be Element of NAT ; :: thesis: ( n < N implies t . n <= (max B) * (f . n) )
A12: f . n > 0 by Def3;
assume n < N ; :: thesis: t . n <= (max B) * (f . n)
then (t . n) / (f . n) in B ;
then (t . n) / (f . n) <= max B by XXREAL_2:def 8;
then ((t . n) / (f . n)) * (f . n) <= (max B) * (f . n) by A12, XREAL_1:64;
hence t . n <= (max B) * (f . n) by A12, XCMPLX_1:87; :: thesis: verum

end;

thus ex c, d being Real st
( c > 0 & d > 0 & ( for n being Element of NAT holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) :: thesis: verum

proof

set D = min ((min B),d);
set C = max ((max B),c);
reconsider C = max ((max B),c), D = min ((min B),d) as Element of REAL by XREAL_0:def 1;
take C ; :: thesis: ex d being Real st
( C > 0 & d > 0 & ( for n being Element of NAT holds
( d * (f . n) <= t . n & t . n <= C * (f . n) ) ) )
take D ; :: thesis: ( C > 0 & D > 0 & ( for n being Element of NAT holds
( D * (f . n) <= t . n & t . n <= C * (f . n) ) ) )
thus C > 0 by A4, XXREAL_0:25; :: thesis: ( D > 0 & ( for n being Element of NAT holds
( D * (f . n) <= t . n & t . n <= C * (f . n) ) ) )

A13: now :: thesis: for n being Element of NAT holds 0 < (t . n) / (f . n)

let n be Element of NAT ; :: thesis: 0 < (t . n) / (f . n)
( f . n > 0 & t . n > 0 ) by Def3;
then 0 * ((f . n) ") < (t . n) * ((f . n) ") by XREAL_1:68;
hence 0 < (t . n) / (f . n) by XCMPLX_0:def 9; :: thesis: verum

end;

min B > 0

proof

min B in B by XXREAL_2:def 7;
then ex n being Element of NAT st
( min B = (t . n) / (f . n) & n < N ) ;
hence min B > 0 by A13; :: thesis: verum

end;

hence D > 0 by A5, XXREAL_0:15; :: thesis: for n being Element of NAT holds
( D * (f . n) <= t . n & t . n <= C * (f . n) )
let n be Element of NAT ; :: thesis: ( D * (f . n) <= t . n & t . n <= C * (f . n) )
A14: f . n > 0 by Def3;

per cases ( n < N or n >= N ) ;

suppose A15: n < N ; :: thesis: ( D * (f . n) <= t . n & t . n <= C * (f . n) )

A16: D * (f . n) <= (min B) * (f . n) by A14, XREAL_1:64, XXREAL_0:17;
(min B) * (f . n) <= t . n by A9, A15;
hence D * (f . n) <= t . n by A16, XXREAL_0:2; :: thesis: t . n <= C * (f . n)
A17: (max B) * (f . n) <= C * (f . n) by A14, XREAL_1:64, XXREAL_0:25;
t . n <= (max B) * (f . n) by A11, A15;
hence t . n <= C * (f . n) by A17, XXREAL_0:2; :: thesis: verum

end;

suppose A18: n >= N ; :: thesis: ( D * (f . n) <= t . n & t . n <= C * (f . n) )

A19: D * (f . n) <= d * (f . n) by A14, XREAL_1:64, XXREAL_0:17;
d * (f . n) <= t . n by A2, A6, A18;
hence D * (f . n) <= t . n by A19, XXREAL_0:2; :: thesis: t . n <= C * (f . n)
A20: c * (f . n) <= C * (f . n) by A14, XREAL_1:64, XXREAL_0:25;
t . n <= c * (f . n) by A2, A6, A18;
hence t . n <= C * (f . n) by A20, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

end;

given c, d being Real such that A21: ( c > 0 & d > 0 ) and
A22: for n being Element of NAT holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ; :: thesis: t in Big_Theta f
( t is Element of Funcs (NAT,REAL) & ( for n being Element of NAT st n >= 0 holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) by A22, FUNCT_2:8;
hence t in Big_Theta f by A1, A21; :: thesis: verum