let f, g be eventually-nonnegative Real_Sequence; :: thesis: ( Big_Oh f = Big_Oh g iff f in Big_Theta g )

hereby :: thesis: ( f in Big_Theta g implies Big_Oh f = Big_Oh g )

assume A1: Big_Oh f = Big_Oh g ; :: thesis: f in Big_Theta g
then g in Big_Oh f by ASYMPT_0:10;
then A2: f in Big_Omega g by ASYMPT_0:19;
f in Big_Oh g by A1, ASYMPT_0:10;
hence f in Big_Theta g by A2, XBOOLE_0:def 4; :: thesis: verum

end;

assume A3: f in Big_Theta g ; :: thesis: Big_Oh f = Big_Oh g

now :: thesis: for x being object holds
( ( x in Big_Oh f implies x in Big_Oh g ) & ( x in Big_Oh g implies x in Big_Oh f ) )

let x be object ; :: thesis: ( ( x in Big_Oh f implies x in Big_Oh g ) & ( x in Big_Oh g implies x in Big_Oh f ) )

hereby :: thesis: ( x in Big_Oh g implies x in Big_Oh f )

assume x in Big_Oh f ; :: thesis: x in Big_Oh g
then consider t being Element of Funcs (NAT,REAL) such that
A4: x = t and
A5: 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 ) ) ) ;
consider c being Real, N being Element of NAT such that
c > 0 and
A6: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A5;

now :: thesis: ex N being Nat st
for n being Nat st n >= N holds
t . n >= 0

reconsider N = N as Nat ;
take N = N; :: thesis: for n being Nat st n >= N holds
t . n >= 0
let n be Nat; :: thesis: ( n >= N implies t . n >= 0 )
A7: n in NAT by ORDINAL1:def 12;
assume n >= N ; :: thesis: t . n >= 0
hence t . n >= 0 by A6, A7; :: thesis: verum

end;

then A8: t is eventually-nonnegative ;
A9: f in Big_Oh g by A3, XBOOLE_0:def 4;
t in Big_Oh f by A5;
hence x in Big_Oh g by A4, A8, A9, ASYMPT_0:12; :: thesis: verum

end;

assume x in Big_Oh g ; :: thesis: x in Big_Oh f
then consider t being Element of Funcs (NAT,REAL) such that
A10: x = t and
A11: 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 * (g . n) & t . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
c > 0 and
A12: for n being Element of NAT st n >= N holds
( t . n <= c * (g . n) & t . n >= 0 ) by A11;

now :: thesis: ex N being Nat st
for n being Nat st n >= N holds
t . n >= 0

reconsider N = N as Nat ;
take N = N; :: thesis: for n being Nat st n >= N holds
t . n >= 0
let n be Nat; :: thesis: ( n >= N implies t . n >= 0 )
A13: n in NAT by ORDINAL1:def 12;
assume n >= N ; :: thesis: t . n >= 0
hence t . n >= 0 by A12, A13; :: thesis: verum

end;

then A14: t is eventually-nonnegative ;
f in Big_Omega g by A3, XBOOLE_0:def 4;
then A15: g in Big_Oh f by ASYMPT_0:19;
t in Big_Oh g by A11;
hence x in Big_Oh f by A10, A14, A15, ASYMPT_0:12; :: thesis: verum

end;

hence Big_Oh f = Big_Oh g by TARSKI:2; :: thesis: verum