let f, g be eventually-nonnegative Real_Sequence; ( f in Big_Theta g iff Big_Theta f = Big_Theta g )
A1:
Big_Theta g = { 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 * (g . n) <= s . n & s . n <= c * (g . n) ) ) ) }
by ASYMPT_0:27;
consider N2 being Nat such that
A2:
for n being Nat st n >= N2 holds
g . n >= 0
by ASYMPT_0:def 2;
consider N1 being Nat such that
A3:
for n being Nat st n >= N1 holds
f . n >= 0
by ASYMPT_0:def 2;
A4:
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 ASYMPT_0:27;
hereby ( Big_Theta f = Big_Theta g implies f in Big_Theta g )
assume A5:
f in Big_Theta g
;
Big_Theta f = Big_Theta gnow for x being object holds
( ( x in Big_Theta f implies x in Big_Theta g ) & ( x in Big_Theta g implies x in Big_Theta f ) )let x be
object ;
( ( x in Big_Theta f implies x in Big_Theta g ) & ( x in Big_Theta g implies x in Big_Theta f ) )A6:
g in Big_Theta f
by A5, ASYMPT_0:29;
assume
x in Big_Theta g
;
x in Big_Theta fthen consider s being
Element of
Funcs (
NAT,
REAL)
such that A17:
s = x
and A18:
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 * (g . n) <= s . n &
s . n <= c * (g . n) ) ) )
by A1;
consider c,
d being
Real,
N3 being
Element of
NAT such that
c > 0
and A19:
d > 0
and A20:
for
n being
Element of
NAT st
n >= N3 holds
(
d * (g . n) <= s . n &
s . n <= c * (g . n) )
by A18;
reconsider N =
max (
N2,
N3) as
Nat by TARSKI:1;
A21:
N >= N3
by XXREAL_0:25;
A22:
N >= N2
by XXREAL_0:25;
then A26:
s is
eventually-nonnegative
;
s in Big_Theta g
by A1, A18;
hence
x in Big_Theta f
by A17, A26, A6, ASYMPT_0:30;
verum end; hence
Big_Theta f = Big_Theta g
by TARSKI:2;
verum
end;
assume
Big_Theta f = Big_Theta g
; f in Big_Theta g
hence
f in Big_Theta g
by ASYMPT_0:28; verum